SMBugFinder: An Automated Framework for Testing Protocol Implementations for State Machine Bugs

Implementations of stateful network protocols must keep track of the presence, order and type of exchanged messages. Any errors, socalled 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. CCS CONCEPTS • Software and its engineering → Software testing and debugging; • Security and privacy → Software security engineering.