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 the CADP Web 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

Back to the CADP case studies page