SciLex, Software Reliability and Security
Contact : Stefan Haar & Florent Kirchner
Programs are very helpful and greatly facilitate our lives. Unfortunately, they are not fully reliable. They often have “bugs”.
Software engineering and software verification have been a concern for many years. Development practices and software usage however have dramatically evolved in recent years. The main evolution comes from the explosion of communications. This is both an opportunity and a threat. It is an opportunity because we have access to many more resources; It is a threat because the execution environment of a program cannot be guessed beforehand. Also, in such an open world, malicious users can disturb the computations or get access to private information. How can we get some assurance of the security of the communications/applications? Task 1 addresses this issue.
Many devices involve both physical components and software (discrete) control: these are hybrid systems. The physical devices use and measure real (continous) values, while the programs compute with discrete domains. The computations are therefore performed on approximations. Furthermore, the operations that are performed by these programs may themselves be approximate, e.g., when dividing floating point numbers. Can we trust such programs, even when they are certified? This requires a robustness guarantee. Task 2 addresses this and other related issues.
Finally, while many companies, e.g., Airbus or Astrium, use verification and test techniques intensively at various levels in their critical embedded software, there is still a problem with the combination of the verification tasks that are performed at these various levels. For example, a theorem prover or a model-checker can be used to prove a specification, invariants can be computed or a static analysis can be performed and verified on some high-level implementation, finally tests and verifications can be performed at the bytecode or circuit level. One major concern from industry is to improve the consistency of these verification tasks. Task 3 addresses this issue and related ones.
Task 1: Security of SystemsContact: Benjamin Smith, INRIA-Saclay & LIX,
Contact: Maryline Laurent, Telecom-Sudparis
Partners involved: : DAVID, LI-PaRAD, LRI, CEA LIST, MAS, UEI, LSV, LIX, INRIA Saclay, LTCI.
Eric Goubault (CEA, LIST).
Contact: Alexandre Chapoutot ( ENSTA Paristech in U2IS).
Partners involved: LRI, CEA LIST, MAS, UEI, LSV, LIX, INRIA Saclay, INRIA Paris - Rocquencourt, L2S
Collaborations: S. Gaubert (INRIA, labex Maths).
Contact:C. Marché (INRIA Saclay).
Partners involved: LRI, CEA LIST, MAS, UEI, LSV, LIX, INRIA Saclay
- CEA LIST
- MAS, Ecole Centrale Paris
- INRIA Paris-Rocquencourt
- INRIA Saclay - Île-de-France
- LIX, Ecole Polytechnique & CNRS
- LRI, Université Paris-Sud & CNRS
- LSV, ENS Cachan & CNRS
- LTCI, Télécoms ParisTech & CNRS
- SAMOVAR, Télécoms SudParis & CNRS
- U2IS, ENSTA ParisTech
Related Phd thesis funded by DigiCosme :
Other related PhD thesis
No records found