PaperlayerView exact revision on arXiv

Source-linked AI summary

Verus: Verifying Rust Programs using Linear Ghost Types (extended version)

Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel

arXiv:2303.05491v2cs.LOcs.PL

TL;DR

Rust’s type safety does not by itself establish deeper functional correctness, especially for low-level and concurrent systems code. Verus addresses this gap with SMT-based verification expressed in Rust, using linear ghost permissions and a mode system, and demonstrates the approach on unsafe-use cases, interior mutability, and concurrency. Its formalization proves type safety and termination properties for the specification and proof modes, while important scope limitations remain for unsafe Rust and pointer modeling.

  • Problem

    Rust’s type safety does not prove deeper functional correctness properties, and low-level programming patterns can require unsafe code.

  • Method

    Verus combines SMT-based verification with Rust-expressed specifications and proofs, using linear ghost permissions and modes that distinguish specifications, proofs, and executable code.

  • Results

    Verus verifies examples involving pointer manipulation, interior mutability, and concurrency, and its formal model proves preservation, progress, and termination for specification and proof expressions.

  • Takeaways & Limitations

    Rust’s linearity and borrow checking can support SMT-based verification of tricky low-level and concurrent code through ghost permissions that impose no executable-code overhead.

  • Takeaways & Limitations

    Verus cannot reason about traditional Rust unsafe code and currently models raw pointers only for allocations in the global heap.

Abstract

from arXiv · show

The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing. We formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.

1 INTRODUCTION

Verus combines Rust’s linearity and borrowing with SMT-based verification to reason about low-level and concurrent code while distinguishing specifications, proofs, and executable programs. The paper presents linear ghost permissions, a mode system, formal metatheory, and examples covering unsafe-use cases and concurrency.

  • Motivation: Rust’s linear types and borrowing support type-safe, high-performance systems programming without garbage collection.These properties make Rust attractive for low-level software requiring high assurance.
  • Motivation: Formal verification extends Rust beyond type safety to prove deeper properties of low-level code and express safe alternatives to some unsafe patterns.The paper motivates SMT-based verification for structures such as doubly linked lists and concurrent reader-writer locks.
  • Core contributions: Linear ghost permissions represent evolving resource state and authorize operations such as writing to memory without adding compiled-code overhead.Because they are linear, permissions can be consumed and produced to track specific resources; because they are ghost, they exist only during checking and verification.
  • Core contributions: Verus uses Rust for specifications and proofs, applies linearity and borrow checking to proofs, and classifies code as specification, proof, or executable.Specification and proof code are checked for termination; proof and executable code are checked for linearity and borrowing; only executable code is compiled.
  • Examples and scope: Verus demonstrates verification of pointer-manipulating, interior-mutability, and concurrent Rust code, while its raw-pointer model is limited to pointers into global-heap allocations.The paper identifies separate crate verification and functions returning mutable references as missing features.
  • Formalization: The paper formalizes the mode system in a Rust-inspired lambda calculus and proves preservation, progress, and termination for specification and proof expressions.The termination result applies to specification and proof modes, while preservation and progress cover well-typed expressions.

2 VERUS BY EXAMPLE

Verus uses Rust-based specifications and proofs, SMT solving, and distinct modes to verify executable Rust while preserving linearity and borrowing checks where needed. Its example workflow combines contracts, loop invariants, inductive lemmas, and ghost state to reason about programs without compiling verification-only code.

  • Modes: Verus annotates Rust functions as executable, proof, or specification code, with each mode imposing different checking and compilation rules.Specification and proof code are checked for termination; proof and executable code are checked for linearity and borrowing; only executable code is compiled.
  • Modes: Verus expresses specifications and proofs in Rust, avoiding a separate verification language while retaining Rust features such as recursion, datatypes, modules, closures, and traits.Soundness requires restricting some features available to specifications and proofs.
  • Verification workflow: Preconditions, postconditions, and loop invariants generate verification conditions that Verus discharges with weakest-precondition reasoning and the Z3 SMT solver.When automation is insufficient, programmers provide recursive inductive proofs and explicit assertions as solver hints.
  • SMT encoding: Verus keeps SMT encodings lightweight by translating specification-function calls directly into SMT functions, requiring those functions to be total and contract-free.Because this removes early precondition feedback, recommends clauses provide soft-precondition warnings after verification errors.
  • Verification workflow: Verus requires recursive specification and proof functions to terminate through decreases clauses, while executable code may retain features such as infinite loops and side effects.Positivity restrictions on recursive types additionally prevent nontermination in specifications and proofs.
  • Linearity and borrowing: Rust’s borrow checker supplies linearity and borrowing guarantees that Verus trusts rather than rechecks in the SMT solver.Verus specifications are exempt from linearity and borrowing checks, allowing them to mention or copy linear values freely.
  • Linearity and borrowing: Proof variables are ghost yet linear, so they represent abstract permissions that can be produced and consumed to verify low-level operations without compiled overhead.Verus uses this mechanism as a safe replacement for some unsafe Rust features, including low-level pointer manipulation.

3 HANDLING UNSAFE CODE SAFELY

Verus handles selected unsafe-adjacent operations by encoding their correctness conditions as specifications checked by SMT verification. A vector-access example illustrates how a trusted unchecked operation can be given a bounds precondition, while the paper notes that more advanced examples follow.

  • Safety conditions: Unsafe Rust is conditionally memory-safe because correctness depends on obeying rules that the language cannot guarantee automatically.Verus targets strong guarantees for selected trusted primitives by making their correctness conditions explicit specifications.
  • Safety conditions: Verus encodes correctness conditions for trusted primitives as specifications, so verified contracts establish memory safety for those supported cases.This guarantee is conditional on the SMT proof showing that the code upholds the contracts.
  • Vector access: Vector indexing is memory-safe in Rust because bounds checks cause out-of-range access to panic, whereas get_unchecked omits the bounds check and is unsafe.The example exposes the missing safety condition as a Verus precondition.
  • Vector access: The safe_get_unchecked wrapper requires 0 <= i && i < v.len() before returning a reference into the vector.The unchecked operation is presented as a trusted primitive whose use is guarded by this specification.
  • Scope: The paper signals that subsequent sections extend the discussion beyond this simple vector-access example to more advanced cases.No further advanced-case result is stated in the supplied passage.

4 SAFE POINTER MANIPULATION WITH LINEAR GHOST TYPES

Verus uses linear ghost permissions to make unsafe pointer manipulation verifiable while preserving zero-cost executable abstractions. It applies this approach to cyclic doubly-linked lists through flattened permission state and sequence-based specifications.

  • Low-Level Pointer Manipulation with Linear Ghost Permissions: Verus introduces PPtr<T> as a zero-cost alternative to raw heap pointers, requiring linear ghost PermData<T> ownership for dereferences.The permission object tracks both the pointer association and the data behind the pointer.
  • Low-Level Pointer Manipulation with Linear Ghost Permissions: PPtr read and write operations update or return the value tracked by the associated permission object, while requiring pointer association and initialization conditions.The API specifications connect executable memory operations to ghost permission state.
  • Low-Level Pointer Manipulation with Linear Ghost Permissions: Consuming PermData<T> during deallocation prevents subsequent pointer reads through Rust’s linearity checking, blocking use-after-free in the verified API.The API’s safety also depends on prover-validated preconditions relating permissions to pointers.
  • Verified Example: Doubly-Linked List: A doubly-linked list uses ghost permissions for every node in a flattened structure, representing cyclic physical pointers while maintaining a verifiable ownership organization.Each permission maps a node pointer to its node contents and pointers.
  • Verified Example: Doubly-Linked List: The list API specifies operations through a view of the structure as a sequence, with well_formed requiring correct endpoints and permissions for every node.The specification abstracts away pointer manipulation while preserving the invariant needed by operations.

5 SUPPORTING INTERIOR MUTABILITY

Verus supports interior mutability by separating shared executable references from ghost state that represents or constrains mutable contents. Its libraries provide both permission-tracking and invariant-based strategies, including verified memoization with shared clients.

  • Supporting Interior Mutability: Interior mutability permits modifying a value through a shared reference, but unrestricted UnsafeCell use is not generally safe.Rust types such as Cell, RefCell, and RwLock impose different sharing or synchronization restrictions.
  • Supporting Interior Mutability: Because Verus models &T as immutable, Cell-like verification cannot encode mutable interior contents directly in the shared reference.The mutable interior must instead be represented or constrained through another verification mechanism.
  • Supporting Interior Mutability: Verus supports two strategies: linear ghost state can track cell contents, or reads can be modeled as nondeterministic values restricted by invariants.The strategies can be mixed through Verus primitives and verified libraries.
  • Supporting Interior Mutability: PCell is Verus’s permissioned alternative to UnsafeCell, using ghost permissions to track the cell’s interior value.Its API and specification are analogous to PPtr’s permission mechanism.
  • Supporting Interior Mutability: InvCell provides a Cell-like interface whose invariant must be proved for writes and may be assumed for reads.Its invariant can specify that the stored value is either absent or the correct memoized result.
  • Verified Example: Memoized Function Calls: Memoized computation uses InvCell to share a result store among multiple clients while returning a value satisfying the computation’s postcondition.The implementation reads an existing result or computes, stores, and returns a new one.
  • Supporting Interior Mutability: LocalInvariant<G> grants temporary exclusive ghost ownership when opened, while AtomicInvariant<G> supports thread-safe atomic-only openings.InvCell uses LocalInvariant because it is intended for single-threaded use, and nested openings are disallowed.

6 CONCURRENCY, USER-DEFINED LINEAR GHOST STATE, AND ATOMICS

Verus combines Rust’s ownership discipline with user-defined linear ghost state to verify concurrent protocols and atomic data structures. Localized transition systems expose protocol state and operations through proof-mode ghost APIs.

  • Concurrency and User-Defined Linear Ghost State: Rust ownership and memory safety support sound verification under multithreading, but fine-grained concurrency requires additional techniques.Verus addresses this need with user-defined ghost state and atomic invariants.
  • Concurrency and User-Defined Linear Ghost State: User-defined ghost state represents custom concurrent protocols as localized transition systems with thread-local views and state transitions.The resulting proof-mode ghost types expose operations whose requirements follow from inductive invariants.
  • Atomics: Verus verifies a concurrent FIFO ring-buffer queue by associating ghost head and tail state with atomic memory through AtomicInvariant.The construction models the evolution of FIFO state while connecting protocol permissions to atomic pointers.
  • Atomics: The consume_start API requires ghost evidence identifying the consumer thread and access to the tail-pointer state before performing the transition.Its proof-mode parameters encode protocol roles and resource access.
  • Concurrency and User-Defined Linear Ghost State: Supplementary examples include a string interner, a thread-safe reader-writer lock, and other single-threaded and multithreaded ghost-state uses.These examples demonstrate that user-defined ghost state is used beyond the FIFO queue.

7 IMPLEMENTATION

Verus is implemented as a compiler-integrated verification driver with additional Rust typechecking hooks. Its verified examples report specification, proof, and executable code sizes alongside verification times and employed features.

  • Implementation: Verus links a separate verification driver against a forked Rust compiler containing additional hooks and typechecking rules.Both the compiler fork and Verus are open source, and integration work targets further Rust language support.
  • Implementation: Table 1 reports spec, proof, and exec lines, verification time, and notable Verus features for each verified example.The full examples are available in supplementary materials, while paper figures show extracts.

8 USER EXPERIENCE AND ERROR REPORTING

Verus combines Rust’s borrow checking with SMT-based verification to provide precise feedback on both logical errors and invalid borrowing. Its user experience supports rapid iteration by identifying failed preconditions and rejecting aliased mutable references before SMT solving.

  • Verification workflow: Verus expresses executable functions with Rust-style preconditions and postconditions, allowing account transfers to be checked against balance specifications.The transfer example specifies sufficient source funds, destination bounds, and the resulting balances.
  • Borrowing errors: Rust’s borrow checker rejects passing the same account as both mutable arguments, so Verus does not invoke Z3 on the invalid aliased program.The rejected call produces an error for borrowing acct1 mutably more than once.
  • Verification workflow: A transfer of 20,000 from an account holding 10,000 fails verification because Verus reports the unsatisfied source-balance precondition at the call site.The diagnostic points to both the failed precondition and the offending invocation.
  • Verification workflow: Changing the transferred amount to 10,000 makes the account-transfer example verify successfully when Verus is rerun.
  • Borrowing errors: Unlike separate separation-logic tools, Verus relies on Rust’s ownership rules to associate memory-reasoning permissions implicitly with owned data.

9 LIMITATIONS

Verus has practical and design limitations around mutable borrows, unsafe code, and Rust’s type system. These boundaries constrain supported programs and some proof-structuring styles.

  • Borrowing support: Verus supports mutable borrows only for data passed as function arguments, not mutable references returned from functions or explicit right-hand-side borrows.
  • Unsafe code: Verus cannot reason about traditional Rust unsafe code because it relies on Rust’s borrow-checking rules rather than re-encoding ownership properties.This may limit applicability to systems that heavily use unsafe code, such as direct communication with memory-mapped devices.
  • Type-system dependence: Verus’s close dependence on Rust’s type system may preclude sophisticated proof-structuring styles available in dependent type systems such as Coq and F*.The limitation follows from Verus’s design choices rather than only from missing engineering support.

10 FORMALIZATION

The formalization models Verus’s modes, linearity, borrowing, ghost permissions, functions, and termination in a small Rust-inspired lambda calculus. It proves type safety and termination while deliberately omitting several full-language features.

  • 10 FORMALIZATION: The formalization targets Verus-specific type-safety features rather than modeling all Rust and Verus semantics.Its topic list includes modes, linear ghost permissions, borrowing, termination, and default values in specification code.
  • 10 FORMALIZATION: The model omits concurrency, verification-condition generation, and most location-based imperative semantics, while retaining permission-controlled loads and stores plus a tiny mutable heap.
  • 10 FORMALIZATION: Borrowing is represented through shared and linear usages attached to variable and expression typings, capturing immutable borrowing and borrowed linear ghost permissions.
  • 10 FORMALIZATION: Environment splitting shares nonlinear bindings across subexpressions while assigning each linear binding to one side and exposing a specification-mode view on the other.The sequencing rule temporarily treats selected bindings as shared before restoring them to linear status.
  • 10 FORMALIZATION: The model prohibits discarding linear resources but permits copying and dropping in specification mode, reflecting a simplified linear system rather than Rust’s affine dropping behavior.Rust’s Copy trait marks inherently nonlinear simple types as freely copyable.
  • 10.2 Functions and Lifetimes: Verus’s lambda-calculus model supports first-class specification functions and simple traits whose self methods can encode first-class functions.
  • 10.2 Functions and Lifetimes: Rust closures are modeled with callability modes distinguishing Fn functions callable many times from FnOnce functions callable only once and able to capture linear variables.
  • 10.4 Semantics and Type Safety: The formal semantics prove preservation, progress, and termination for specification and proof expressions, with termination established through a translation to CIC.Executable functions are erased in the termination proof, while permissions translate to values and the heap is erased.

11 RELATED WORK

Related work positions Verus among Rust verification tools by its use of Rust’s borrow checker and linear ghost permissions, while noting simplified pointer modeling and overlap with prior systems.

  • Verus is distinguished by leveraging Rust’s borrow checker to enforce linear ghost permissions.
  • Creusot uses Rust specifications and proofs, while Verus checks executable code and proofs through its own mode distinctions.
  • Prusti translates Rust into Viper and rechecks ownership, whereas Verus relies on memory safety enforced by Rust’s borrow checker.
  • Aeneas translates Rust into a purely functional F★ representation, unlike Verus’s Hoare-logic style with annotations on Rust code.
  • Verus’s pointer specification handles only pointers into global-allocator heap allocations, not stack variables, fields, references, or pointer provenance.
  • Verus permissions are program-level values combined in datatypes, simplifying verification-condition generation for SMT solvers compared with separation logic’s separating conjunction.

Well-typed expression (main rules, continued)

The formal rules type-check expressions by combining permissions and environments, tracking modes and usage, and enforcing restrictions on executable, proof, and specification code.

  • Constructor rules type-check each argument under separate permissions and environments, then combine them with # for the enclosing expression.
  • Function rules constrain argument and body modes, callability, lifetimes, and linearity when typing applications and function bodies.
  • Specification functions are checked in spec mode with unrestricted permissions and environments, separating them from linear executable and proof contexts.
  • Strict evaluation requires an executable, linear heap and a static lifetime, while well-typed configurations combine heap and expression judgments.
  • The model assigns default values to int, Unit, and Never, and recursively constructs defaults for structs from their field defaults.
  • The formal development draws on linear ghost capabilities and SMT solving to represent changing state while keeping permissions convenient for verification.

12 CONCLUSIONS

Verus uses Rust’s linearity and borrow checking to express ghost permissions for difficult low-level and concurrent code. The authors conclude that Rust itself is a valuable tool for verifying Rust programs.

  • Verus uses Rust’s linearity and borrow checking to express linear ghost permissions for tricky low-level and concurrent code.
  • Rust’s type safety and aliasing control also let Verus treat code more like functional code when generating verification conditions.
  • The authors conclude that Rust itself is among the most valuable tools for verifying Rust code.
Loading 2303.05491v2…