[Show/Hide Left Column]

  • World
    • No language is assigned to this page.

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 Systems
Contact: 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.
Task 2: Continuous and discrete systems: models and verification
Contact: 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).
Task 3: From high-level to low-level certification
Contact: Virgile Prevosto (CEA, List),
Contact:C. Marché (INRIA Saclay).
Partners involved: LRI, CEA LIST, MAS, UEI, LSV, LIX, INRIA Saclay
  • 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

No records found
Page: 1/7Last Page