Jean-Louis LANET
Engineer at Inria DirDRI
and senior research associate in the Everest team at INRIA Sophia-Antipolis.
Formerly senior researcher at Gemplus Research Labs, leading smart card
manufacter.
Research Interests
- formally certified platforms components for smartcards,
- secure and modular operating systems,
- program verification,
- testing technology.
Scientific Activities
Publications
Some of my papers can be easily accessed through page at DBLP; most of my papers can be accessed through
Gemplus Research Labs publication page".
Some current projects:
- ACI Sécurité SPOPS: Secure
Operating Systems for Trusted Personal Devices : The use of Personal
Devices as secure token s for multiple applications in a distributed
and heterogeneous environnement creates needs of flexibility and security. The aim of this project
is to study the feasability of a compromise by developping verification
mechanisms based on type systems and proof carrying code to guarantee
the security of the system in a dynamically reconfigurable exo kernel.
- IST Project INSPIRED. Proposal n°507894 : The
concept of an individual object representing the root of trust is
the paradigm which definitely made the success of the smart card. This
project intends to extend it for the next generation of secure
communicating devices. Within this project our role is to define
methodology to verify the correctness of smart card applications.
Some past projects
- Matisse project (IST
program) methodologies and technologies for industrial engineering. In
this project we successfully applied formal methods for software
design. We obtained the first formally developed smart card. This work
has been presented to Sun Microsystems and Visa International as the
first full Java bytecode verifier embedded into a smart card.
- COTE project (founded by
RNTL): test synthesis in collaboration with IRISA (French Computer
Science Research Institute). In this we applied model-checking
techniques to generate from UML diagram test sequences. One of the
tools developed within this project has been adapted to JML technology.
- PACAP project.
We have developed a tool for analysing interaction between Java
applications inside smart card in collaboration with ONERA-Toulouse. We
translated call graphs into SMV semantics, automatically inserting the
properties in the model. The verification was done using the SMV model
checker.
Contact
INRIA Sophia-Antipolis
2004 Route des Lucioles
BP 93, 06902 Sophia Antipolis Cedex
France
Phone: (33) 06 77 68 88 49
e-mail: Jean-Louis.Lanet@inria.fr
Supervisor of
- Ludovic Casset,
Thèse soutenue à Marseille en octobre 2002, Construction
correcte de logiciels pour carte à puces,
- Hugues Martin,
Thèse soutenue à Lille en mars 2001, Une
méthodologie de génération automatique de suites de
tests pour applet Java Card,
- Damien Deville, DEA
Université de Lille septembre 2001, Développement d’un
vérifieur de byte code java optimisé pour carte à
micro processeurs,
- Abdellah El-Marouani,
DESS Université de Marseille, juillet 2000, Traducteur de byte
code Java vers SMV,
- Stéphanie Motré,
DEA de l’Université de Marseille, soutenu en juin 1999,
Modélisation du Firewall en utilisant des méthodes
formelles,
- Ludovic Casset, DEA de
l’université de Marseille, soutenu en juin 1999,
Spécification formelle du vérifieur de byte code Java en
utilisant la méthode B,
- Gaëlle Bossu,
Mémoire de maîtrise, Université de Besançon
juin 1999, Traducteur de spécification B vers C,
- Antoine Requet, DEA de
l’Université de Besançon, septembre 1998,
Spécification formelle en B d’unconvertisseur de byte code pour
applet java card.
Back Home
Program committee
Afadl 2001,ZB 2002,RCS03, E-smart
2002 et 2003 et Cardis 2004.
Back Home
Revue
- Checking Secure Interactions of Smart Card Applets, (Extended
version) Journal of Computer Security vol. 10, N°4, 2002, pp.
369-398, co-author with P. Bieber, J. Cazin, P. Girard, V. Wiels, G.
Zanon
- Cartes à puce et méthodes formelles, une lente
intégration…, TSI, Vol. 20 n°7/2001, pp. 959-964.
- New Security Issues Raised by Open Cards, Elsevier Information
Security, vol. 4, n°2, pp. 19-27, June 1999, coauthor with P. Girard
Back Home
International conference
- Java Card Applet Validation: method and tool,submitted at
e-smart’03, co-author with Lydie Du Bousquet and Hugues Martin.
- Java Applet Correctness: a Developper-Oriented Approach,
submitted at FME’03, co-author with Lilian Burdy and Antoine Requet.
- An integrated Approach for Java Card applets Validation,
submitted at QSIC, September 2003, co-author with Lydie Du Bousquet and
Hugues Martin.
- Increasing smart card dependability, SIGOPS EW 2002, pp. 209-212,
Saint Emilion, September 2002, co-author with L. Casset.
- On Card byte code verification, the ultimate step, Java One 2002,
Technical session, San Francisco, March 2002, co-author with D. Deville
and L. Casset.
- The use of B for Smart Card, FDL’02, Forum on Specification and
Design Languages, proceedings vol.2, Marseille, September 24-27, 2002.
- Checking Secure Interactions of Smart Card Applets, ESORICS 2000,
LNCS n°1895, pp. 1-16, Toulouse, October 2000 co-author with P.
Bieber, J. Cazin, P. Girard, V. Wiels and G. Zanon
- The PACAP prototype: a tool for detecting Java Card illegal flow,
Java Card 2000, LNCS n°2041, pp. 25-37, Cannes Sept. 2000, co-author
with P. Bieber, J. Cazin, A. El Marouani, P. Girard, V. Wiels and G.
Zanon
- FACADE-A typed Intermediate Language Dedicated to Smart Cards,
Esec Fse'99, LNCS n°1687, pp. 476-493, Toulouse, September 1999,
co-author with G. Grimaud and J.-J. Vandewalle.
- How to formally specify the Java Byte code semantics using the B
method, ECOOP 99 Workshop06, Formal Techniques for Java Programs, pp.
1-8, Lisbon, June 99, TR University of Hagen n°251-5/1999 co-author
with L. Casset
- Formal Proof of Smart Card Applets Correctness, CARDIS'98, LNCS
Louvain la Neuve; Belgium, LNCS n°1820, pp. 85-97, September 98,
co-author with A. Requet
- The Use of Formal Methods for Smart Cards, a comparison between B
and SDL to Model the T=1 protocol, International Workshop on Comparing
Systems Specification Techniques, pp. 3-16, Nantes March 26-27 1998,
coauthor with P. Lartigue.
- Jet Engine Control Systems, IEEE International Workshop on
Embedded Fault Tolerant Systems, September 1996, Dallas, Texas USA,
co-author with T. Bickard and N. Hubart
- A load Balancing Task Allocation Scheme in a hard Real Time
System, Euro-Par'96, pp. 640-643, August 96, Lyon.
- Maintenance Tool for a Fault-Tolerant Distributed Turbo Jet
Engine Control Computer, CESA'96, pp. 659-663, July 1996, Lille,
co-author with N. Hubart
- Allocating tasks in a Fault Tolerant Real Time System, Conference
on Real Time Systems, pp 244-252 , September 95, Wroclaw, Poland.
Back Home
Invited Speaker
- GemClassifier, a formally developed smart card, 2nd HCSS
Conference, pp. 17-23, Baltimore Maryland, USA, March 2002.
- Are smart card the ideal domain for applying formal methods, ZB
2000, LNCS n°1878, pp. 363-373, York, August 2000.
- Industrial Use of Formal Methods at Gemplus, Workshop on
Modelling and Verification, Besançon, 1999
Back
Home