Deductive Verification of Rust Programs
by Xavier Denis
Monday 18 December 2023 at 2pm
Batiment 660, Amphitheatre and video conferencing Zoom link.
Abstract. Rust is a programming language introduced in 2015, which provides the programmer with safety features regarding the use of memory. The goal of this thesis is the development of a deductive verification tool for the Rust language, by leveraging the specificities of its type system, in order to simplify memory aliasing management, among other things. Such a verification approach ensures the absence of errors during the execution of the considered programs, as well as their compliance with a formal specification of the expected functional behavior. The theoretical foundation of the approach proposed in this thesis is to use a notion of prophecy that interprets the mutable borrows in the Rust language as a current value and a future value of this borrow. The Coq proof assistant was used to formalize this prophetic encoding and prove the correctness of the associated proof obligation generation. Furthermore, the approach has been implemented in a verification software for Rust that automates the generation of proof obligations and relies on external solvers to validate these obligations. In order to support Rust iterators, an extension has been developed to manipulate closures, as well as a verification technique for iterators and combinators. The implementation has been experimentally evaluated on relevant algorithm and data structure examples. It has also been validated through a significant case study: the verification of a satisfiability modulo theories (SMT) solver.
Jury:
- Sylvain Boulmé, Grenoble INP, VERIMAG (Reviewer)
- Peter Muller, ETH Zürich (Reviewer)
- Claire Dross, Adacore (Examiner)
- Ralf Jung, ETH Zürich (Examiner)
- François Pottier, INRIA, Cambium (Examiner)
- Mihaela Sighireanu, Université Paris-Saclay, LMF (Examiner)
- Jacques-Henri Jourdan, Université Paris-Saclay, LMF (Supervisor)
- Claude Marché, Université Paris-Saclay, LMF (Supervisor)