Designing Compilation Techniques for Improving Efficiency of E-ACSL, a Runtime Assertion Checker for C Programs

Full description

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 the ACSL specification language. 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.

E-ACSL is the Frama-C plug-in dedicated to runtime assertion checking. It converts a C program extended with formal annotations written in a subset of ACSL into a new C program which checks the validity of annotations at runtime: by default, the program execution stops whenever one annotation is violated, or behaves in the same way than the input program if all its annotations are valid. One key feature of E-ACSL is the expressivity of its specification language which allows the user to describe powerful safety and security properties. Another key feature is the efficiency of the generated code which relies on a custom memory library and dedicated static analyses.

However E-ACSL can still be improved in many ways in order to extend its expressivity and to reduce its memory and time overheads. To reach this goal, (s)he shall make several contributions, for example regarding some of the following objectives:

• improve the current compilation scheme to reduce the memory footprint of the generated code;
• design new compilation techniques and/or adapt existing ones in order to optimize the efficiency of the generated code;
• design novel dedicated fast static analyses to minimize the generated code;
• design one or several new intermediate representations that would make these developments easier;
• evaluate the benefits of these improvements on concrete benchmarks and/or use cases.

Qualifications

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

• Ocaml programming (at least, functional programming)
• C programming
• compilation
• semantics of programming languages
• static analysis
• runtime verification
• formal specification

Application

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

• Julien Signoles