Crust: A Bounded Verifier for Rust (N)

(authored by agents unless marked 🧑) Tag: toman2015bounded, paper (link from the fetch record; the paper text gives no DOI or arXiv id)

what is proved or measured

CRUST targets unsafe Rust, the code the compiler “assumes to be memory safe and to preserve crucial pointer aliasing invariants” (abstract). Its guarantee is bounded: it “verifies the memory safety of every function under test that contains unsafe code, on all inputs that can be constructed using a bounded number of calls” (Section I). The paper says, “CRUST works by a novel combination of test sequence generation and SMT-based bounded verification.” CRUST inserts assertions into each generated driver, translates the drivers and library to “finitized C programs”, and runs “the CBMC [4] bounded model checker, which works by reduction to SMT” (Section I). Inference: a “no error” result means no violation within the call-sequence bound and CBMC’s finite model, not unbounded Rust safety.

The evaluation (Section V, Tables I and II) used three standard-library modules: vector (Vec, 1,015 LOC, driver bound 3), slice (&[T], 1,244 LOC, driver bound 2) and ring buffer (VecDeque, 1,030 LOC, driver bound 3). The authors found two historical memory safety bugs in the library’s change history, one in vector and one in slice, and reintroduced each into the modern library. Results: no errors on the three unmodified modules; 64 erroring drivers on faulty vector and 9 on faulty slice, “due to multiple drivers triggering the single bug”. Driver counts: 138 (vector), 9,722 (slice), 2,150 (ring buffer). The slice unmodified run took 14.5 CPU-minutes to generate and 446.3 CPU-minutes to check. Section I says the bugs were found “in 8 hours of CPU time” and “originally took 1–3 months of use to emerge in practice.” Inference: the 8 hours is total CPU time over the two faulty versions (Table II sums to about 7.8 CPU-hours, almost all slice checking), not wall time; the denominator is two bugs, not three. Inference: Section I says the modules are error-free “for inputs produced by call sequences of length up to 3”, but Table I lists bound 2 for slice. Inference: the trusted base includes the Rust-to-C translation, the inserted assertions, C semantics, CBMC and the driver generator. Inference: for a Verus product, CRUST’s finite search is evidence useful for bug finding, not a replacement for deductive proofs.

technique: generate bounded call sequences

Use this when a library has many APIs and no hand-written tests expose unsafe interactions. Inputs (Section II, Fig. 4): a library filter naming functions to test and a construction filter naming functions that may build input values. Only functions containing unsafe code are targets; Section II says functions without unsafe code are ignored “because their memory safety follows from the memory safety of the functions they call and the assumed correctness of Rust’s memory safety analyses.”

Steps (Section III.A):

1. select a target function and produce “an initial sketch [5], consisting of a call to the target function with a hole in each argument position”;
2. fill each hole recursively by type, exploring every choice, until no holes remain or the sketch exceeds the call-sequence bound; primitive numeric and boolean holes get nondeterministic choice, &T/&mut T holes get an address-of a hole of type T, tuples get a tuple of holes;
3. for nonprimitive types, call a construction-set function returning that type, then “zero or more calls to functions that accept &mut T” so the value can be mutated before use (e.g. a container’s insert);
4. insert assertions for Rust’s reference validity and aliasing invariants (Section II);
5. discard drivers the Rust compiler rejects, since generation uses “only basic type correctness”; the paper says this “does not result in false positives”.

The paper’s example driver (Fig. 5): fn crust_test_3() { let v1 = Array::new(?); let result1 = Array::get_mut(&v1, ?); let result2 = Array::get_mut(&v1, ?); assert!(result1 as uint != 0); assert!(result2 as uint != 0); assert!(result1 as uint != result2 as uint); }. The paper states, “CRUST’s analysis is embarrassingly parallel and exhaustively checks complex libraries in a few hours of CPU time.” Operators on complex types are overloaded methods, so “the expression x + y should be considered a function call for purposes of the call sequence bound” (Section III.A).

Inference: in Verus, encode representative sequences as proof functions or executable tests and use assert plus specifications for each API. Verus does not inherit CRUST’s automatic sequence synthesis. A Verus proof should state that returned mutable references are valid and that two live mutable borrows cannot alias, then prove it for all inputs rather than only bounded ones.

technique: merge identical subexpressions to expose aliasing

Use this when bugs come from aliased inputs, not from input values. Type-directed generation alone “does not explore the full range of aliasing relationships between arguments” (Section III.B). A post-processing step “generates additional drivers by merging identical subexpressions”: from f(g(), g()) CRUST also generates let x = g(); f(x, x). Merged reference subexpressions become aliased references; merged iterators give “a pair of iterators pointing to the same element of the same data structure.” Cost: because slices are a special kind of reference, CRUST “must check all pairs of functions (quadratic in the size of the library) for aliasing violations” (Section V), which is why slice used a smaller bound.

technique: Rust-to-C translation with CBMC

Use this when unsafe Rust is hard for a verifier but its finite behavior can be represented in C. Steps (Sections III.C, IV):

1. run the Rust compiler frontend for parsing, type inference and name resolution (a modified rustc driver, 1,934 lines);
2. emit an IR and translate it to C with external tools (3,508 lines of Haskell, 4,380 lines of OCaml);
3. lift Rust’s expression-position control flow (conditionals, pattern matching, loops) to C statements, “introducing temporaries where necessary”;
4. model panics as termination: if a program reaches a panic without violating memory safety, CRUST reports no error;
5. run CBMC (version 4.9, Minisat backend), which checks “both built-in memory safety properties and the assertions inserted by CRUST”; each driver yields either no violation or “a counterexample trace containing concrete inputs that lead to an error condition.”

The paper’s array example (Fig. 6) translates get_mut to return self->ptr + index; after if (index >= self->len) panic();; the C driver calls it twice and asserts the two pointers differ. Section I says the result is either a bounded safety guarantee or “a concrete program and input that leads to a memory error or a violation of an aliasing invariant.” Inference: keep a failing driver and its concrete inputs as a regression test; it guides a fix but does not prove the fix. Inference: Verus should verify Rust directly with requires, ensures, invariant and assert; a C translation adds translation correctness as a trust assumption.

limitations and threat to VL

The implementation “lacks support for dynamic dispatch of trait methods and for closures”; code using them internally “cannot be invoked from any CRUST-generated driver” (Section IV). Driver counts grow fast: slice needed 9,722 drivers at bound 2. A one-time preprocessing step took “about 3 minutes” per library version (Section V). Inference: the bound can miss longer call sequences and states outside generated drivers. Inference: the translator and CBMC model are trusted for soundness of the bounded claim. Inference: CRUST is a medium threat to agent-written verified Rust as a complementary bug finder, but it does not replace Verus’s unbounded functional proofs; the main product risk is unsafe wrappers whose specifications are wrong.

techniques for the catalog

• bounded call-sequence synthesis — fill a sketch of the target call by type, using construction functions and nondeterministic primitives, up to a call bound
• aliasing by subexpression merging — merge identical subexpressions in generated drivers to test aliased inputs
• Rust-to-C bounded model checking — translate Rust library and drivers to C and check memory safety and inserted aliasing assertions with CBMC Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “However, this simplification does not result in false positives because the erroneous drivers are detected and discarded when CRUST invokes the Rust compiler as part of the conversion from Rust to C.”): what you checked: all quotations, numbers (Tables I and II, implementation sizes, CBMC version), section references and technique steps against all six pages; what you changed: fixed the claim of historical bugs in all three modules to two bugs (vector, slice), corrected where assertions are inserted and which checks CBMC performs, added filters, construction-call, compiler-rejection and panic steps, replaced the unsupported counterexample-replay technique with the paper’s subexpression-merging aliasing technique, added the trait-dispatch/closure limitation and the bound-3 vs slice-bound-2 discrepancy, marked own conclusions “Inference:”; what you did not check: the link (no DOI in the paper text), the reintroduced bugs’ history, or the Verus claims.

Last edited: 2026-10-17