
Research
CRYSCOE Project (ANR SSIA). Students:
|
![]() |
| As a hobby, I am the main architect of the RhoBan project. This consists in designing and realising a biped humanoid robot from scratch as a computer science challenge, like these ones. It started as challenge between friends, and finaly I am very proud to announce that the robot, called RhoBan, is now operational, he can walk, get up, go upstairs ... and even dance! | ![]() |
![]() |
My work regarding
software security concerns smart card technology. I am interested in
two particular aspects of security:
Verification of Security Properties using Formal Methods In collaboration with J. Andronick (LRI - AXALTO) and B. Chetali (AXALTO), I investigate the use of the Coq proof assistant for the formal verification of applet isolation properties in Java Card technology. We focus on the confidentiality property. Our work aims at showing how this property is verified by the embedded Java Card virtual machine card manager and the APIs. We also aim at setting up a verification method which allows to complete specifications and to enhance the secure design of the platform. For instance, we describe how the proof of the integrity puts the light on a known bug. Some more information about this work can be found in this paper. |
This technology aims at enforcing semi-automatically counter-measures against fault injection attacks of smart cards. It addresses in a generic way the whole software embedded on the card. In particular, it addresses threats going beyond cryptography-related parts of the embedded software, like threats against the firewall of the Java Card embedded virtual machine, the PIN code verification, etc. Counter-measures are automatically integrated to the source code during the pre-compilation step, according to a guideline defined by the programmer under the form of a set of directives included into the source code. All this technology is developed with the OCAML language.
Some more information about this work can be found in this paper; this technology is protected by a patent belonging to AXALTO company.| Infinite Model
Theory My current work in this area concerns the problem of compositionality of specifications of sequential programs. This consists in deciding in an effective way whether or not a given set of local structural properties of the functions of a program implies a given global behavioural property of the program. I focus on properties expressed in monadic second-order logic dealing with the control flow of the program and the function calls occuring during its execution. This problem has been investigated in relation with the security of open multi-application smart cards. I proved that the compositionality is a decidable problem for sequential programs whose control-flow graphs are of tree-width less than a fixed integer value, which includes in particular structured programs. More information about this work can be found in this paper. |
![]() |
![]() |
Construction
of Pseudo-Isometries for Tree-Like Non-Compact 3-Manifolds Comptes Rendus de l'Académie des Sciences - CRAS 337:7, p 457-460 (2003).[pdf] Using Coq to Verify Java Card Applet Isolation Properties with J. Andronick and B. Chetali proceedings of "16th Theorem Proving in Higher Order Logic", Roma (TPHOL'2003) LNCS 2758, p335-351 (2003). [pdf] Automatic Graph and Graph D0L-Systems proceedings of "25th Mathematical Foundations of Computer Science", Bratislava (MFCS'2000) LNCS 1893, p 539-548 (2000). The Weak Monadic Quantifier Alternation Hierarchy of Equationnal Graphs is Infinite proceedings of "20th Foundations of Software Technology and Theoretical Computer Science", New Delhi (FST-TCS'2000) LNCS 1974; p188-200 (2000). [pdf] |