Current INRIA RBA
UMR CNRS nÂ°6172
Head of the Team SSD
Beside the founded projects, students are paying a particular attention to find impossible challenges:
- extract the memory map of a Java Card using what they called the EMAN attack, which they defind themself,
- execute Java Card applet with a mix of native and interpreted methods. Of course they hard coded the native methods, which is known to be impossible by the specification,
- try to find flaws in implemented byte code verifier.
- In 2002, we designed the first full fledged byte code verifier for Java Card without any external process, we code it into a smart card.
- In 2003, we synthetized specification into a smart card from formal specification. The card was fully functionnal, having written only 10% of the code.
- In 2004, we developped at Gemplus the framework JACK, the Java Applet Correctness Kit, a tool for applet validation. Jack takes Java or JVM programs annotated with JML specifications (or JML-like specifications for JVM programs) as input, and generates appropriate proof obligations. These can be used as input for different proof assistants (automatic or interactive), such as Simplify. This work has been transfered to INRIA.