Design and develop the new AST of Frama-C

Context: CEA List, Software Safety and Security Lab

CEA List’s offices are located at the heart of Université Paris-Saclay, the largest European cluster of public and private research. Within CEA List, the Software Safety and Security Lab has an ambitious goal: help designers, developers and validation experts ship high-confidence systems and software.

Systems in our surroundings are getting more and more complex, and we have built a reputation for efficiently using formal reasoning to demonstrate their trustworthiness through the design of methods and tools to ensure that real-world systems can comply with the highest safety and security standards. In doing so, we get to interact with the most creative people in academia and the industry, worldwide.

Our organizational structure is simple: those who pioneer new concepts are the ones who get to implement them. We are a fifty-person team, and your work will have a direct and visible impact on the state of formal verification.

Work Description

Our team develops Frama-C, a code analysis platform for C programs which provides several analyzers as plug-ins. Frama-C itself is developed in OCaml. Frama-C allows the user to annotate C programs with formal specifications written in a specification language named ACSL. Frama-C can then ensure that a C program satisfies its formal specification by relying on several techniques including abstract interpretation, weakest preconditions calculus, and runtime assertion checking.

Frama-C uses its own AST, based on CIL. The main reason is that it eases the development of analyzers by normalizing some program constructs. Today, we have better high-level abstractions for that, and oppositely we have increasing need for APIs that are close to the original code. Furthermore, we want to move Frama-C to new programming languages, thus this C AST is not suitable anymore. Thus, we have started the design of a new AST, able to capture any programming language.

For now, our work focused on creating an AST with type-safe transformation steps, limited to C so that we can evaluate it with our current analysis capabilities. Now, we need to finish this C support and extend to the specification language: ACSL.

Your role will be to: - finalize the new typer/code transformer for C, - implement the ACSL support, - implement the conversion to the CIL AST for analyzers compatibility, - adapt analyzers to the new AST.

Qualifications

• PhD or more than three years of experience in a research-intensive team
• Ability to develop in OCaml or other functional languages
• Knowledge of formal methods or language semantics
• Knowledge of the C language and ability to quickly grasp new ones

Application

This position will be filled as soon as possible; yet a 3+-months procedure for administrative and security purposes is required.

• Virgile Prevosto
• Allan Blanchard