Nov 28, 2023


Lecture Notes




  • INOSSEM (2012-2013) It is a Grand Emprunt project: Technologie de sĂ©curitĂ© et rĂ©silience des rĂ©seaux. It got the label PĂ´le de compĂ©titivitĂ© from Systematic and Elopsys. The aim is to provide security interoperability between smart card manufacturers. Ourmain objective is to provide a Java Card smart card accepting as an additional component security annotation.
  • DIL (2011-2012) This is a regional project (RĂ©gion Limousin) in order to industrialize a prototype of web service to verify on-line security properties of NFC applications. This project ends in April, and the incubation process started. It got an OSEO award.
  • Tisphanie (2009-2011) It is a FUI project, that got the label PĂ´le de compĂ©titivitĂ© from Systematic and Elopsys. The aim of the project is to propose a structured methodology, tools and security evaluation process to give in advance to users (mobile operators, application developers, universities, police , ..) a rapid assessment of the safety of 'secure components' used in mobile phones, PDAs, terminals, PMR, etc. .., for critical applications. Our participation consists in virtualisation security evaluation.
  • Mecanos (2008-2010): It is a FUI project, that got the label PĂ´le de compĂ©titivitĂ© in 2008 from the SCS and Elopsys. The main objective for SSD is to provide an embedded component that could dynamically detect attacks against embedded web server in a Java Card 3.0.
  • 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. 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.
  • 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.

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

Page Actions