Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming

Project Scope and Objective

• The "Rust Belt" project at the MPI for Software Systems applies decades of academic work on logical foundations to the actively developed programming language Rust.
• The primary goal is to establish formal logical foundations to verify that Rust's safety guarantees (type safety, memory safety, and data race freedom) hold in the presence of "unsafe" code.
• The project aims to provide verification tools that allow Rust developers to safely evolve the language and its standard libraries in the future.

The Rust Safety Challenge

• Rust addresses the historical trade-off between high-level safety and low-level control by preventing the unrestricted combination of mutation and aliasing, the root cause of errors like use-after-free and data races.
• The language uses an ownership type system where an object cannot be both mutable and aliased at the same time; it allows either multiple shared immutable references or a single unique mutable reference.
• Limitation of Core Discipline: The core type system cannot inherently support widely used data structures (e.g., doubly linked lists) or synchronization primitives (e.g., locks, reference counting) which require mutation of shared state.
• Solution via Encapsulation: Rust libraries (e.g., Arc, Mutex) are implemented using unsafe blocks that perform raw pointer manipulation but are wrapped in safe APIs that guarantee clients cannot trigger undefined behavior.
• Real-World Risk: A 2015 bug in the scoped_threads API, developed alongside reference counting (Rc), revealed that combining safe-looking APIs could result in use-after-free errors, highlighting the need for formal verification of these unsafe implementations.

Verification Methodology

• The project rejects "syntactic safety" (progress and preservation) because it fails when unsafe code is present; syntactic rules cannot validate code outside the "safe fragment."
• Instead, the project employs "semantic safety," defined observationally: an API is safe if no well-typed program can observe undefined behavior (e.g., out-of-bounds memory access or data races) by interacting with it.
• Framework Structure:
  • A semantic model maps API interfaces to verification conditions (safety contracts).
  • Safe Fragment Proofs: Proved once and for all that code written strictly in the safe fragment satisfies its safety contract by construction.
  • Unsafe Library Proofs: Manually verified that specific unsafe implementations (e.g., Arc, Mutex) satisfy their corresponding safety contracts within the semantic model.
• Modularity: The model ensures that different libraries can be verified independently; if a combination of libraries (like the deprecated scoped_threads and Rc) is unsafe, the proof for the offending component fails without requiring re-verification of unrelated components.
• Tooling: All proofs are mechanized in the Coq proof assistant, which facilitates evolving the semantic model as new, more complex APIs are discovered.
• Bug Discovery: The verification process has identified a few bugs, including one in the Mutex API and an issue regarding relaxed memory ordering in the Arc API.

Logical Foundations: Separation Logic and Iris

• The project utilizes a derivative of Separation Logic because its primitive notion of "ownership" aligns naturally with Rust's ownership type system.
• Problems with Existing Logics: Traditional Concurrent Separation Logic (CSL) cannot express complex protocol behaviors (e.g., temporal state changes, role switching) without requiring bespoke, non-composable logics with complex, custom soundness proofs.
• The Iris Framework:
  • Iris is a unifying framework that allows the derivation of advanced reasoning principles (e.g., "borrow propositions" for temporary ownership) from two core features: standard invariants and user-defined ghost state (logical state independent of physical memory).
  • This framework allows the project to define logical predicates (e.g., "arc of x") that represent permissions rather than physical memory ownership, enabling the verification of shared mutable state.
• Mechanization: The soundness of custom axioms (e.g., for reference counting logic) is derived within Iris using algebraic structures (Partial Commutative Monoids) rather than being baked into the logic itself.

Memory Models and Future Work

• The initial verification was performed against a sequentially consistent memory model.
• Ongoing work addresses the need for a realistic memory model supporting relaxed atomic operations (C++ style), which are essential for high-performance concurrent code but difficult to model.
• The team is adapting the Iris framework to accommodate more aggressive memory models required for modern compiler optimizations while maintaining formal guarantees.