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

Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors in Rust

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

The paper introduces PanicCheck, a Rust annotation and macro pipeline that turns one #[panic_check] annotation into a symbolic test and runs KLEE to find panic-triggering inputs. The paper’s abstract says: “Using PanicCheck, engineers only need to annotate the function-to-verify with #[panic_check].” (Abstract, p. 1). Rust’s Result<T, E> represents recoverable errors; panics terminate execution and are the paper’s shorthand for unrecoverable errors (Introduction, p. 1).

What it is. PanicCheck wraps Rust Verification Tools (RVT), LLVM bitcode generation, and KLEE. KLEE conducts inter-procedural analysis to explore execution paths, uses the constraint solver STP to decide whether each path is feasible, generates a concrete input for each feasible path, and checks whether any values can cause an unrecoverable error (Section 2.1, p. 2). Without PanicCheck, RVT requires a developer to define a test function that asserts a property (e.g., no panic), and to specify with RVT’s domain-specific language how each parameter is symbolized (Section 2.2, pp. 2–3). The paper’s motivating decode_var(src: &[u8]) example requires a vector of 30 symbolic u8 values, a call to decode_var(&v), and assert!(result.is_ok()) on the result of panic::catch_unwind (Listing 1, p. 3).

How to apply it. The paper defines four phases (Figure 1, p. 2); steps 1 and 6 below are the user’s actions around them:

  1. add #[panic_check] to the function to verify. The paper’s example is #[panic_check] fn decode_var(src: &[u8]) -> (Self, usize) { ... } (Listing 2, p. 3)
  2. extract context (Phase I). The macro receives the annotated function’s token stream from the compiler, parses it with syn, and traverses the syntax tree to locate the function name, parameter list, and parameter types (Section 3, pp. 3–4; Section 3.1, p. 4)
  3. create symbolic variables (Phase II). For each parameter, choose a type-specific generator (Section 3.2, p. 4). The generated code declares a Strategy1 trait with a uniform value_gen(...) function, implements it per parameter type, and calls RVT’s AbstractValue::abstract_value() (Section 3.3.1, p. 5; Figure 2, p. 7)
  4. generate and compile the test (Phase III). A template declares the symbolic variables and calls the function. PanicCheck produces a human-readable Rust version and an executable version for KLEE; the command cargo-verify --backend=KLEE --tests builds the program and all test functions, then executes the built code with KLEE (Section 3, p. 3; Section 3.3, p. 5)
  5. execute KLEE (Phase IV). During conversion to LLVM bitcode, the cargo-verify command injects value checks that guard critical instructions and inserts panic! macros for failed checks; PanicCheck implements nothing for this step. KLEE unrolls loops as needed, explores paths reaching panic statements, and outputs value assignments to symbolic variables as panic-triggering inputs (Section 3.3.2, pp. 5–6)
  6. inspect the counterexample. In the example, KLEE reports src = [128, 128, 128, 128, 128, 128, 128, 128, 128, 128, 0, ...], the code location src/varint.rs:121:23, and “attempt to shift left with overflow” (Section 3.3.2, p. 6)

Inference: in Verus, the same safety obligation would usually be expressed as a contract rather than as generated symbolic tests. A verified Rust function can state requires bounds on a slice and ensures relating the returned value to the input, while assert and proof fn establish arithmetic facts. Verus can prove that a shift count is below the bit width for all inputs admitted by the precondition; KLEE’s concrete input is a bug-finding witness rather than a universal proof. The paper’s annotation can still be useful as a test harness around Verus code, especially for panic behavior in dependencies or unsupported Rust features.

Evidence. The experiment used Rust 1.47.0-nightly (2020-08-02), LLVM 10.0.0, and KLEE commit c51ffcd... (Section 4, p. 6). It annotated 125 entry functions in 21 open-source projects (100 of them main functions of coreutils subprojects) and more than 40 functions in two closed-source ByteDance projects (Section 4.2, pp. 6–7). In the open-source set, “PanicCheck revealed 59 panics for 59 functions but failed to verify 11 functions due to state explosion; 3 functions passed complete verification and 52 functions passed partial verification due to the time limit.” (Finding 1, Section 4.3, pp. 7–8). The closed-source projects yielded two panics, both confirmed and fixed (Section 4.3, p. 8). Across all 23 projects, it found 61 panics; 52 had already been fixed before the authors filed any report, and developers fixed seven of the nine issues the authors filed, giving 59/61 addressed as of the authors’ September 2023 recheck (Section 4.3, p. 8). The denominator is panics, not functions or projects. The paper says the 61 panics reside in 6 projects (Section 8, p. 10). Of the 61, 45 came from the clap library’s “unexpected invalid UTF-8 code point” and nine from unwrap() on invalid values, all in coreutils subprojects (Section 4.3, p. 8). The paper reports that all errors KLEE reported were true positives (Section 6.1, p. 9).

PanicCheck added 6–128 seconds to the build, which the paper describes as expanding compilation overhead by 0.4–21.2 times; the overhead applies only in testing mode (Section 4.3, pp. 7–8). KLEE finished in 1–886 seconds for 56 coreutils subprojects and 5 other projects; for 44 coreutils subprojects and 16 other projects it did not finish within the two-hour limit; nine projects were stuck in state explosion (Section 4.3, p. 8). These numbers count functions, projects, or subprojects as the paper states them, not a fraction of all Rust code.

Limits and assumptions. KLEE has path explosion, bounded loop checking, and potentially long STP solving (Section 2.1, p. 2). PanicCheck fully or partially supports 28 types: 18 primitive, four compound, and six collection types (Section 3.2, p. 4). It fully supports 16 of the 22 primitive types and the unit type; shared references are partial, mutable references are unsupported, and fn and pointer types are unsupported (Section 3.2.1, p. 4; Table 1, p. 5). Arrays require primitive elements and length 1–30. Option, Result, and String are the only supported enum/struct forms. Tuples must have 2–11 primitive elements. Vec, VecDeque, and LinkedList are fixed at 30 elements; BTreeMap and BTreeSet at 10; BinaryHeap at five (Table 1, p. 5). HashMap and HashSet are unsupported (Section 3.2.3, p. 4). The paper explains the collection bound: “We noticed that KLEE becomes extremely slow and usually produces no output if the length goes beyond 30.” (Section 3.2.3, p. 4). String enumeration and raw-pointer conversion caused state explosion in the evaluation (Table 3, p. 8). KLEE cannot analyze concurrent programs, cannot symbolize the size of memory allocation, and has very limited pointer support (Section 6.2, p. 9). The implementation targets Rust 2018, does not analyze or validate lifetime annotations, and does not generate mutable-reference variables (Section 5, p. 9).

technique: type-specific symbolic value synthesis

What it is. PanicCheck uses one generation strategy per supported Rust type. Primitive types call the corresponding abstract_value() API. A char is generated as symbolic u32 and passed through char::from_u32(c).unwrap_or_reject() so only valid character values remain. A shared reference first creates a symbolic referent and then borrows it (Section 3.2.1, p. 4). An array declares the fixed length and fills every element with an independent symbolic primitive. Collections are populated with independent symbolic primitive elements, keys, or values (Table 1, p. 5).

How to apply it. For each function parameter, inspect its exact Rust type; select the table’s generator; use the paper’s fixed bound when the type is a collection; generate only primitive elements where the paper permits elements; and reject unsupported pointers, mutable references, hash collections, custom structs, custom enums, and bare slice or str types (slice and str references are supported) (Sections 3.2.1–3.2.3, p. 4; Table 1, p. 5). The generated strategy implementation calls RVT’s AbstractValue::abstract_value() as needed to create symbolic variables (Section 3.3.1, p. 5).

Inference: Verus does not need a symbolic-value generator for a universal contract. A Verus proof can quantify over a sequence abstraction and prove a loop invariant such as 0 <= i <= src.len(), but executable Rust still needs a concrete test value. For a bounded smoke test, use ordinary Rust constructors and assert; for the proof, use requires, ensures, loop invariant, and proof lemmas in the supported Verus syntax. The paper’s 30/10/5 bounds become test-model assumptions and cannot establish behavior for longer collections.

Evidence and failure. The type table is the evidence of coverage, and its denominator is the paper’s listed types, not all Rust types (Table 1, p. 5). The paper attributes partial support for arrays and tuples to the number of independent variables KLEE must explore, and for custom structs/enums to the difficulty of generating symbolic variables for arbitrary custom data structures (Section 3.2.2, p. 4). Inference: a Verus encoding can model a custom struct directly when its fields and invariants are specified, but the proof burden moves to those invariants and does not disappear.

technique: choosing entry functions for a large study

What it is. Instead of annotating every function, the paper annotates only entry functions, because verifying every function is time-consuming and KLEE’s inter-procedural analysis can make the symbolic execution of some functions cover that of others (Section 4.2, p. 6).

How to apply it. First choose functions already covered by proptests. If there is no proptest, annotate every API listed in lib.rs. If neither exists, annotate main (Section 4.2, pp. 6–7). With these rules the authors annotated 125 entry functions in 21 open-source projects, one of which, coreutils, contributed 100 subproject main functions, and more than 40 closed-source functions (Section 4.2, p. 7).

Inference: for Verus, entry selection should follow the public API and proof decomposition. Prove reusable helpers once, then expose contracts at public functions; retain PanicCheck or ordinary tests at API boundaries for integration behavior. Selecting only entries leaves internal functions covered only when reachable in the explored call graph or when their contracts are separately proved.

Evidence and limits. The paper gives the redundancy of inter-procedural exploration as a reason for the rule (Section 4.2, p. 6). Inference: the approach does not check functions unreachable from the chosen entries. The paper’s external-validity threat is explicit: “All the empirical observations we made so far are based on our experimental dataset.” (Section 5, p. 9).

what is proved, what remains trusted, and product relevance

The paper demonstrates that a particular Rust-to-LLVM-to-KLEE pipeline can find concrete panic inputs and that developers fixed 59 of the 61 reported panics (Section 4.3, p. 8). Inference: it does not prove panic freedom for paths KLEE timed out on, loops beyond its bounded exploration, unsupported types, or arbitrary Rust programs. KLEE, STP, LLVM’s Rust lowering, the injected checks, PanicCheck’s parser and templates, the Rust compiler, and the interpretation of a panic as a product defect remain trusted or assumed. Verus changes the trust boundary by proving contracts with a solver, but the Verus verifier, solver, compiler, erased proof code, specifications, and external-library contracts remain trusted in the same broad sense.

Inference: the threat to VeruLaw is medium. PanicCheck is a practical front end for finding crashes in agent-written Rust and supplies concrete regression tests, but its bounded symbolic values and KLEE limitations cannot replace Verus’s universal functional and memory-safety proofs. The useful integration is to let an agent add #[panic_check]-style exploratory tests while Verus contracts prove the general arithmetic, bounds, ownership, and API properties. The product should preserve the denominator and timeout metadata from each KLEE run, because “pass” in the paper’s Table 2 includes both complete verification and partial verification cut off by the two-hour limit (Table 2, p. 7).

The paper’s own work already covers annotation-driven test synthesis, type-specific symbolic construction, entry-point selection, and a 23-project empirical study; LLVM instrumentation and KLEE path exploration come from the existing RVT toolchain it invokes (Section 3, p. 3). Inference: a new VL implementation should reuse these ideas and focus on the gap they leave: translating a discovered panic input into a Verus precondition, a regression test, and a proof obligation, while recording unsupported types and timeouts instead of treating them as successful verification.

techniques for the catalog

  • annotation-driven KLEE panic search: annotate one Rust function, synthesize a test, compile to LLVM, and use KLEE to emit panic-triggering inputs
  • type-specific symbolic value synthesis: map supported Rust parameter types to RVT symbolic constructors with fixed collection bounds
  • strategy-pattern test generation: generate a uniform value_gen() implementation per parameter type and call the function under test
  • entry-function selection: prioritize proptest targets, public lib.rs APIs, and finally main to reduce redundant exploration
  • LLVM panic instrumentation: the existing cargo-verify toolchain injects value checks on critical instructions and panic! on failure before KLEE explores the resulting paths Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “PanicCheck does not generate any symbolic variable for pointers, as KLEE does not handle pointers well.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed most page references (they were off by one, e.g. Table 1 is p. 5, Section 6.1 is p. 9), corrected the four-phase steps and the 0.4–21.2 overhead wording, fixed the dataset count to 21 open-source projects with coreutils among them, softened an overstated claim of impossibility about custom types, attributed instrumentation to the existing cargo-verify toolchain, added the closed-source, root-cause, 6-project and concurrency facts, marked unsupported conclusions “Inference:” and removed an unsupported pointer to other Verus notes; did not check the Verus statements against Verus documentation, the linked repository, or the PDF layout beyond the text.

Last edited: