Verifying C Programs with Abstraction and Refinements

Institution

The French Alternative Energies and Atomic Energy Commission (CEA) is a key player in research, development, and innovation. Drawing on the widely acknowledged expertise gained by its 16,000 staff spanned over 9 research centers with a budget of 4.1 billion Euros, CEA actively participates in more than 400 European collaborative projects with numerous academic (notably as a member of Paris-Saclay University) and industrial partners. Within the CEA Technological Research Division, the CEA List institute addresses the challenges coming from smart digital systems.

Among other activities, CEA List’s Software Safety and Security Laboratory (LSL) research teams design and implement automated analysis in order to make software systems more trustworthy, to exhaustively detect their vulnerabilities, to guarantee conformity to their specifications, and to accelerate their certification. In particular, the Frama-C platform is dedicated to perform a wide range of analyses over C programs (with an experimental C++ front-end).

Objectives

Formal methods are dedicated to mathematically prove that a program meets its specification. The usual way to do that is to provide developers with a formal specification language, ACSL in the case of Frama-C, in which they can express what their code is supposed to do, often in the form of function contracts, loop invariants, and/or plain assertions. However, such specification languages stay quite close to the code and often impose to speak about very low-level implementation details together with higher-level requirements. This leads to specifications that are hard to maintain, and, maybe more importantly, can make it difficult to assess whether what has been actually proved accurately reflects these high level requirements.

Several approaches, the most well-known being the B method, introduce the notion of refinement to build step by step an implementation starting from an abstract model on which requirements are easy to express. At each step, proof obligations are generated to ensure that the properties expressed at higher level are preserved by the refinement, so that the final implementation is correct by construction. However, this requires writing the entire software within the refinement framework and leaves open the question of linking a correct-by-construction implementation with other components (e.g., hardware drivers). The goal of this internship is to investigate, in the context of Frama-C, C code and ACSL specifications, how to ensure that properties established at an abstract level still hold in the (possibly pre-existing) implementation. In addition to top-down refinement, it will be possible to explore bottom-up approaches for extracting a model from the C code together with invariants formalizing the relationships between code and model.

A possible starting point, related to the 2^nd VerifyThis Long-term Challenge, would be to build a Why3 model for some data structures defined in memcached and investigate how properties established on the model can be reflected back on the actual implementation.

Qualifications

• Minimal

  • Master (M2) student or equivalent
  • knowledge of formal methods
  • knowledge of functional programming
  • ability to work in a team

• Preferred

  • some knowledge of OCaml
  • some knowledge in C
  • a certain flair/affinity for mathematical matters

Characteristics

• Duration: 4-6 months

• Location: CEA Nano-INNOV, Paris-Saclay Campus, France

• Compensation:

  • €700 to €1300 monthly stipend (determined by CEA wage grids)
  • up to €229/month in housing and travel expenses (in case a relocation is needed)
  • CEA shuttle services in Paris region and 75% subsidy on regional transport pass (Navigo)
  • Corporate cafeteria with subsidized lunch

Application

If you are interested in this internship, please send to the contact persons an application containing: - your resume; - a cover letter indicating how your curriculum and experience match the qualifications expected and how you would plan to contribute to the project; - your bachelor and master 1 transcripts; - the contact details of two persons (at least one academic) who can be contacted to provide references.

Applications are welcomed until the position is filled. Please note that administrative processing may take up to 3 months.

Contact persons

For further information or details about the internship before applying, please contact:

• Virgile Prevosto (virgile.prevosto@cea.fr)
• Julien Signoles (julien.signoles@cea.fr)