SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs
Paul Fiterău-Broştean, Bengt Jönsson, Konstantinos Sagonas, Fredrik Tåquist · 2024
Implementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, so-called state machine bugs, can compromise security. SMBugFinder provides an automated framework for detecting these bugs in network protocol implementations using black-box testing. It takes as input a state machine model of the protocol implementation which is tested and a catalogue of bug patterns for the protocol conveniently specified as finite automata. It then produces sequences that expose the catalogued bugs in the tested implementation. Connection to a harness allows SMBugFinder to validate these sequences. The technique behind SMBugFinder has been evaluated successfully on DTLS and SSH in prior work. In this paper, we provide a user-level view of the tool using the EDHOC protocol as an example.