Internship Position at CEA List - LSL

Context: CEA LIST, Software Security and Reliability Lab

The Software Security and Reliability Laboratory (LSL) at CEA List has an ambitious goal: help designers, developers and validation experts ship high-confidence systems and software. Objects in our surroundings are getting more and more complex, and we have built a reputation for efficiently using formal reasoning to demonstrate their trustworthiness. Within the CEA List Institute, LSL is dedicated to inventing the best possible means to conduct formal verification. In collaboration with the most creative people in academia and the industry, we design methods and tools that leverage innovative approaches to ensure that real-world systems can comply with the highest safety and security standards

Our organizational structure is simple: those who pioneer new concepts are the ones who get to implement them. We are a forty-person team, and your work will have a direct and visible impact on the state of formal verification. CEA List’s offices are located at the heart of Campus Paris Saclay, in the largest European cluster of public and private research.

Work Description

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.

In the context, the goal of the internship will be to propose a Why3 module defining a set of primitives providing a high-level view of some memory operations typically done by a C program. In order to assess the relevance of these operations, the module will be used to define a model of some datastructures, for instance Singly-linked Tail queues, defined in the memcached, which is the subject of the 2^nd VerifyThis Long-term Challenge. The model will consist in implementing a Why3 datatype, with its invariant, and the functions that manipulate this type with their contracts. Ideally, all the contracts will be proved, and, if possible within the duration of the internship, some experiments on using the model to formally verify the actual C code will be conducted.

Application

Qualifications

• Minimal

  • Master student or equivalent. Subject can be adapted to good bachelor students if required
  • knowledge of formal methods
  • knowledge of functional programming
  • ability to work in a team

• Preferred

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

Duration: 4-6 months

Location: CEA Nano-INNOV, Paris-Saclay Campus, France (Work from home possible up to 2 days/week)

Compensation:

• €850 (Bac+3/Bachelor), €1300 (Bac+4/M1), or €1400 monthly stipend
• 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

Availability: Position is opened for academic year 2024-2025; note that a 3-month procedure for administrative and security purposes is required

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

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