Research Interests

• formally certified platforms components for smartcards,
  
• secure and modular operating systems, 
• program verification,
• testing technology.
  

Scientific Activities

• Supervisor of several Students
• Member of program committees
  

Publications

• Journals
  
• International conference
• Invited speaker
  

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

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

• 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

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

• 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