Abstract:
Low-level, pointer-manipulating programs are tricky to write and devilishly hard to verify, requiring complex spatial program logics to reason about heap updates. Recent systems like Prusti and Creusot take advantage of Rust ownership mechanisms to shield the programmer from some spatial assertions, allowing them to only write pure, first-order logic specifications which can be automatically verified by a solver. Even with these advances, verification remains unpleasant. For instance, when working over collections, program-logic based methods require the use of loop invariants that are universally quantified to account for the potentially unbounded contents of the collection. Such invariants often require a sophisticated understanding of the underlying spatial program logic, and worse, the quantification makes them difficult to synthesize.
This talk presents Flux, a refinement type checker for Rust that shows how logical refinements can work in tandem with Rust’s ownership mechanisms to yield ergonomic type-based verification. First, we describe how Flux extends Rust’s type system with logical refinements that can be used to specify properties about data. Next, we demonstrate how the combination of refinements and Rust’s ownership mechanisms allows the specification and verification of imperative code.
To showcase how the interaction between refinement and ownership types enables ergonomic verification, we describe a simple but powerful refined API for vectors that uses polymorphism to track quantified assertions about their elements. Using this API, we demonstrate how Flux can be used to verify lightweight properties in a suite of vector-manipulating programs and parts of a verified sandboxing library. We use these examples to compare how, when specifications are encoded as types, refinement inference makes verification more ergonomic and efficient relative to program-logic based techniques.
Bio:
Nico Lehmann is a Ph.D. student in the ProgSys group at UCSD, supervised by Ranjit Jhala. His current research focuses on integrating refinement types into the Rust programming language with the broader goal of bringing expressive typing disciplines into mainstream programming. Nico holds a master’s degree from the University of Chile.
Galois was pleased to host this tech talk for the public on May 17, 2023. See above for the recording of this presentation.