Paul Fiterau-Brostean (Uppsala University, Sweden), Bengt Jonsson (Uppsala University, Sweden), Konstantinos Sagonas (Uppsala University, Sweden and National Technical University of Athens, Greece), Fredrik Tåquist (Uppsala University, Sweden)

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 emph{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 then 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 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.

View More Papers

Drone Security and the Mysterious Case of DJI's DroneID

Nico Schiller (Ruhr-Universität Bochum), Merlin Chlosta (CISPA Helmholtz Center for Information Security), Moritz Schloegel (Ruhr-Universität Bochum), Nils Bars (Ruhr University Bochum), Thorsten Eisenhofer (Ruhr University Bochum), Tobias Scharnowski (Ruhr-University Bochum), Felix Domke (Independent), Lea Schönherr (CISPA Helmholtz Center for Information Security), Thorsten Holz (CISPA Helmholtz Center for Information Security)

Read More

Accurate Compiler and Optimization Independent Function Identification Using Program...

Derrick McKee (Purdue University), Nathan Burow (MIT Lincoln Laboratory), Mathias Payer (EPFL)

Read More

Detecting Unknown Encrypted Malicious Traffic in Real Time via...

Chuanpu Fu (Tsinghua University), Qi Li (Tsinghua University), Ke Xu (Tsinghua University)

Read More

POSE: Practical Off-chain Smart Contract Execution

Tommaso Frassetto (Technical University of Darmstadt), Patrick Jauernig (Technical University of Darmstadt), David Koisser (Technical University of Darmstadt), David Kretzler (Technical University of Darmstadt), Benjamin Schlosser (Technical University of Darmstadt), Sebastian Faust (Technical University of Darmstadt), Ahmad-Reza Sadeghi (Technical University of Darmstadt)

Read More