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 page Rust 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 page GitHub and can be used via the external page "Prusti Assistant" extension for Visual Studio Code.

Project Members

Aurel Bílý
Jonas Fiala
external page Jasper Geer (UBC)
external page Zack Grannan (UBC)
external page Christoph Matheja (DTU Copenhagen)
Peter Müller
external page Alex Summers (UBC)

Links

external page Prusti User Guide
external page GitHub repository
external page Zulip channel
Prusti versions of the examples and exercises from Rustan Leino's book external page Program Proofs

 

Key Publications

  • V. Astrauskas, A. Bílý, J. Fiala, Z. Grannan, C. Matheja, P. Müller, F. Poli, and A. J. Summers: The Prusti Project: Formal Verification for Rust (invited)
    NASA Formal Methods (14th International Symposium), 2022. [Download PDF][BIB][external page Publisher]
  • F. Wolff, A. Bílý, C. Matheja, P. Müller, and A. J. Summers: Modular Specification and Verification of Closures in Rust
    Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2021 [Download PDF][BIB][external page Publisher][external page Talk]
  • V. Astrauskas, C. Matheja, P. Müller, F. Poli, and A. J. Summers: How Do Programmers Use Unsafe Rust?
    Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2020. [Download PDF][BIB][external page Publisher][external page Talk]
  • V. Astrauskas and P. Müller and F. Poli and A. J. Summers: Leveraging Rust Types for Modular Specification and Verification
    Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2019. [Download PDF][BIB][external page Publisher][external page Talk]
  • V. Astrauskas and P. Müller and F. Poli and A. J. Summers, Leveraging Rust Types for Modular Specification and Verification
    Technical Report, ETH Research Collection
    , 2019. [Download PDF][BIB][external page ETH Collection]

Acknowledgments

The Prusti project has been funded by the external page Swiss National Science Foundationexternal page Facebook, and external page Amazon Web Services.