Engineering a Formally Verified Automated Bug Finder

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

scope and result

The paper defines correctness for symbolic-execution bug finders and implements WiSE in Coq. Its central claim is that a tester can be both T-sound (soundness for testing: a yes answer to the question whether the program has a bug implies a bug witness exists) and T-complete (completeness for testing: if a bug witness exists, the tester eventually answers yes). The paper’s conditions are a symbolic semantics related to the concrete one by reachability, breadth-first path selection, and a constraint solver that classifies unsatisfiable path conditions correctly (Sect. 3.1, 3.5). The authors formalize a small imperative language IMP with assignments, sequencing, conditionals, while loops, skip, and fail; IMP has no multiplication or division (Sect. 1.1). They prove symbolic reachability equivalent to concrete reachability, derive bug-detection theorems, extract an OCaml implementation from Coq automatically, and port WiSE to Python (PyWiSE) manually (Sect. 4). The paper states: “This paper presents a systematic approach for engineering provably sound and complete symbolic execution-based bug finders by relating a programming language’s operational semantics with a symbolic semantics.” (Abstract, p. 1)

technique 1: relate concrete and symbolic semantics

Use this when a symbolic executor must be justified rather than tested only by examples. Define concrete states as environment/program pairs and give small-step rules. Define symbolic states as path-condition/store/program triples. Start execution at <true, id, p>, where id maps each variable to a same-named symbolic value. Symbolic assignments update expressions; conditionals and loops fork, conjoining the guard or its negation to the path condition.

The proof uses a concretization relation. A concrete state is represented by a symbolic state when the program counters agree, the concrete environment equals the initial environment concretized through the symbolic store (V = V0 ◦ S), and the initial environment satisfies the path condition (Definition 2.3). Prove store-update commutation (Lemma 2.1) by structural induction on the expression, monotonicity of path conditions (Lemma 2.2), and one-step simulation in both directions (Lemma 2.3 for soundness, Lemma 2.5 for completeness). Lift one-step simulation to reflexive-transitive closure (Lemmas 2.4 and 2.6). The resulting theorem is Reachsym(p, σ) ⇔ Reach(p, σ) (Theorem 2.1). The paper states: “The glue we use to establish this connection is reachability.” (Sect. 2.1, p. 4)

Inference: In Verus, model an IMP state with Rust datatypes and define a spec fn for expression evaluation and a recursive concretization relation. State simulation as ensures on proof functions, using requires for well-formed stores and path-condition satisfaction. Verus can encode the inductive lemmas, but the paper’s Coq extraction and coinductive streams do not carry over directly.

technique 2: reduce bug finding to reachability and stuckness

Use this when the product needs a precise bug oracle. Define Progress(σ) as the program being skip or σ having a successor; define Stuck(σ) as its negation. skip is excluded on purpose: the authors were “more thinking of fail” (Sect. 2.2). A program has a bug when some reachable state is stuck. Define symbolic counterparts by replacing concrete reachability with symbolic reachability and concretizing the symbolic state before testing stuckness. Prove equivalence for three queries (Theorems 2.4 to 2.6): whether a program has any bug (HasBug), whether a particular state is erroneous (IsBug), and whether a given input triggers a bug (BadInput). The paper states: “A buggy program has a reachable, stuck state.” (Definition 2.7, Sect. 2.2, p. 5)

The implementation’s oracle is_stuck marks a state as stuck when the next command is fail; the paper says it “can be shown that a state is stuck if and only the next statement to be executed is fail” (Sect. 3.1, p. 7). For division the paper suggests, as an extension of IMP and not as part of it, adding before each x / y the statement if y == 0 then fail else d = div(x,y), replacing x / y with the fresh variable d, where div uses repeated subtraction (Sect. 3.1). To report a bug-triggering input, a constraint solver must extract a solution V0 from the path constraint; the paper states “Constraint solving is not in our scope” (Sect. 2.2). Figure 5 decomposes symbolic bug finding into checks for reachability, satisfiability, and stuckness (p. 6).

Inference: In Verus, represent the oracle as a spec fn returning whether a state is fail and prove that any reported witness satisfies the concrete transition relation. Keep SMT solving outside verified code; treat returned models as inputs checked by a verified replay function.

technique 3: breadth-first lazy exploration with proved properties

The paper argues that depth-first search is incomplete in general: such executors “likely get lost in ever deeper iterations of loops at the beginning of a program” (Sect. 3.1). Implement expand to return the symbolic successors of a state (at most two, for if and while; Fig. 7). Implement run over a FIFO task list: yield the first state, append expand results at the end, and recurse; yield None when the queue is empty (Fig. 6). The paper states: “At every iteration, it yields the first state from the queue. Then, the direct successors of the current state are computed using expand and enqueued in the task queue (with the lowest priority, realizing a breadth-first search).” (Sect. 3.2, p. 7)

Represent execution as a lazy infinite stream rather than imposing a loop-unrolling bound inside the verified executor; the paper says a bound “prevents us from reasoning about the T-completeness of a symbolic executor”. The OCaml and Python implementations still retrieve elements from the stream up to a user-specified bound (Sect. 3.1). Prove expand matches the symbolic one-step relation exactly (Theorem 3.1). Prove every emitted state is reachable from the input list (relative soundness, Theorem 3.2), every →*sym successor eventually appears (relative completeness, Lemma 3.1 and Theorem 3.4), and None is permanent once emitted (sound termination, Theorem 3.3). The completeness proof relies on BFS: a successor appears at a predictable index, at most |l| + 2 places after its parent, because each state has at most two successors. Convert states to Pending, BugFound, or Finished messages with display (Fig. 8) and prove relative soundness and completeness for the bug finder (Theorems 3.5 and 3.6) and sound termination (Theorem 3.7).

Inference: In Verus, a finite queue and an explicit fuel parameter are practical. Prove that each dequeue either emits a previously queued state or decreases a queue measure; represent unbounded completeness as a theorem over any finite depth rather than an executable infinite stream.

technique 4: obtain T-sound/T-complete decisions with a solver

Use this when a binary “has bug” answer is required. Filter BugFound states through a satisfiability check is_sat on the path condition. Iterate the stream until a BugFound with a satisfiable path is found (YES) or a Finished message is reached (NO). Figure 10 gives has_bug this way, and Theorem 3.8 states has_bug(p) = YES ⇔ HasBug(p) (Sect. 3.5, p. 10). The paper says excluding false positives with unsatisfiable path constraints “requires a complete constraint solver that correctly classifies all unsatisfiable path conditions” (Sect. 3.3, p. 8).

The proof of Theorem 3.8 is pen-and-paper, not mechanized: “Since only terminating functions can be implemented in Coq, we have to resort to a “pen-and-paper” proof of has_bug’s T-soundness and T-completeness” (Sect. 3.5, p. 10). It follows from relative soundness/completeness.

Evidence: OCaml extraction is automatic, while PyWiSE is a manual port that “re-implemented the Coq code with only small, purely syntactical changes” (Sect. 4, p. 10). Three numeric algorithms (factorial, integer square root, greatest common divisor) are annotated with assertions and each has a hand-made buggy mutation (for example, while _s > x do changed to while _s < x do). The authors assert that their executors find the inserted bug and report no bug for the original programs, and that symbolic execution terminates with Finished for correct programs when the input domain is restricted to a finite range. With a --depth-first option added to PyWiSE, the factorial bug is not found because symbolic execution is trapped in infinite iterations of an early loop (Sect. 4, p. 10). The paper gives no timings or other quantitative results. The extracted implementations are not themselves proved correct. The paper explicitly says: “Since the transformations from Coq to executable programs are not formally proven correct, we evaluated them with three numeric algorithms.” (Sect. 4, p. 10)

what is proved, measured, and trusted

Proved in Coq (the paper’s claim; Coq sources not inspected here): reachability equivalence, the three bug-detection equivalences, correct expansion, and relative soundness, completeness, and sound termination of run and the bug finder. Proved on paper only: T-soundness and T-completeness of has_bug (Theorem 3.8). Defined, not proved: the IMP operational and symbolic semantics. Tested, not measured: three algorithm case studies, plus termination on finite input domains. Trusted, as stated in the paper: the external constraint solver (the paper names Z3 and CVC5 as typical off-the-shelf solvers for symbolic executors, Sect. 3.5), solver completeness for T-soundness, and the unproved Coq-to-OCaml/Python transformations.

techniques for the catalog

• semantic simulation: prove symbolic and concrete reachability equivalent through concretization and step simulation
• stuck-state oracle: define bugs as reachable stuck states and separate reachability, satisfiability, and oracle checks
• BFS lazy executor: explore symbolic states with FIFO expansion and prove relative soundness, completeness, and termination signaling
• solver-filtered decision: turn a stream of bug reports into a T-sound/T-complete binary result with satisfiable path conditions (needs a complete solver; the proof of this step is pen-and-paper)

Last edited: 2026-10-18