The CREUSOT Environment for the Deductive Verification of Rust Programs
Résumé
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, which aims at proving the conformity of some code with respect to a specification of its intended behavior. In this report we present Creusot, a tool for the formal specification and deductive verification of Rust programs.
There are two main original features in the approach implemented in Creusot. First, Creusot’s specification language features a notion of prophecies, which is central for the specification of behavior of programs performing memory mutation. Prophecies also permit efficient automated reasoning for verifying about such programs.
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 the second 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.
Rust est un langage de programmation relativement récent pour la programmation système, apportant des garanties statiques de sûreté des accès mémoire à travers une politique rigoureuse d’ownership. Cette approche ouvre une voie prometteuse pour la vérification déductive de code Rust, qui vise à prouver la conformité d’un code vis-à-vis d’une spécification de son comportement prévu. Dans ce rapport nous présentons CREUSOT, un outil pour la spécification formelle et la vérification déductive de programmes Rust.
L’approche mise en œuvre dans CREUSOT s’appuie sur deux caractéristiques originales. Premièrement, le langage de spécification de CREUSOT fournit une notion de prophétie, qui est centrale pour la spécification du comportement des programmes effectuant des modifications en place de la mémoire. Les prophéties permettent aussi un raisonnement automatisé efficace pour vérifier ces programmes.
Rust fournit des fonctionnalités d’abstraction avancées basées sur une notion de trait, largement utilisée dans la bibliothèque standard et dans les codes utilisateur. La prise en charge des traits est la deuxième caractéristique principale de CREUSOT, car elle est au cœur de sa démarche, en particulier pour fournir une abstraction élaborée du comportement fonctionnel des programmes.
Origine : Fichiers produits par l'(les) auteur(s)