University of Applied Sciences Upper Austria (AUSTRIA)
Radboud University Nijmegen (THE NETHERLANDS)
Finite State Machines
CADP (Construction and Analysis of Distributed Processes)
22 states and 154 transitions.
Finite state machines are convenient to model system behaviour. In the
context of security-sensitive systems, finite state machines can be
used to check conformance with security protocols, e.g., to confirm
that some security-sensitive action is only possible after a
successful PIN code check. Thus, state machine learning is a very
useful technique that can be used to automatically reverse engineer
implementations of security protocols, with the objective to detect
security flaws or confirm their absence. Using this technique, it is
possible to discover vulnerabilities occurring when performing actions
in an unexpected order, e.g., performing a security sensitive
operation before having entered a PIN code.
This case study investigates the use of state machine learning to reverse engineer different versions of the e.dentifier2, a USB-connected smartcard reader that a customer operates using his bank card and PIN code. The smartcard reader has a keyboard for the user to enter his PIN code and buttons to cancel or confirm Internet banking transactions. A security vulnerability was discovered in this device by a manual analysis of the USB communication between the PC and the device and the communication between the device and the smartcard.
The goal of this research was to study the automation of such an analysis. To be able to learn the behaviour of the reader, a Lego robot was constructed to operate the keyboard of the smartcard reader. Controlling all this from a laptop, the LearnLib software library for state machine inference, to learn the behaviour of readers.
The models resulting from the automated learning process, were converted to the Aldebaran file format for labelled transition systems. These files were then used as input for the CADP model checker to automatically search for possible vulnerabilities. Doing so, the security vulnerability was automatically revealed. It was also shown that the vulnerability is no longer present in a new version of the device.
Model checkers can then be very helpful to verify security properties,
in particular when the models get increasingly complex. It is also
helpful if the input language of the model checker is easy to
Georg Chalupar and Stefan Peherstorfer and Erik Poll and Joeri de Ruiter.
"Automated Reverse Engineering using Lego".
Proceedings of the 8th USENIX Workshop on Offensive Technologies WOOT'14,
Usenix, August, 2014.
Available on-line at: http://www.usenix.org/conference/woot14/workshop-program/presentation/chalupar
or from the CADP Web site in PDF or PostScript
Joeri de Ruiter
School of Computer Science
University of Birmingham
Birmingham B15 2TT
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|