Database of Case Studies Achieved Using CADP

Verification of Models Reverse Engineered from Smart-card Readers

Organisation: University of Applied Sciences Upper Austria (AUSTRIA)
Radboud University Nijmegen (THE NETHERLANDS)

Method: Finite State Machines

Tools used: CADP (Construction and Analysis of Distributed Processes)
LearnLib

Domain: Security.

Period: 2014

Size: 22 states and 154 transitions.

Description: 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.

Conclusions: 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 translate to.

Publications: [Chalupar-Peherstorfer-Poll-DeRuiter-14] 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 our FTP site in PDF or PostScript

Contact:
Joeri de Ruiter
School of Computer Science
University of Birmingham
Edgbaston
Birmingham B15 2TT
UNITED KINGDOM
Email: j.deruiter@cs.bham.ac.uk



Further remarks: This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Mon Feb 29 10:38:23 2016.


Back to the CADP case studies page