Private and public contracts for ACSL

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.

When developing a software component, we generally do not expose the same level of visibility in the component (its implementation, the private view) and out of it (its API, the public view). However, this architectural aspect of software design is today an important difficulty for verifying system with Frama-C, since we need to expose all the internal details of the implementation in the specification because ACSL does not distinguish between public and private specifications.

Having these two kinds of specification would be interesting for two main reasons:

• first, it would not be needed modifying software components to verify them using Frama-C, which is a strong need, in particular for certification purposes,
• second, this separation of views would improve verification modularity, which is always useful for scalability.

Of course, having this separation between public and private specification implies important research questions related to correctness and analysis hypotheses. The goal of this 18/24 months postdoc is thus to:

• study the State of the Art,
• design the feature in ACSL,
• determine the changes needed in ACSL++,
• extend the Frama-C kernel and adapt main analyzers,
• evaluate the feature on realistic case studies.

Qualifications

Knowledge in at least one of the following fields is required:

• OCaml programming (at least, functional programming)
• C programming
• semantics of programming languages
• static analysis
• formal specification

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