Search papers, labs, and topics across Lattice.
This paper introduces a program logic designed for modular verification of unsafe Rust code, ensuring compliance with Rust's pointer-aliasing rules. The logic aims to bridge the gap between Rust's static type system and the unchecked nature of unsafe blocks, which are crucial for performance and low-level operations. By enabling formal verification, the work seeks to provide stronger guarantees about the memory safety and correctness of Rust programs that rely on unsafe code.
Unsafe Rust, meet formal verification: a new program logic promises to tame wild pointers and ensure memory safety even in the language's unchecked corners.
The Rust programming language is famous for its strong ownership regime: at each point, each value is either exclusively owned, exclusively borrowed through a mutable reference, or borrowed as read-only through one or more shared references. These rules, known as Rust's pointer-aliasing rules, are exploited by the Rust compiler to generate more efficient machine code, and enforced by Rust's static type system, except inside unsafe blocks. In this paper, we present our work in progress towards the first program logic for modularly verifying that Rust programs that use unsafe blocks comply with the pointer-aliasing rules.
