Internship Position at CEA List - LSL

Context: CEA LIST, Software Security and Reliability Lab

The Software Safety and Security 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

Frama-C is a software platform dedicated to the formal verification of C programs via a wide set of program analysis technics provided as plugins. Frama-C is often used in the context of critical software development (in aeronautics, railways, nuclear industry, etc.), where regulations impose very stringent code verification objectives, and integrated as part of a broader safety and/or security validation process.

One of the key results of the analysis plug-ins is the validity status of properties about the code, which take the form of ACSL annotations, either written by the user or generated by a plug-in. A notable example of annotations generator is the RTE plug-in, that emits ACSL assertions whose validity implies the absence of undefined behaviors in the program. Another important result is brought specifically by the Eva analyzer, that provides for each program point an over-approximation of all the memory states with which this point might be reached during any concrete execution, using abstract interpretation techniques.

These results can be visualized in Ivette, Frama-C’s GUI. However, in order to facilitate the integration of the tool into various development processes, it would also be useful to provide a way for accessing these results through an IDE, or a web UI (e.g. in a GitHub or GitLab project). A first step towards this goal has been materialized by a prototype implementing a LSP server. LSP, or Language Server Protocol, is a widely-used protocol for communicating information about some code to IDEs. However, LSP is mostly aimed at editing code, and not at verifying an already written program. The goal of this internship is to extend this initial prototype to support other formats that are better suited to let Frama-C interact with IDEs. Two possibilities can be considered, whose choice will be left to the intern:

• SLSP, an extension of LSP that adds messages dedicated to specification and verification activities
• LSIF, which can be seen as a static version of LSP, where the language “server” dumps its entire knowledge in a LSIF database, which can then be queried at will by the client, be it an IDE or a web UI.

Application

Qualifications:

• Minimal
  • Bachelor or Master student in Computer Science or Computer Engineering
  • Solid knowledge of OCaml
  • Ability to work in a team
• Preferred
  • Familiarity with the Frama-C platform
  • Familiarity with LSP/LSIF
  • Some knowledge of imperative programming, preferably C

Duration: 5-6 months

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

Compensation:

• €850 (Bac+3/Bachelor), €1300 (Bac+4/M1), €1400 (Bac+5/M2) monthly stipend
• Maximum €229 housing and travel expense monthly allowance (in case a relocation is needed)
• CEA shuttle in Paris region and 75% refund of transit pass
• Subsidized lunches

Availability: Position is opened for the academic year 2024-2025; Please 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)
• Michele Alberti (michele.alberti@cea.fr)