Nov 28, 2023


Lecture Notes





Former XLIM UMR CNRS n°6172
DĂ©partement Informatique

Head of the Team SSD

Research Activities

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.

Main contributions

  • 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.

This page may have a more recent version on PmWiki:Research, and a talk page: PmWiki:Research-Talk.

Page Actions