Reasoning about Interior Mutability in Rust using Library-Defined Capabilities

TL;DR

This paper introduces Mendel, a novel verification technique for safe Rust code with interior mutability, using library-defined capabilities and annotations to automatically verify real-world programs involving complex mutable types.

Contribution

It presents the first automated verification method for interior mutability in Rust, leveraging implicit capabilities and new annotations to handle existing library types.

Findings

Successfully verified Rust programs using standard interior mutable types.

Required zero client-side annotations in many verified programs.

Demonstrated effectiveness on real-world Rust libraries.

Abstract

Existing automated verification techniques for safe Rust code rely on the strong type-system properties to reason about programs, especially to deduce which memory locations do not change (i.e., are framed) across function calls. However, these type guarantees do not hold in the presence of interior mutability (e.g., when interacting with any concurrent data structure). As a consequence, existing verification techniques for safe code such as Prusti and Creusot are either unsound or fundamentally incomplete if applied to this setting. In this work, we present the first technique capable of automatically verifying safe clients of existing interiorly mutable types. At the core of our approach, we identify a novel notion of implicit capabilities: library-defined properties that cannot be expressed using Rust's types. We propose new annotations to specify these capabilities and a first-order logic encoding suitable for program verification. We have implemented our technique in a verifier called Mendel and used it to prove absence of panics in Rust programs that make use of popular standard-library types with interior mutability, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex and RwLock. Our evaluation shows that these library annotations are useful for verifying usages of real-world libraries, and powerful enough to require zero client-side annotations in many of the verified programs.