Prusti

Prusti is an automated program verifier for Rust, based on the Viper infrastructure. It leverages Rust's strong type guarantees to simplify the specification and verification of Rust programs.

Formal verification of system software is notoriously difficult and requires complex specifications and logics (such as separation logic) to reason about pointers, aliasing, and side effects on mutable state. Although powerful, these formal techniques are typically applicable only by expert researchers.

The external pageRust programming language includes an ownership type system which guarantees rich memory safety properties: well-typed Rust programs are guaranteed to not exhibit problems such as dangling pointers, data races, and unexpected side effects through aliased references.

In this project, we exploit Rust's type system to greatly simplify the specification and verification of Rust programs. In particular, we lift the ownership and framing-related information required for a separation logic proof from the type-checking of the program performed by the Rust compiler; user specifications are automatically interwoven, and focus on the desired functional guarantees expressed in a syntax similar to that of Rust program expressions.

In particular, although our verification tools construct formal proofs in a sophisticated logic, the user-level interaction with these tools is kept at a suitable level of abstraction which elides these full details. Our underlying tools are based on the Viper verification infrastructure.

The first versions of our tools are under development, and target a small but interesting fragment of Rust without unsafe features; in the future, we plan to extend our work to tackle a large portion of the language, including certain patterns of unsafe Rust code. The project is available on external pageGitHub and can be used via the external page"Prusti Assistant" extension for Visual Studio Code.

Project Members

Vytautas Astrauskas
Aurel Bílý
Jonas Fiala
external pageChristoph Matheja (DTU Copenhagen)
Peter Müller
Federico Poli
external pageAlex Summers (UBC)

Links

external pagePrusti User Guide
external pageGitHub repository
external pageZulip channel
Prusti versions of the examples and exercises from Rustan Leino's book external pageProgram Proofs

 

Key Publications

Acknowledgments

The Prusti project has been funded by the external pageSwiss National Science Foundationexternal pageFacebook, and external pageAmazon Web Services.

JavaScript has been disabled in your browser