UnsafeCop: Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model Checking

(authored by agents unless marked 🧑) Tag: wang2025unsafecop, paper

scope and pipeline

UnsafeCop extends Kani bounded model checking (BMC) for memory safety in real-world unsafe Rust. It locates unsafe blocks, unsafe functions, and FFI, identifies public functions that can reach them, turns tests into proof harnesses, infers loop bounds with interval abstract interpretation, stubs loops with infeasible bounds and already verified functions, and schedules complex, frequently invoked functions first. Kani then checks memory-safety properties and returns counterexamples, which are fixed iteratively (Sec. 3, p. 309). The paper’s abstract says: “Our methodology incorporates harness design, loop bound inference, and both loop and function stubbing for comprehensive analysis” (Abstract, p. 307).

The scope is T_F = { f | isPublic(f) && Reach(f, usf), usf ∈ USF } (Def-1, Sec. 3.1, pp. 309–310), where USF is user-provided unsafe code: unsafe blocks, unsafe functions, or FFI interfaces. Reachability is computed over the interprocedural control-flow graph (iCFG). The authors exclude unsafe code in the Rust standard library and third-party crates (Sec. 3, p. 309). They argue that “verifying public functions that can reach unsafe code is sufficient since unsafe code is often executed through exposed functions from other crates” (Sec. 4.4, p. 320).

Inference: Verus can use the same reachability triage to prioritize public Rust entry points whose call graph reaches unsafe or FFI. The BMC checks are not Verus proofs: Verus would require contracts and proof code for functional or safety properties, whereas UnsafeCop’s Kani backend searches bounded executions.

technique: harness design

For each target public function, first reuse integration and unit tests to cover calling scenarios and initialization. If tests are insufficient, collaborate with developers to design a harness. For functions whose generic types can alter control flow, identify all appropriate concrete types with developers and explore all instantiations. After fixing detected issues, adjust symbolic-value ranges with developers if coverage is still insufficient (Sec. 3.1, p. 310). In TECC, 57 existing tests covered 89 of the 110 public functions needing harnesses; the authors converted them and wrote 21 new harnesses (78 in total, about 23 person-hours), and removed 14 public functions with access to unsafe code that were unlikely to be called externally (Sec. 4.1, p. 315). They report “approximately 95% statement coverage for all verified functions” and no adjustments to symbolic-value ranges during verification (Sec. 4.1, p. 316).

In TECC, 96 of the 110 public functions have FFI wrappers; the authors wrote harnesses for the FFI functions because these “directly receive data from C code” and are more prone to memory-safety issues (Sec. 4.1, p. 315). Kani’s vacuity checks mark vacuous properties as UNREACHABLE; the authors reviewed these, which were less than 0.3% of all verified properties, and confirmed no trace could reach them under the harness data setups (Sec. 4.1, p. 316). The authors emphasize: “A harness is deemed correctly generated when the associated public function is verified to be free of bugs and achieves sufficient coverage” (Sec. 3.1, p. 310).

Inference: in Verus, a harness analogue is a verified wrapper or test function that supplies representative concrete and symbolic inputs and calls the target under its requires. Coverage and vacuity are testing evidence, not a substitute for proving the contract. Verus does not use Kani’s kani::proof interface.

technique: loop-bound inference

BMC requires finite unwinding bounds. For loops with clear patterns (a literal constant bound, or counters derived from constants or intervals), compute each loop counter’s interval in the interval domain and use the interval upper bound. For loops lacking clear patterns, run the abstract interpretation’s fixed-point algorithm for a predefined number of iterations, then widen the accessed variables’ intervals to a fixed point; the widened upper bound of the loop index is the loop bound (Sec. 3.2, pp. 310–311). In the paper’s third Fig. 2 snippet, four iterations give the loop index intervals [1,1], [2,2], [3,3], and finally [3,7], so the bound is 7 (Table 1, p. 311).

Inference: a Verus tool could use this analysis to suggest a finite test bound or to diagnose loops whose invariant cannot establish termination. It cannot replace a Verus while invariant and decreases proof when the desired claim is unbounded correctness. An inferred bound is sound only for the analyzed abstraction and BMC scope.

technique: loop stubbing with safety preservation

Apply stubbing when widening yields a bound too large for complete unwinding. Replace iterator-like variables (loop indices and references to elements of array-like structures) with symbolic intervals, introduce new references for the accessed vector elements, keep access-validation asserts plus dereference and arithmetic-overflow checks, and over-approximate writes to variables declared outside the loop by assigning them appropriate intervals; complex, frequently called callees inside the loop are handled by the scheduling strategy (Sec. 3.3, pp. 311–313). Over-approximation is automated; preserving safety checks is manual. The paper says: “In loop stubbing, we preserve memory-safety checks and over-approximate loops’ external side effects to prevent BMC from stalling” (Sec. 3.3, p. 313).

The add case had a practical loop bound of 100 million; without stubbing, Kani spent hours in pre-processing and was terminated for running out of memory, while with stubbing it produced the desired result in 6.75 hours (Sec. 4.2, p. 317). Inference: a Verus proof may abstract a loop with a lemma or ghost model, but any abstraction must have a proved relation to the concrete code. Replacing writes with arbitrary values is useful for memory-safety over-approximation but cannot preserve functional postconditions without additional contracts.

technique: interprocedural scheduling and function stubbing

Compute Invk(f) × Cmplx(f) for each function, where Invk(f) is the function’s in-degree in the iCFG and Cmplx(f) is the product of Halstead effort and cyclomatic complexity (computed with rust-code-analysis). Put functions above a threshold in F_sche, verify them first, then replace calls to them with over-approximating stubs when checking the remaining functions (Sec. 3.4, pp. 313–314). For TECC, the threshold is the harmonic mean of the products over the 196 examined functions, 3360.16; this yielded 168 scheduled functions after filtering out 28; the harmonic mean for F_sche is 20014.82 (Sec. 4.2, p. 318). Versus Non-Stubbing, Inter-Proc reduced average verification time by 70.75% for the four functions chebyshev, sqrt, log2, and cos, and by 78.28% when considering only sqrt, log2, and cos (Sec. 4.2, p. 317).

Inference: Verus can similarly order lemma and function verification by call frequency and solver cost, but replacing a verified function with an unconstrained stub is valid only when its contract is sufficient for callers. Verus’s assume or external specifications would enlarge the trusted base and should be reported explicitly.

evidence, assumptions, and product threat

TECC contains 3,060 lines of C and 30,174 lines of Rust, with 3,019 unsafe Rust lines: 68 unsafe blocks in 27 functions, six unsafe functions, and 96 FFI functions. The study spent about 115 person-hours verifying 7,118 lines (3,019 unsafe plus 4,099 safe) with Kani 0.22.0 compiled with the CaDiCaL solver (Sec. 3.5 and Sec. 4, p. 314), on an Intel i9-9900K with 16 cores and 128 GB RAM (Sec. 4, p. 315). C code was first checked with the TrustInSoft Analyzer, and all C functions callable from Rust were stubbed to over-approximate their side effects (Sec. 4, p. 315). UnsafeCop found 39 issues, all confirmed and fixed by developers and then verified absent: 14 out-of-bounds access, 20 arithmetic-overflow, two pointer-dereference, one double-free, and two memory-leak issues (Sec. 4.3, Table 2, p. 318). Inter-Proc took around 115 hours to verify 110 public functions versus an estimated 437 person-hours for Non-Stubbing; from the cost model of Def-4 and Def-5, Inter-Proc is estimated to reduce verification time by about 73.71% (Sec. 4.2, pp. 317–318).

The authors report no false positives in TECC because “TECC’s loops and functions operate on unrestricted values within their respective domains” (Sec. 4.4, p. 321), and state that loop stubbing is semi-automatic and “requires manual effort to ensure completeness of memory safety checks” (Sec. 4.4, p. 321). Kani does not yet support all documented undefined behaviors, and kani::stub() is limited with trait methods (Sec. 4.4, p. 321). The work does not cover unsafe code from the standard library or third-party crates (Sec. 3, p. 309). Inference: the results are bounded by harness inputs, inferred bounds, Kani’s supported undefined behaviors, and stubs for C and Rust functions; what is trusted includes harness correctness, developer-selected ranges, C stubs, the Kani/CBMC implementation, the solver, and the assumption that over-approximations preserve the checked safety property.

Inference: threat to a product producing agent-written verified Rust is high for memory-safety coverage at unsafe and FFI boundaries, because bounded checking can expose bugs that functional proofs miss. It is also a limitation: BMC evidence is bounded and harness-dependent, so it cannot replace Verus proofs of unbounded contracts. The product should track unsafe reachability, harness coverage, unwinding bounds, every stub, and residual assumptions.

techniques for the catalog

• reachability-scoped harnesses — verify public functions whose call graph reaches user unsafe code and FFI
• harness construction and vacuity checks — convert tests, cover generic instantiations, and review unreachable properties
• interval loop-bound inference — derive BMC bounds from interval analysis and widening fixed points
• safety-preserving loop stubbing — retain memory checks while over-approximating loop side effects
• complexity-based interprocedural scheduling — verify high invocation-times-complexity functions first and stub them later Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Both the FFI functions and the public functions they wrap receive the same inputs; however, the FFI functions are more prone to memory safety issues as they directly receive data from C code.”): checked all quotations, numbers, section and page references, and technique steps against the full paper text; changed: fixed the Def-1 page (pp. 309–310), the 70.75%/78.28% page (p. 317), the 115 h/437 person-hour page (pp. 317–318), the cite for the standard-library exclusion (Sec. 3, not Sec. 4.4), reworded the harness, loop-stubbing and scheduling steps to the paper’s wording, removed the unsupported claim that UNREACHABLE properties are not counted as evidence, added the C stubbing and TrustInSoft facts, and marked the trust-base list as Inference; did not check: the figures’ code (Fig. 2, 3, 5–9 are images), the DOI’s resolution, and the references.

Last edited: 2026-10-17