Rust's type system ensures memory safety: well-typed Rust programs are guaranteed to not exhibit problems such as dangling pointers, data races, and unexpected side effects through aliased references. Ensuring correctness properties beyond memory safety, for instance, the guaranteed absence of assertion failures or more-general functional correctness, requires static program verification. For traditional system programming languages, formal verification is notoriously difficult and requires complex specifications and logics to reason about pointers, aliasing, and side effects on mutable state. This complexity is a major obstacle to the more-widespread verification of system software.
In this paper, we present a novel verification technique that leverages Rust's type system to greatly simplify the specification and verification of system software written in Rust. We analyse information from the Rust compiler and synthesise a corresponding <em>core proof</em> for the program in a flavour of separation logic tailored to automation. To verify correctness properties beyond memory safety, users can annotate Rust programs with specifications at the abstraction level of Rust expressions; our technique weaves them into the core proof to verify modularly whether these specifications hold. Crucially, our proofs are constructed and checked automatically without exposing the underlying formal logic, allowing users to work exclusively at the level of abstraction of the programming language. As such, our work enables a new kind of verification tool, with the potential to impact a wide audience and allow the Rust community to benefit from state-of-the-art verification techniques. We have implemented our techniques for a subset of Rust; our evaluation on several thousand functions from widely-used Rust crates demonstrates its effectiveness.
Wed 23 OctDisplayed time zone: Beirut change
11:00 - 12:30
|Modular Verification of Heap Reachability Properties in Separation Logic|
OOPSLALink to publication DOI Pre-print File Attached
|Modular Verification of Web Page Layout|
Pavel Panchekha University of Utah, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle, Shoaib Kamil AdobeDOI
|Modular Verification for Almost-Sure Termination of Probabilistic Programs|
Mingzhang Huang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Amir Kafshdar Goharshady IST AustriaDOI
|Leveraging Rust Types for Modular Specification and Verification|
Vytautas Astrauskas ETH Zurich, Switzerland, Peter Müller ETH Zurich, Federico Poli ETH Zurich, Switzerland, Alexander J. Summers ETH ZurichDOI Pre-print