NICTA Embedded Systems Public Seminar
Formal Modeling and Verification of Smart Cards Embedded Systems
June Andronick, Gemalto's Security Lab.
Time/Venue
Monday 21 April 2008, 12 noon
National ICT Australia Ltd, Level 1 Seminar Room, 223 Anzac Parade (Building L5), Kensington NSW 2052
Abstract
June will present her work done within the Formal Methods Team of Gemalto, the leading smart card manufacturer. She will focus on two main topics: High Level Common Criteria Certification of the Java Card platform and formal verification of low-level embedded C programs.
The Common Criteria is a standard defined to evaluate the security level of computer systems. The highest level of certification requires formal models and proofs giving the assurance that the product respects its security requirements. June will present her contribution to their certification of the Java Card platform, the world's first certificate of a Java product involving formal components. More precisely, June will first present the formal proof that the Java Card platform ensures the confidentiality and integrity of the embedded applications and she will then describe the formal correctness proof of the RMI (Remote Method Invocation) protocol implemented in Java Card 2.2 API.
In the second part, June will focus on the smart card lower levels, with the formal verification of both the correctness and high level properties of C programs. The correctness verification is done using the Caduceus tool that June has extended so that it may handle some unions and casts and so that card-tears may be formalized. June will explain the main ideas of these extensions. The high level verification consists in extracting a transition model from the formal specification in order to enable some temporal reasoning. June will illustrate the whole methodology by the proof of the anti-tearing property for a small erasing function.
Biography
June Andronick is a French Research Engineer in Formal Methods within Gemalto's Security Lab, who started in October 2002 for her master internship. Her PhD has been carried out within Gemalto and supervised by Christine Paulin-Mohring in the team DÉMONS (Proofs and Programs) of the L.R.I. (Laboratory of Research in Computer Science) of the Paris-Sud University. June was also supervised by Boutheina Chetali at Gemalto and Olivier Ly (initially at Gemalto and now at the LaBRI - University of Bordeaux). The aim of their team and of her work is to strengthen the security and safety level of smart card embedded systems, with the use of Formal Methods.