Runtime Verification of Dependency Properties with Undefinedness

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 as the input program if all its annotations are valid.

In ACSL, assigns clauses allow the user to declare the set of memory locations whose values possibly change when executing a function or a statement. Such clauses are usually referred to as frame conditions. They are currently not supported by E-ACSL. The only known solution for implementing frame conditions applies to a simpler setting than ACSL. Checking such properties at runtime in a sound and efficient manner is actually not easy: not only is it necessary to detect which memory locations have been written, but also whether their values have changed, i.e. whether or not the value before the execution of a function/statement is identical to the value after the execution of that function/statement.

Any assigns clause can be extended with a \from clause indicating which memory locations are required for computing the new values of the assigned locations, thereby specifying dependencies between memory locations. For instance, assigns x \from y, *p; means that x is the only modified value and its value can only be computed from the value of y and *p. The support of \from clauses would also constitute a pertinent addition to the runtime checking capabilities of Frama-C, particularly in a security-oriented context.

Last but not least, the memory locations used in assigns ... \from ... clauses may be undefined at runtime, for instance if they involve pointers that point to unallocated memory blocks. This problem, usually referred to as the undefinedness problem, is even more general: many terms involved in ACSL predicates are possibly undefined, meaning that they would lead to undefined behaviors if executed at runtime. Therefore, a mechanism preventing E-ACSL from generating code that leads to undefined behaviors currently exists, but it is fully obsolete: a new solution must be designed and implemented.

The hired researcher should design, formalize, prove correct, implement and evaluate on use cases new solutions to the above problems. We are open to creative solutions, such as proposing static analyses to reduce the time and memory overheads of the generated code or pre-computing symbolic expressions at compile time to be fully evaluated at runtime. The designed solution is to be implemented in E-ACSL and experimented in concrete use cases provided in the context of a research project started in~2025. The results are expected to be published in top-ranked international conferences.

Qualifications

Knowledge in the following fields is warmly appreciated:

• OCaml programming (at least, functional programming)
• C programming
• compilation
• program transformation
• formal semantics of programming languages

Application

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

• Julien Signoles
• Jan Rochel