Runtime Verification of Multi-State Properties

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.

This PhD will be a collaboration between CEA List and Université d’Orléans in the context of a recently accepted research project. Therefore, the PhD student will also be a member of the Languages, Modeling, Verification (LMV) team of LIFO, the Laboratory of Fundamental Computer Science in Orléans, Université d’Orléans. The overall objective of the LMV team is to advance the reliability and security of software, particularly in the context of the Internet of Things (IoT). We aim to ensure that the software involved satisfies critical properties either by construction by leveraging the design of libraries and programming languages, or by using formal methods.

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.

In the ACSL specification language, the at construct allows the user to refer to the value of a term (or a predicate) at another program point. For instance, the assertion /*@ assert x == \at(x, L) + 1; */ checks that the value of variable x has been incremented by 1 between the program point L and the current program point. It generalizes the \old construct that exists in most similar specification languages. Such properties are sometimes refered to as “multi-state properties”. Another example of a multi-state property is related to function/predicate calls, such as f{L}(x). Here, the challenge consists in evaluating the function/predicate body at program point L but its argument (here, x) at the current program point.

The goal of the PhD consists in designing, formalizing, implementing, and proving correct new solutions for runtime checking of as many multi-state properties as possible. Currently, for the at construct, the state-of-the-art solutions for languages in which the size of any allocated blocks is statically known require to copy large pieces of program memory, which is not efficient. For languages in which the size of allocated block is not necessarily statically known, such as C, an equivalent solution would require to copy the whole program memory, which is not reasonable. In such a context, a solution might consist in including a static analysis that would approximate soundly the memory locations that would be copied at runtime. There is currently no solution for multi-state function/predicate calls.

The designed solution will be implemented in E-ACSL and experimented in concrete use cases. In particular, supporting such constructs is required to support runtime verification of MetAcsl’s high-level properties, such as confidentiality and integrity properties. Among others, Thales uses MetAcsl to verify security properties of smard card’s virtual machine: this PhD thesis would help Thales to include E-ACSL in its verification toolchain.

The formalization work and the proof of soundness will be done on a subset of C and ACSL, including the key constructs. Optionnally, they could be done within a proof assistant, such as Coq.

Qualifications

Knowledge in the following fields is appreciated:

• Ocaml programming (at least, functional programming)
• C programming
• compilation
• runtime verification
• 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.

• Jan Rochel
• Julien Signoles
• Frédéric Loulergue

Please join a detailed CV, and a motivation letter.