Downloads provided by UsageCounts
This deposit provides an Ubuntu Virtual Machine (VM) containing the implementation of the bug detection approach presented in the paper 'Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations', accepted at NDSS 2023. The VM also includes instructions for reproducing bug detection experiments on a number of DTLS and SSH implementations. The VM is provided in an '.ova' file, from which it can be imported using a virtual machine client such as VirtualBox. Username and password are 'user' and 'user', respectively. Instructions on how to run the implementation are available in the 'Artifact' folder for which a shortcut is available on the desktop. Paper Abstract: Implementations of stateful security protocols must carefully manage the type and order of exchanged messages and cryptographic material, by maintaining a state machine which keeps track of protocol progress. Corresponding implementation flaws, called state machine bugs, can constitute serious security vulnerabilities. We present an automated black-box technique for detecting state machine bugs in implementations of stateful network protocols. It takes as input a catalogue of state machine bugs for the protocol, each specified as a finite automaton which accepts sequences of messages that exhibit the bug, and a (possibly inaccurate) model of the implementation under test, typically obtained by model learning. Our technique constructs the set of sequences that (according to the model) can be performed by the implementation and that (according to the automaton) expose the bug. These sequences are transformed to test cases on the actual implementation to find a witness for the bug or filter out false alarms. We have applied our technique on three widely-used implementations of SSH servers and nine different DTLS server and client implementations, including their most recent versions. Our automatic technique easily reproduced all bugs identified by security researchers before, and produced witnesses for them. More importantly, it revealed several previously unknown bugs in the same implementations, two new vulnerabilities, and a variety of new bugs and non-conformance issues in newer versions of the same SSH and DTLS implementations.
protocol testing, network security, automata learning
protocol testing, network security, automata learning
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 43 | |
| downloads | 42 |

Views provided by UsageCounts
Downloads provided by UsageCounts