Research

Foundations and Spreading of Deductive Program Verification

Programming language semantics

A representative fundational work is those of Balabonski, Lanco, and Melquiond who devised a call-by-need lambda-calculus enabling strong reduction (i.e. reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once 1160. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is strongly normalizing. Moreover, by adding some restrictions to it, the calculus gains the diamond property and only performs reduction sequences of minimal length, which makes it systematically better than the existing strategies. The Abella proof assistant has been used to formalize part of this calculus.

Improving Verification Condition Generation

Continuation-passing style allows us to devise an extremely economical abstract syntax for a generic algorithmic language. This syntax is flexible enough to naturally express conditionals, loops, (higher-order) function calls, and exception handling. It is type-agnostic and state-agnostic, which means that we can combine it with a wide range of type and effect systems. Paskevich 31 shows how programs written in the continuation-passing style can be augmented in a natural way with specification annotations, ghost code, and side-effect discipline. He defines the rules of verification condition generation for this syntax, and shows that the resulting formulas are nearly identical to what traditional approaches, like the weakest precondition calculus, produce for the equivalent algorithmic constructions. This amounts to a minimalistic yet versatile abstract syntax for annotated programs for which one can compute verification conditions without sacrificing their size, legibility, and amenability to automated proof, compared to more traditional methods. This makes it an excellent candidate for internal code representation in program verification tools, a subject of the on-going PhD thesis of P. Patault.

Inference of invariants

The discovery of invariants is another important topic. A fully automatic generation of invariants was studied in collaboration with an industrial partner: we devised an original abstract interpretation based approach using a domain of parametrized binary decision diagrams 27.

Formal Specification Language for C code

ACSL, short for ANSI/ISO C Specification Language, is meant to express precisely and unambiguously the expected behavior of a piece of C code. It plays a central role in Frama-C, as nearly all plug-ins eventually manipulate ACSL specifications, either to generate properties that are to be verified, or to assess that the code is conforming to these specifications. It is thus very important to have a clear view of ACSL’s semantics in order to be sure that what you check with Frama-C is really what you mean. Marché contributed to a chapter 28 of the Frama-C book, describing the language in an agnostic way, independently of the various verification plug-ins that are implemented in the Frama-C platform. It contains many examples and exercises that introduce the main features of the language and insists on the most common pitfalls that users, even experienced ones, may encounter.

Reasoning on mutable memory in program verification

Verification of Rust programs

One of the major success of Toccata during the last years is represented by the results obtained concerning the verification of Rust programs. Rust is a fairly recent programming language for system programming, bringing static guarantees of memory safety through a strong ownership policy. This feature opens promising advances for deductive verification of Rust code. The project underlying the PhD thesis of Denis  51, supervised by Jourdan and Marché, is to propose techniques for the verification of Rust program, using a translation to a purely-functional language. The challenge of this translation is the handling of mutable borrows: pointers which control of aliasing in a region of memory. To overcome this, we used a technique inspired by prophecy variables to predict the final values of borrows  52. This method is implemented in a standalone tool called Creusot  53. The specification language of Creusot features the notion of prophecy mentioned above, which is central for the specification of behavior of programs performing memory mutation. Prophecies also permit efficient automated reasoning for verifying about such programs. Moreover, Rust provides advanced abstraction features based on a notion of traits, extensively used in the standard library and in user code. The support for traits is another main feature of Creusot, because it is at the heart of its approach, in particular for providing complex abstraction of the functional behavior of programs 53. An important step to take further in the applicability of Creusot on a wide variety of Rust code is to support iterators, which are ubiquitous and in fact idiomatic in Rust programming (for example, every for loop is in fact internally desugared into an iterator). Denis and Jourdan 20 proposed a new approach to simplify the specifications of Rust code in presence of iterators, and to also make the proofs more automatic.

Reasoning on Memory Separation using Arithmetic

Paskevich and Filliâtre 26 proposed an approach that helps to improve automation of proofs for certain classes of pointer-manipulating programs. It consists in mapping a recursive data structure onto a numerical domain, in such a way that ownership and separation properties can be expressed in terms of simple arithmetic inequalities. In addition to making the proof simpler, this provides for a clearer and more natural specification.

Reasoning on Resources

Ownership can also be used to reason about resources other than program memory. Guéneau, Jourdan et al. 24 present formal reasoning rules for verifying amortized complexity bounds in a language with thunks. Thunks can be used to construct persistent data structures with good amortized complexity, by suspending expensive computations and memoizing their result. Based on the notion of time credits and debits, this work presents a complete machine-checked reconstruction of Okasaki’s reasoning rules on thunks in a rich separation logic with time credits, and demonstrates their applicability by verifying several of Okasaki’s data structures.

Ownership and Well-Bracketedness

Ability to reason about ownership is also fertile ground for designing reasoning principles that capture powerful semantic properties of programs. In particular, Guéneau et al. 25 show that it is possible to capture well-bracketedness in a Hoare-style program logic based on separation logic, providing proof rules to show correctness of well-bracketed programs both directly and also through defining unary and binary logical relations models based on this program logic.

Multi-language verification

Most of the existing verification tools and systems focus on programs that are written in a single programming language. In practice, however, programs are often composed of components written in different programming languages, interacting through a foreign function interface (FFI). Guéneau et al. 22 develop a novel multi-language program verification system, dubbed Melocoton, for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of programs components written in OCaml and C. The Melocoton program logic is based on separation logic and expressive enough to express fine-grained transfers of ownership between the different languages. It has been fully mechanized in Coq on top of the Iris separation logic framework.

Capability Machines

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. Guéneau et al. 13 present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. They use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. In subsequent work, they show that this approach enables the formal verification of full-system security properties under multiple attacker models: different security objectives of the full system can be verified under a different choice of trust boundary (i.e. under a different attacker model) 69. The proposed verification approach is modular, and is robust: code outside the trust boundary for a given security objective can be arbitrary, unverified attacker-provided code.

Distributed Programs and Concurrency

Our work regarding concurrent programs is mostly represented by new methods based on model-checking, and implemented in the Cubicle tool. The Model Checking Modulo Theories (MCMT) framework is a powerful model checking technique for verifying safety properties of parameterized transition systems. In MCMT, logical formulas are used to represent both transitions and sets of states and safety properties are verified by an SMT-based backward reachability analysis. To be fully automated, the class of formulas handled in MCMT is restricted to cubes, i.e. existentially quantified conjunction of literals. While being very expressive, cubes cannot define properties with a global termination condition, usually described by a universally quantified formula. Conchon and Korneva 19 presented the Cubicle Fuzzy Loop (CFL), a fuzzing-based extension for Cubicle. To prove safety, Cubicle generates invariants, making use of forward exploration strategies like BFS or DFS on finite model instances. However, these standard algorithms are quickly faced with the state explosion problem due to Cubicle’s purely nondeterministic semantics. This causes them to struggle at discovering critical states, hindering invariant generation. CFL replaces this approach with a powerful DFS-like algorithm inspired by fuzzing. Cubicle’s purely nondeterministic execution loop is modified to provide feedback on newly discovered states and visited transitions. This feedback is used by CFL to construct schedulers that guide the model exploration. Not only does this provide Cubicle with a bigger variety of states for generating invariants, it also quickly identifies unsafe models. As a bonus, it adds testing capabilities to Cubicle, such as the ability to detect deadlocks. The first experiments yielded promising results. CFL effectively allows Cubicle to generate crucial invariants, useful to handle hierarchical systems, while also being able to trap bad states and deadlocks in hard-to-reach areas of such models.

Verification of Computer Arithmetic

Error analysis for Logarithm-Sum-Exponential

We have a long tradition of study of various subtle algorithms involving numerical computations, and verified properties regarding accuracy in particular when using floating-point numbers. A set of numerical programs that we studied this year is related to combination of exponential and logarithm functions, Bonnot et al. 30 provide certified bounds on the accuracy of the log-sum-exp function known in the context of Machine Learning  62. Writing a formal proof offers the highest possible confidence in the correctness of a mathematical library. This comes at a large cost though, since formal proofs require taking into account all the details, even the seemingly insignificant ones, which makes them tedious to write. This issue is compounded by the fact that the objects whose properties we need to verify (floating-point numbers) are not the ones we would like to reason about (real numbers and integers). Geneau, Melquiond and Faissole 21 explore some ways of reducing the overhead of formal proofs in the setting of mathematical libraries, so as to let the user focus on the details that really matter.

Automating the reasoning on Floating-Point Numbers and Real Numbers

Performing a formal verification inside a proof system such as Coq might be a costly endeavor. In some cases, it might be much more efficient to turn the whole process of proof generation and proof checking into the evaluation of a boolean formula, accompanied with a proof that, if this formula evaluates to true, then the original property holds. This approach has long been used for proofs that involve computations on large integers. Martin-Dorel, Melquiond and Roux 14 have shown that computational reflection can also be achieved using floating-point arithmetic, despite the inherent round-off errors, thus leveraging the large computing power of the floating-point units for formal proofs.

Survey on Floating-Point Arithmetic

Boldo et al. published a survey on floating-point arithmetic 12 as an open-access journal paper in Acta Numerica in order to spread the knowledge on computer arithmetic.

Formalization of Mathematics

The correctness of programs solving partial differential equations may rely on mathematics yet unformalized, such as Sobolev spaces. Boldo et al.  43 therefore formalized the mathematical concept of Lebesgue integration and the associated results in Coq ( $\sigma$ -algebras, measures, simple functions, and integration of non-negative measurable functions, up to the full formal proofs of the Beppo Levi Theorem and Fatou’s Lemma). Boldo et al.  29, 18 extended this formalization with Tonelli’s theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration.

Manifest Termination

In formal systems combining dependent types and inductive types, such as Coq, non-terminating programs are frowned upon. They can indeed be made to return impossible results, thus endangering the consistency of the system, although the transient usage of a non-terminating Y combinator, typically for searching witnesses, is safe. To avoid this issue, the definition of a recursive function is allowed only if one of its arguments is of an inductive type and any recursive call is performed on a syntactically smaller argument. If there is no such argument, the user has to artificially add one, e.g., an accessibility property. Free monads can still be used to address general recursion and elegant methods make possible to extract partial functions from sophisticated recursive schemes. The latter yet rely on an inductive characterization of the domain of a function, and of its computational graph, which in turn might require a substantial effort of specification and proof. This leads to a rather frustrating situation when computations are involved. Indeed, the user first has to formally prove that the function will terminate, then the computation can be performed, and finally a result is obtained (assuming the user waited long enough). But since the computation did terminate, what was the point of proving that it would terminate? Mahboubi and Melquiond 23 investigated how users of proof assistants based on variants of the Calculus of Inductive Constructions could benefit from manifestly terminating computations.

Spreading Formal Proofs

Specifying, Testing, and Verifying OCaml programs

Our work on OCaml programs is not limited to purely static verification: we worked on runtime assertion checking for OCaml. In behavioural specifications of imperative languages, postconditions may refer to the prestate of the function, usually with an old operator. Therefore, code performing runtime verification has to record prestate values required to evaluate the postconditions, typically by copying part of the memory state, which causes severe verification overhead, both in memory and CPU time. Filliâtre and Pascutto  55, 67 consider the problem of efficiently capturing prestates in the context of Ortac, a runtime assertion checking tool for OCaml. Their contribution is a postcondition transformation that reduces the subset of the prestate to copy. They formalize this transformation, and they provide proof that it is sound and improves the performance of the instrumented programs. They illustrate the benefits of this approach with a maze generator. Benchmarks show that unoptimized instrumentation is not practicable, while their transformation restores performances similar to the program without any runtime check.

Leveraging Formal Specifications to Generate Fuzzing Suites

When testing a library, developers typically first have to capture the semantics they want to check. They then write the code implementing these tests and find relevant test cases that expose possible misbehaviours. In this work, Osborne and Pascutto  66, 67 present a tool that automatically takes care of these last two steps by automatically generating fuzz testing suites from OCaml interfaces annotated with formal behavioral specifications. They also show some ongoing experiments on the capabilities and limitations of fuzzing applied to real-world libraries.

Compiling OCaml to WebAssembly

As part of his CIFRE PhD with OCamlPro, Léo Andrès formalizes a compilation scheme from OCaml to WebAssembly. This on-going work already validated several Wasm extensions 17. A by-product of the thesis is the implementation of a new, efficient interpreter for Wasm, owi. Léo collaborates with José Fragoso Santos and Filipe Marques (Universidade de Lisboa, Portugal), who are using owi for concolic execution of WebAssembly programs.