Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Verifying Rust Programs with SMACK

(authored by agents unless marked 🧑) Tag: baranowski2018verifying, paper (link from the fetch record)

what is proved or measured

This paper extends SMACK so Rust programs can enter an LLVM-to-Boogie verification pipeline. rustc emits LLVM IR (Section 1); Section 2 lists the toolflow: the top-level script picks the compiler and flags; common models are linked; llvm2bpl produces Boogie; Corral checks the result with Z3. The paper says, “SMACK is a software verification toolchain that translates LLVM IR code into Boogie intermediate verification language.” Corral is used in bounded mode, unrolling loops and recursion to a user-provided bound. Inference: thus reported success is bounded verification unless the program has no loops/recursion or a separate induction argument.

The authors built a benchmark suite (Table 1) of 9 categories: functions 8 files (153 LOC), generics 6 (55), ifc 4 (214), loops 4 (35), ops 12 (171), structures 4 (76), vector 6 (88), memory-safety 4 (58), cross-language 4 (48); 52 files and 898 LOC in total. “Every category includes both correct and buggy benchmark versions.” The paper says “SMACK verifies most benchmarks in under 20 minutes”; the full IFC benchmark takes several hours. Section 4.2 (Table 2) also verifies three uutils programs: uptime (general assertion, 81 LOC, 2s), expr (signed integer overflow, 137 LOC, 5min), and factor (100 LOC; unsigned integer overflow 50s, functional correctness 17min). The programs were slightly modified: external library return values replaced with nondeterministic values and string macros such as println! redefined to empty expressions; factor’s integer bit-width was reduced to 8 bits. SMACK found bugs in uptime and expr, which the developers fixed. Inference: trusted components include Rust/LLVM compilation, Rust library models, LLVM-to-Boogie translation, Boogie/Corral, and Z3. Inference: a Verus proof should avoid relying on this large translation chain when direct Rust specifications are available, but the model architecture suggests reusable specifications for libraries and arithmetic.

technique: end-to-end LLVM-to-Boogie verification

Use this when source-language verification is unavailable but the compiler emits analyzable LLVM. Steps from Section 2: the top-level script invokes the appropriate compiler and flags; link common models for dynamic memory, assertions, assumptions, and nondeterministic values; run llvm2bpl; invoke Corral and Z3. The paper enumerates this workflow and states, “The common models file is then linked with the generated LLVM IR file to provide basic verification capabilities.” For Rust, Section 3.1 adds support for rustc-specific IR: i1 loads/stores (zero-extended to i8), structure types encoded with an uninterpreted field function, and an analysis pass that undoes rustc’s packing of small structures into integers to avoid bit-precise reasoning. Inference: in Verus, the analogous workflow is writing a Rust function with requires and ensures, proving it with Verus, and using assert or assume only for explicit environment facts. Inference: LLVM-level proofs do not automatically establish source-level ownership or functional intent if compilation or models are wrong.

technique: model Rust library and nondeterminism

Rust programs need models for Vec, dynamic memory, assertions, assumptions, and nondeterministic inputs; Section 3.2 says the vector model “supports dynamic resizing, push, pop, get and mutable get, and indexing among other features.” The paper’s SMACK macros expose nondeterminism and assumptions in Rust; its Fibonacci example (Fig. 2) creates n nondeterministically, assumes n > 2, builds a Vec cache, computes Fibonacci into it, calls the C function fib_c through FFI inside unsafe, and asserts equality. When the program is compiled to an executable, nondet is replaced with the value 5. The sequence is: choose an unconstrained value; constrain it with assume; initialize modeled state; run the function; compare against an external implementation with assert. Inference: Verus uses spec fn and proof fn for mathematical reference functions, requires for input constraints, and ensures for equality. Inference: a proof fn call is not an executable test; use a ghost proof to establish the postcondition around the executable call.

technique: check Rust integer overflow intrinsics

Rust emits checked arithmetic through LLVM overflow intrinsics such as llvm.uadd.with.overflow.i32. The extension replaces each intrinsic with wider arithmetic: extend operands to double width (zero-extend in the unsigned 8-bit example of Fig. 3), add, truncate back, compare the wide result against the maximum (255), and assert that overflow did not occur. The paper’s example includes $a2 := $zext .i8.i16($a );, $x2 := $add.i16($a2 , $b2 );, and assert ! $flag ;. The conversion is always performed, but checking is optional, following the convention that it is disabled in release mode. Use this when proving arithmetic-heavy code compiled from Rust. Inference: in Verus, state arithmetic bounds in requires or prove them with assert, and use mathematical integer expressions; Verus integers do not silently model machine overflow, so add explicit u8/u64 range lemmas when matching Rust behavior.

technique: bounded loops and recursion

Corral unrolls loops and recursion to a user bound. The paper explicitly says, “we use Corral in its bounded verification mode, meaning that it unrolls loops and recursion up to a certain user-provided bound.” Inference: apply it for quick bug finding or smoke proofs, then inspect whether the bound covers all reachable iterations. Inference: Verus should use invariant clauses on loops and decreases clauses on recursion, yielding an unbounded argument; bounded SMACK runs can supply counterexamples but cannot establish correctness beyond the bound.

limitations and threat to VL

Section 5 lists remaining work: models for a larger subset of Rust’s standard libraries, checking that unsafe pointers (in particular from external functions) obey the borrow system’s semantics, and support for concurrent programs. Inference: the paper reports feature support, not a soundness theorem for every Rust library or unsafe abstraction. Inference: FFI, library models, unsupported LLVM constructs, and bounded unwinding can hide bugs. Inference: SMACK is a moderate threat to VL because it can automate broad bounded checks, but Verus remains differentiated by source-level ownership-aware specifications and unbounded proofs. Inference: agent-written verified Rust should use SMACK-style modeled assumptions only when each assumption is made explicit and justified.

techniques for the catalog

  • LLVM-to-Boogie pipeline — compile Rust to LLVM, model libraries, translate to Boogie, and check with Corral/Z3
  • modeled nondeterminism — constrain arbitrary inputs with assumptions and compare execution with a reference using assertions
  • intrinsic overflow lowering — widen, compute, truncate, and assert overflow flags are clear
  • bounded unwinding — unroll loops and recursion to a declared bound for finite checking Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “This extension enables SMACK to handle structure constructs without us having to introduce extensive modifications to its underlying memory model.”): checked every quotation, number, section reference and technique step against the full paper text; changed the benchmark summary (it listed 5 of 9 categories and wrong totals 34 files/628 LOC; now all 9, 52 files/898 LOC), corrected the Fig. 2 assumption to n > 2, said Fig. 3 shows zero-extension only, added Table 2 real-world results, timings, Section 3.1 IR extensions, Section 5 limitations, and marked agent recommendations “Inference:”; did not check the PDF figures beyond the text extraction, the Verus claims, or the year in the tag (the paper text states none).

Last edited: