fold/docs/internal/symex-fuzz-landscape.md

Symbolic Execution + Fuzzing Tools Landscape

Architecture expansion research for fold. Generated 2026-05-27.

Maps the symbolic execution, model checking, abstract interpretation, and fuzzing tools relevant to fold's multi-language expansion across C++, Rust, Swift, and binary targets. For each tool: approach, IR level, language support, false-positive profile, maturity, and concrete integration pattern for fold.

Table of contents

1. Taxonomy
2. Symbolic execution engines
3. Model checkers & verifiers
4. Abstract interpreters
5. Fuzzing engines
6. Binary analysis frameworks
7. Integration pattern catalog
8. Architecture expansion recommendations

---

Taxonomy

Approach	What it does	fold already does it?
Symbolic execution	Tracks symbolic values along paths, queries SMT at branches	Yes — Z3 BV-64 encoder, per-sink SAT queries
Concrete fuzzing	Mutates byte inputs, runs target natively, reports crashes	Yes — libFuzzer/AFL++ via fold fuzz-run
Concolic execution	Concrete execution + parallel symbolic shadow store, negate branches	Planned — M31 Phase 3 (LibAFL+symcc-rt)
Model checking	Encode full program + property as SMT formula; prove or find counterexamples	No — fold is per-function, not whole-program BMC
Abstract interpretation	Fixed-point over abstract domains (intervals, octagons, polyhedra)	Partial — interval pre-pass, no AI fixpoint engine
Binary analysis	Disassemble + lift to IR for pattern/heuristic detection	Yes — R2Backend for strings/symbols/calls/xrefs

---

Symbolic execution engines

KLEE

Dimension	Detail
Approach	Full symbolic execution
IR level	LLVM IR (bitcode)
Languages	C, C++ (any language that compiles to LLVM IR)
Solver	KLEE's own constraint solver + Z3 backend
FP rate	Low — explores actual paths. Missing code produces false negatives, not false positives.
Maturity	Very high. 15+ years. Active maintenance (KLEE 3.1, 2024). SV-COMP participant.
License	GPL-2.0 (with LLVM exception for the ucKLEE variant)
Key capability	Bottom-up path exploration from a harness entry point. Produces high-quality test inputs for every covered path. Symbolic filesystem, POSIX environment models.

How it works:

KLEE interprets LLVM bitcode symbolically. Memory is a flat symbolic array with byte-level granularity. At branches, KLEE forks the state and adds the branch condition to each path's constraint set. When a path terminates, KLEE concretizes the symbolic input to produce a test case. KLEE's constraint solver layer (KQuery → STP/Z3) optimizes for the pattern-matching checks common in path exploration.

Integration pattern for fold:

The license mismatch (GPL-2.0 vs fold's planned GPL-3.0) is noted in docs/internal/m31-phase3-concolic.md and is the primary reason fold deferred KLEE adoption. Architectural mismatch too: KLEE owns the process (its own interpreter loop), while fold orchestrates child processes via posix_spawn.

If fold's license posture changes, a useful integration would be:

fold scan → findings with Z3 witnesses
    ↓
fold fuzz-prep → emit KLEE harness (.c file calling target function)
    ↓
klee --libc=uclibc --posix-runtime harness.bc
    ↓
fold fuzz-ingest ← KLEE test cases → ConcreteWitness promotion

KLEE's strength — exhaustive bounded path coverage from an entry point — complements fold's per-sink SAT approach. KLEE could confirm that a fold-flagged sink is actually reachable from a program entry point, closing fold's "SAT under our encoding but maybe unreachable" gap.

Relevance to fold: Medium. The license barrier is real. The architectural mismatch (KLEE as interpreter, fold as orchestrator) means integration would be a side-by-side pipeline, not an embedded pass. Worth reconsidering if fold adds a verification tier (e.g., CBMC-style whole-module bounded verification) where KLEE's path coverage complements fold's bottom-up scan.

---

Haybale

Dimension	Detail
Approach	Symbolic execution
IR level	LLVM IR (via llvm-ir crate)
Languages	Any language with LLVM bitcode (practically: C, C++, Rust via --emit=llvm-ir)
Solver	Boolector (default), Z3 (optional backend)
FP rate	Very low — full path exploration, well-defined memory model.
Maturity	Research-grade. Last major release 2021. Trail of Bits project, not actively maintained.
License	MIT / Apache-2.0
Key capability	Pure Rust symbolic execution for LLVM IR. Clean API for programmatic path exploration, hookable function models, and SMT query callback.

How it works:

Haybale is a Rust library that loads LLVM bitcode and provides a symbolic execution engine. It uses Boolector (a bitvector SMT solver, also from the Boolector/STP/KLEE lineage) for constraint solving. The API is designed for embedding: you write a Rust program that uses Haybale to explore specific functions. Haybale handles memory as a flat byte-addressable array, models LLVM instructions symbolically, and provides hooks for modeling library functions.

Integration pattern for fold:

Haybale's Rust-native design and permissive license make it the most architecturally natural symbolic execution backend for fold's Rust expansion. Integration shape:

fold scan --mode rust <crate>
    ↓
fold-rust extract → NDJSON (IR + findings)
    ↓
fold-concolic (Rust crate) → Haybale Project::from_bc_path()
    ↓                            ↓
target_fn.bc ← rustc --emit=llvm-ir    symbolically_execute_fn()
    ↓
path constraints → Boolector/Z3 → new seeds → libFuzzer corpus

Haybale could serve as fold's Rust-native answer to the C++ side's symcc-rt + LibAFL concolic bridge. Because Haybale is a library (not a process), it avoids the subprocess IPC overhead. It also avoids the license problem KLEE has.

Relevance to fold: High for the Rust frontend specifically. Haybale provides symbolic execution for LLVM IR from a Rust host — exactly what a fold-concolic Rust crate would need to do path exploration on Rust-generated bitcode. The lack of active maintenance is a risk, but for fold's bounded-model use case (not full-system symbolic execution), the existing codebase may be sufficient. Evaluate in a spike: can Haybale load and symbolically execute the bitcode from a fold-rust extract target in under 100 lines of integration code?

---

Model checkers & verifiers

Kani

Dimension	Detail
Approach	Bounded model checking (CBMC-based)
IR level	Rust MIR → GOTO intermediate representation → SMT
Languages	Rust
Solver	CBMC's built-in SMT pipeline (Z3, MathSAT, CVC5 backends)
FP rate	Very low (sound for the bound chosen). Properties are proved, not guessed.
Maturity	High. AWS-backed, active development (2024 releases). Growing adoption in safety-critical Rust.
License	MIT / Apache-2.0
Key capability	Verify Rust programs against user-written #[kani::proof] harnesses. Prove absence of panics, overflows, and user-specified assertions within a bounded unrolling depth.

How it works:

Kani compiles Rust MIR into CBMC's GOTO intermediate representation, then runs CBMC's bounded model checker on the result. Users write proof harnesses annotated with #[kani::proof] and kani::assume()/kani::assert(). Kani then verifies (proves or finds counterexamples for) those harnesses. The result is either a proof (no property violation within the unrolling bound) or a concrete counterexample trace.

Kani is verification, not scanning: it proves properties of specific harnesses, not "find all bugs in this codebase."

Integration pattern for fold:

Kani occupies a different niche than fold (verification vs scanning), but they compose well:

fold scan --detectors security → findings for Rust unsafe blocks
    ↓
For each high-confidence finding:
    ↓
fold emit-kani-proof → generate #[kani::proof] harness for the flagged function
    ↓
cargo kani --harness <name>
    ↓
    ├─ VERIFIED → fold finding downgraded to "Kani-proved unreachable"
    └─ FAILED  → Concrete counterexample → fold promotes to ConcreteWitness

Fold adds bottom-up scanning ("find plausible bugs") and Kani adds top-down verification ("prove this specific property"). Fold's per-sink SAT queries find candidates; Kani's whole-program BMC confirms or refutes them with higher confidence.

The integration is straightforward because both tools work with Rust's MIR (fold-rust via rustc_driver → HIR; Kani via kani-compiler → GOTO). A fold emit-kani-proof command that generates Kani harnesses from fold's Rust findings would be a ~200-line addition to tools/fold-rust/.

Relevance to fold: High for the Rust expansion's confidence pipeline. Kani provides the verification tier fold's Rust side currently lacks (all Rust findings are Heuristic today). A fold→Kani bridge would promote some findings to "verified unreachable" and others to "concrete counterexample" — the same closed loop the C++ side achieves with Z3→libFuzzer→ConcreteWitness.

---

Rudra

Dimension	Detail
Approach	Static analysis (pattern-matching + dataflow)
IR level	Rust MIR (via rustc plugin, now deprecated) and HIR
Languages	Rust
FP rate	Low for unsafe-API patterns; moderate on send/sync inference.
Maturity	Research project (Georgia Tech, 2020-2021). Deprecated as of 2023 — the rustc plugin API it used is removed.
License	MIT
Key capability	Found 76 CVEs and 112 RustSec advisories in the Rust ecosystem. Pioneered systematic unsafe-block auditing at ecosystem scale.

How it works:

Rudra ran as a rustc plugin (before the plugin API was removed) and analyzed Rust MIR for three classes of bugs: (1) unsafe API misuse (e.g., Vec::from_raw_parts with untrusted lengths), (2) incorrect Send/Sync implementations leaking interior mutability, and (3) panic safety violations in unsafe code. The analysis was primarily pattern-matching over MIR combined with limited dataflow.

Why Rudra is listed even though deprecated:

Rudra's detector catalog — the specific patterns it flagged — is a design blueprint for fold-rust's security detectors. Rudra proved these patterns have high yield in real-world Rust code (112 advisories). fold-rust can re-implement the same patterns as HIR visitors in tools/fold-rust/src/.

Integration pattern for fold:

Rudra is a source of detector ideas, not a runtime to integrate:

Rudra's detector catalog → fold-rust HIR visitors:
    Send/Sync inference ↓
    unsafe API patterns ↓
    panic safety      ↓
    → fold-rust finding_kind: rust-unsafe-api

fold-rust already has the rust-unsafe-api and rust-unchecked-index finding kinds (include/fold/report/finding.hpp). Rudra's specific patterns (e.g., "Vec::from_raw_parts with untrusted capacity") should be added as rules under those kinds. This is a detector-authoring task within fold-rust, not a tool integration.

Relevance to fold: Medium (as a detector catalog). Rudra's 112-advisory track record makes it the strongest source of real-world Rust unsafe patterns. fold-rust's DerefHunter covers raw-pointer derefs; adding Rudra's send/sync and unsafe-API patterns would make fold-rust a genuine Rust SAST rather than a single-detector tool.

---

MIRAI

Dimension	Detail
Approach	Abstract interpretation
IR level	Rust MIR
Languages	Rust
FP rate	Moderate — abstract interpretation over-approximates; many "maybe" results.
Maturity	Research project (Facebook/Meta, 2019-2023). Not actively maintained as of 2024.
License	MIT
Key capability	Taint tracking, integer overflow detection, unreachable code detection. Abstract domain with widening on MIR.

How it works:

MIRAI runs as a rustc driver (similar to fold-rust's architecture) and lifts Rust MIR into an abstract interpreter. It tracks integer ranges (via intervals + widening) and taint, flagging potential panics, overflows, and unreachable code. Unlike Kani (which does bounded model checking), MIRAI does abstract interpretation: it computes a fixpoint over abstract domains and reports when the abstract state indicates a possible problem.

Integration pattern for fold:

MIRAI's abstract interpreter is conceptually similar to fold's interval pre-pass (src/symbolic/ interval analysis), but applied at the MIR level for Rust. Direct integration is impractical (MIRAI is unmaintained research code). However, the architectural lesson is valuable:

MIRAI-style abstract domain → fold-rust MIR visitor (future)
    Interval domain      → refine Heuristic findings with range constraints
    Taint domain         → feed fold's taint-track detector on Rust
    Layout domain        → prove pointer provenance at compile time

fold-rust currently operates at the HIR level (via rustc_driver + rustc_hir). To match MIRAI's precision, fold-rust would need a MIR visitor for the abstract domains. The existing HIR infrastructure (DerefHunter) works for syntactic patterns; MIR adds type resolution after monomorphization, which is necessary for range analysis.

Relevance to fold: Medium (architectural lesson). MIRAI proves that abstract interpretation on Rust MIR is practical and can find real bugs. fold-rust should plan a MIR visitor layer for future precision upgrades (RF-3b already calls this out: "move to MIR + monomorphization context"). MIRAI is the prior art that demonstrates it works.

---

Miri

Dimension	Detail
Approach	MIR interpreter (concrete execution, not symbolic)
IR level	Rust MIR
Languages	Rust
FP rate	Essentially zero — detects actual UB at runtime on concrete inputs. False negatives possible (input-dependent).
Maturity	Very high. Official Rust project, shipped via rustup +nightly component add miri. Actively maintained.
License	MIT / Apache-2.0
Key capability	Detects undefined behavior in Rust (including unsafe code) by interpreting MIR with UB checks. Stacked Borrows model for pointer provenance.

How it works:

Miri interprets Rust MIR directly instead of compiling to machine code. During interpretation, it checks for UB: out-of-bounds accesses, use-after-free, data races, invalid pointer dereferences, and violations of the Stacked Borrows aliasing model. Miri is a concrete interpreter — it runs a single execution path with concrete inputs. It does not do symbolic execution or path exploration.

Integration pattern for fold:

Miri is a runtime checker, not a static analyzer, but it's fold's most natural Rust validation tier — analogous to ASan on the C++ side:

fold scan --mode rust → findings (Heuristic confidence)
    ↓
fold fuzz-prep → generate Rust harness with concrete seeds
    ↓
MIRIFLAGS="-Zmiri-disable-isolation" cargo +nightly miri test
    ↓
    ├─ UB detected → fold finding promoted to ConcreteWitness
    └─ Clean run   → finding remains Heuristic (unconfirmed)

The integration is simpler than Kani: fold's fuzz-prep already generates C harnesses (for libFuzzer+ASan). A Rust variant would generate #[test] functions with miri cfg-gating, and fold's runner would shell out to cargo +nightly miri test instead of compiling + running a libFuzzer binary.

Miri also integrates with cargo-fuzz: cargo fuzz targets can run under cargo +nightly miri run for fast UB detection on small inputs before a full fuzzing campaign. fold's Rust fuzz-prep could emit fuzz targets that are Miri-compatible from day one.

Relevance to fold: Very high for Rust validation. Miri is the Rust ecosystem's gold standard for UB detection, comparable in authority to ASan+UBSan for C++. Every fold Rust finding that passes through a Miri check and produces a UB trace is a ConcreteWitness with the same authority as an ASan crash on the C++ side.

---

Swift tools

SWAN (Swift ANalysis)

Dimension	Detail
Approach	Static analysis framework
IR level	Swift SIL (Swift Intermediate Language)
Languages	Swift
FP rate	Depends on detector. SWAN is a framework; individual analyses vary.
Maturity	Research project (University of Bremen, 2018-2023). SWAN 2.0 added SIL support. Not actively maintained.
License	MIT
Key capability	Taint analysis framework for Swift. SIL-level analysis with configurable sources/sinks, framework for writing custom detectors.

How it works:

SWAN is a static analysis framework built on top of the Swift compiler. It operates at the SIL level and provides taint analysis infrastructure: users define taint sources, propagation rules, sanitizers, and sinks. SWAN then computes TaintFlows through the program. Initially operated on the AST; SWAN 2.0 shifted to SIL for better precision.

Integration pattern for fold:

SWAN is directly relevant to tools/fold-swift/ (Task 73 in the current sprint). The integration pattern:

Swift .swift → swiftc -emit-sil → .sil file
    ↓                                   ↓
fold-swift → parses SIL            SWAN → TaintFlows
    ↓                                   ↓
fold-swift detectors:              fold-swift taint detector:
  - unsafe cast patterns     ←     - taint config from SWAN's source/sink catalog
  - force-unwrap detection          - flow paths from SWAN's propagation model
  - raw pointer derefs
    ↓
NDJSON findings → fold RustBackend → SARIF/JSON report

SWAN provides two things fold-swift needs:

1. A proven taint framework for SIL — the source/sink/sanitizer model already works for Swift.
2. A detector catalog — SWAN ships with detectors for common Swift security patterns (sensitive data leaks, injection, path traversal).

fold-swift can either:

• (A) Shell out to SWAN as a subprocess (SWAN → TaintFlow JSON → fold finding), matching fold-rust's subprocess model.
• (B) Re-implement SWAN's taint propagation in fold-swift's own SIL visitor (more work, but avoids an external dependency).

Option A is preferred for speed; option B for long-term maintenance. The immediate path: shell out to SWAN for taint, add fold-swift's own SIL visitors for pattern-matching detectors (unsafe casts, force-unwrap, raw pointer access).

Relevance to fold: High for the Swift frontend. SWAN is the only existing open-source taint framework for Swift SIL, and it's MIT-licensed. It fills the taint-tracking gap fold-swift would otherwise have to build from scratch.

---

Fuzzing engines

AFL++

Dimension	Detail
Approach	Coverage-guided greybox fuzzing
IR level	Source-level instrumentation (compiler pass) OR binary-level (QEMU, Unicorn)
Languages	C, C++, Rust (via cargo-afl), any binary
Solver	None — pure mutation-based with coverage feedback
FP rate	Near-zero — crashes are real. But false negatives (missed bugs) are inherent in fuzzing.
Maturity	Very high. Primary fuzzing engine in the AFL lineage. Active maintenance (2025 releases).
License	Apache-2.0
Key capability	Industry-standard fuzzer. Custom mutators, persistent mode, binary-only fuzzing, LibAFL framework for custom fuzzing pipelines.

How it works:

AFL++ instruments the target (at compile time or binary level) to track edge coverage. It maintains a corpus of interesting inputs and repeatedly mutates them, keeping inputs that discover new coverage edges. Forkserver mode (or persistent mode) avoids process startup overhead. Binary-only mode uses QEMU user-mode emulation with coverage instrumentation.

Integration pattern for fold:

fold already uses AFL++-adjacent patterns via libFuzzer and is planning LibAFL adoption for M31 Phase 3. Specific integration points:

fold fuzz-run currently: libFuzzer + ASan
    ↓
fold fuzz-run future:   LibAFL + libFuzzer (configurable backend)
    ↓
fold binary-fuzz-prep:  AFL++ QEMU mode for Mach-O/ELF binaries
    ↓
fold binary-fuzz-run:   AFL++ -Q (QEMU mode) or LibAFL binary-only

For fold's binary analysis path (R2Backend), AFL++ is the primary fuzzing runtime. fold's docs/internal/binary-fuzz-corpus.md already documents the dlopen harness pattern; AFL++'s QEMU mode would allow fuzzing binaries without source access — a natural complement to fold's r2-based binary string/symbol detectors.

Relevance to fold: High. AFL++ (via LibAFL) is fold's planned concolic runtime (M31 Phase 3). AFL++ QEMU mode fills the binary fuzz gap currently occupied by the unimplemented fold binary-fuzz-prep path. AFL++ custom mutators could consume fold's Z3-derived dictionaries (already emitted by src/fuzz/dict_miner.cpp).

---

libFuzzer

Dimension	Detail
Approach	Coverage-guided in-process fuzzing
IR level	Source-level (compiled with -fsanitize=fuzzer)
Languages	C, C++ (LLVM toolchain)
Solver	None — mutation-based
FP rate	Near-zero for crashes; coverage gaps are false negatives
Maturity	Very high. Part of LLVM. Stable and well-documented.
License	Apache-2.0 (LLVM)
Key capability	In-process, fast, tightly integrated with ASan/UBSan/MSan. Data-flow-guided mutations (-use_value_profile=1).

How it works:

libFuzzer is an in-process, coverage-guided fuzzer. The user writes LLVMFuzzerTestOneInput(const uint8_t *Data, size_t Size) and links with -fsanitize=fuzzer. libFuzzer takes over main(), maintains a corpus, mutates inputs (with coverage feedback), and reports crashes to ASan. It's single-process and uses fork() only when requested.

Integration pattern for fold:

fold's tightest integration is with libFuzzer — it's already shipped in M31 Phase 1+2 (src/fuzz/):

fold fuzz-prep → emits:
    ├─ harness.c       (LLVMFuzzerTestOneInput calling target function)
    ├─ seed_corpus/    (Z3-derived witness bytes)
    ├─ dictionaries/   (libFuzzer dict from Z3 model constants)
    └─ param_schema.h  (struct layout for parameter passing)

fold fuzz-run → compiles harness + runs libFuzzer → ingest crashes → ConcreteWitness

fold's harness emitter (src/fuzz/harness_emitter.cpp) already generates libFuzzer-compatible harnesses. The fuzz runner (src/fuzz/runner.cpp) shells out to clang for compilation and orchestrates libFuzzer campaigns.

Relevance to fold: Already integrated. libFuzzer is fold's primary fuzzing backend. The M31 Phase 3 plan may supplement it with LibAFL for concolic tracing, but libFuzzer remains the default for simple coverage-guided fuzzing.

---

cargo-fuzz

Dimension	Detail
Approach	Coverage-guided fuzzing (wraps libFuzzer)
IR level	Rust source → LLVM IR → libFuzzer
Languages	Rust
Solver	None
FP rate	Near-zero for crashes
Maturity	High. Official Rust fuzzing tool. Maintained by rust-fuzz team.
License	MIT / Apache-2.0
Key capability	cargo fuzz init scaffolds a fuzz target; cargo +nightly fuzz run builds + runs. Integrates with ASan, cargo-fuzz also supports structure-aware fuzzing via arbitrary.

How it works:

cargo fuzz is a Rust build-system wrapper around libFuzzer. It generates fuzz targets (Rust source files with fuzz_target!() macro), compiles them with -fsanitize=fuzzer via the Rust compiler's LLVM backend, and runs the resulting binary. It also manages corpora, artifacts, and coverage reports.

Integration pattern for fold:

fold already references cargo-fuzz in src/cli/fuzz_prep_runner.cpp:462 (RF-8: "when running in Rust mode, generate cargo-fuzz-style harnesses"). The integration plan:

fold scan --mode rust → Rust findings with Z3 witnesses
    ↓
fold fuzz-prep --mode rust → emits:
    ├─ fuzz/fuzz_targets/target_fn.rs   (cargo-fuzz target)
    ├─ fuzz/corpus/target_fn/           (Z3-derived seeds)
    └─ fuzz/dictionaries/target_fn.dict (libFuzzer dict)
    ↓
fold fuzz-run --mode rust → cargo +nightly fuzz run target_fn
    ↓
ingest crashes → ConcreteWitness promotion

The key difference from C++ fuzz-prep: Rust harnesses compile via cargo fuzz, not direct clang++. The harness generator needs to emit Rust source (not C), with arbitrary::Arbitrary derives for structured input generation. The runner invokes cargo +nightly fuzz run instead of clang++ -fsanitize=fuzzer.

Relevance to fold: High for Rust validation. This is the Rust-side equivalent of fold's existing C++ fuzz-prep→fuzz-run pipeline. The infrastructure is already planned (RF-8). Implementation requires: (1) a Rust harness emitter, (2) cargo fuzz project scaffolding, and (3) runner invocation via cargo instead of direct clang++.

---

Binary analysis frameworks

rev.ng

Dimension	Detail
Approach	Binary lifting + decompilation + symbolic execution
IR level	QEMU TCG → LLVM IR (via rev.ng's own lifter)
Languages	Binary (x86-64, ARM64, MIPS) → lifted LLVM IR
FP rate	Depends on analysis. Lifting introduces approximation; decompilation is best-effort.
Maturity	Active development. Commercial offering (rev.ng S.r.l.) with open-source components. LLVM 19 support as of 2025.
License	GPL-2.0 (open-source core) + proprietary (commercial extensions)
Key capability	Lift binaries to LLVM IR, then apply LLVM-based analysis (including libFuzzer fuzzing via dlopen harnesses).

How it works:

rev.ng lifts machine code to LLVM IR through a multi-stage pipeline: (1) disassemble and recover functions, (2) lift to QEMU TCG (Tiny Code Generator), (3) translate TCG to rev.ng's intermediate representation, and (4) lower to LLVM IR. The resulting LLVM IR can then be analyzed with any LLVM-based tool (optimizers, static analyzers, fuzzers). rev.ng also includes a decompiler that produces C-like output from the lifted IR.

Integration pattern for fold:

rev.ng is referenced in docs/internal/binary-fuzz-corpus.md for the dlopen harness pattern. Two integration modes:

Mode A — Lift-then-fuzz (binary→LLVM IR→libFuzzer):

Mach-O / ELF binary → rev.ng lift → LLVM IR (.bc)
    ↓
fold binary-prep → function list (from exported symbols)
    ↓
emit dlopen harness (C source, calls dlsym → target function)
    ↓
clang++ harness.c lifted_module.bc -fsanitize=fuzzer,address → harness.fuzz
    ↓
libFuzzer + ASan → crash artifacts → fold ConcreteWitness

This is a substantial capability upgrade: it allows fold's full libFuzzer+ASan pipeline to run on binaries without source code. The lifted LLVM IR preserves function boundaries and basic-block structure, so libFuzzer's coverage instrumentation works.

Mode B — Lift-then-analyze (binary→LLVM IR→fold detectors):

Binary → rev.ng lift → LLVM IR
    ↓
rev.ng decompile → C-like output
    ↓
fold scan --compile-db ... → Z3-powered detectors on lifted code

This mode is speculative — lifted LLVM IR is not the same as source-level Clang AST output, and fold's detectors expect source-level constructs (function declarations, types, CFG from Clang). However, for simple functions (no inlining, no optimization artifacts), the lifted→decompiled path could enable fold's Z3 detectors on binary-only targets.

Relevance to fold: Medium. rev.ng's lift → LLVM IR pipeline is the cleanest path for applying source-level analysis techniques to binaries. However, the GPL-2.0 license and commercial split create the same friction as KLEE. fold's binary path today uses r2 for heuristic extraction — rev.ng would upgrade that to symbolic-quality analysis, but at significant integration cost.

---

Integration pattern catalog

Summary of integration patterns relevant to fold's architecture.

Pattern 1: Subprocess + NDJSON (already shipped)

Used by: fold-rust (today), fold-swift (planned), fold's own fuzz orchestrator.

fold binary → posix_spawnp("tool", [args...]) → NDJSON stdout → fold parser → findings/summaries

Where it works: When the tool is a standalone binary with a stable output format. Where it doesn't: When the tool requires an in-process API (KLEE, Haybale).

Pattern 2: Cargo/Rust crate dependency (planned)

Used by: fold-concolic (M31 Phase 3 planned), fold-rust.

tools/fold-concolic/Cargo.toml:
    [dependencies]
    libafl = "..."
    haybale = "..."  (if chosen for Rust symex)

fold binary → fork+exec(fold-concolic) → stdin/argv → findings

Where it works: When the tool is a Rust library and fold can add a Rust crate. Where it doesn't: When the tool is C/C++ only (KLEE, SWAN).

Pattern 3: LLVM pass plugin (not yet adopted)

Used by: symcc-rt (C++ concolic), rev.ng (binary lifting).

fold scan --concolic → clang++ -fpass-plugin=fold_concolic.so → instrumented binary

Where it works: When the tool is an LLVM pass and fold controls the compiler invocation. Where it doesn't: When every LLVM release requires pass rewrites (the symcc lesson).

Pattern 4: Harness generation + external runner (shipped)

Used by: fold fuzz-prep, fold emit-kani-proof (proposed).

fold fuzz-prep → emits harness.{c,rs} + seeds + dict → external runner compiles + runs

Where it works: When the analysis tool takes a harness/entry point as input. Where it doesn't: When fold needs runtime feedback during analysis (needs Pattern 1 or 2).

Pattern 5: Detector catalog import (not runtime integration)

Used by: Rudra (patterns → fold-rust detectors), Clippy (lint catalog).

External tool's detector catalog → re-implement as fold detector.

Where it works: When the tool is a research prototype whose detectors are the valuable artifact. Where it doesn't: When the tool's analysis engine is the valuable artifact (KLEE, Kani, Miri).

---

Architecture expansion recommendations

Based on the landscape analysis, fold's architecture expansion should follow these priorities:

Tier 0 — Ship what's already scoped (current sprint)

Item	Tool	Pattern	Status
Rust MIR validation via Miri	Miri	Harness gen + external runner	Scoped as RF-8 in fuzz_prep_runner.cpp:462
Swift SIL scanning	SWAN	Subprocess + NDJSON	Scoped as Task 73 (tools/fold-swift/)
Concolic execution	LibAFL+symcc-rt	Rust crate dependency	Scoped as M31 Phase 3

Tier 1 — High-impact, low-risk additions (next 2-3 sprints)

1. Rust Kani bridge. fold emit-kani-proof command that generates Kani harnesses from fold-rust findings. Kani verifies (proves or counterexamples) the flagged functions. ~200 lines of Rust in tools/fold-rust/, leveraging fold-rust's existing rustc_driver infrastructure.

2. Haybale spike for Rust symex. Evaluate whether Haybale can load and symbolically execute LLVM bitcode from fold-rust targets. If viable, Haybale could be the Rust-side counterpart to the C++ side's Z3 encoder — providing Proved confidence (not just Heuristic) for Rust findings without crossing the language barrier.

3. AFL++ QEMU mode for binary fuzz. Extend fold binary-fuzz-prep (currently documented in docs/internal/binary-fuzz-corpus.md but unimplemented) to emit dlopen harnesses and run AFL++ QEMU mode against Mach-O binaries. This closes the binary fuzz gap without requiring source code or LLVM bitcode.

Tier 2 — Medium-impact, medium-risk (next 6 months)

4. Rudra detector catalog import. Add Rudra's top-10 highest-yield patterns (send/sync, unsafe API, panic safety) to fold-rust as HIR visitors. Target: fold-rust finds at least 50% of what Rudra found (56 advisories out of 112) via HIR pattern matching alone.

5. MIRAI-style MIR visitor for fold-rust. Add a MIR visitor layer to tools/fold-rust/ that performs interval analysis and taint tracking on monomorphized MIR. This would upgrade fold-rust from "mostly HIR pattern matching" to "has path-sensitive analysis" — closing the precision gap between fold-rust and fold's C++ encoder.

6. rev.ng lift-then-fuzz spike. Evaluate the "lift binary to LLVM IR then fuzz with libFuzzer" pipeline on a small Mach-O fixture. If the lifted IR is stable enough for coverage-guided fuzzing, this unlocks fold's full Z3+libFuzzer pipeline for binary-only targets.

Tier 3 — Strategic, high-risk (long-term)

7. KLEE integration. If fold's license posture changes to accommodate GPL-2.0 (or if KLEE adopts GPL-3.0 or a later-compatible exception), KLEE would provide exhaustive bounded path coverage from entry points, complementing fold's per-sink SAT approach. This is the verification tier fold currently lacks for C++.

8. SWAN taint integration for fold-swift. Beyond the SIL pattern matching covered in Task 73, integrate SWAN's taint analysis framework as a subprocess to add taint-track findings to the Swift frontend.

Decision rules by language target

Language	Scan-time analysis	Validation/confirmation	Concolic/symex
C++	Z3 encoder (shipped)	libFuzzer+ASan (shipped)	LibAFL+symcc-rt (planned)
Rust	HIR visitors (shipped MVP)	Miri + cargo-fuzz (planned)	Haybale spike (Tier 1)
Swift	SIL visitors (Task 73)	ASan via fuzzing (future)	SWAN taint (Tier 3)
Binary	r2 heuristics (shipped)	AFL++ QEMU (Tier 1)	rev.ng lift-then-analyze (Tier 2)

What NOT to pursue

• Prusti, Creusot, Verus (Rust deductive verifiers). These are verification tools requiring user-written specifications in separation logic or Rust-specific assertion languages. fold's value is bottom-up scanning without user annotations. They are complementary, not integrable.
• SymCC pass port (Option A from M31 Phase 3). The maintenance burden of owning an LLVM pass across releases was explicitly rejected in docs/internal/m31-phase3-concolic.md. LibAFL+symcc-rt (Option B) is the chosen path.
• CodeQL for fold's own detectors. CodeQL is a CPG query engine, not a symbolic execution tool. fold already has superior arithmetic reasoning via Z3. CodeQL's strengths (interprocedural dataflow, declarative queries) overlap with fold's taint-track detector and are not a differentiator.

---

References

Tool homepages

Tool	URL
KLEE	https://klee.github.io/
Kani	https://model-checking.github.io/kani/
Rudra	https://github.com/sslab-gatech/Rudra
MIRAI	https://github.com/facebookexperimental/MIRAI
Miri	https://github.com/rust-lang/miri
Haybale	https://github.com/trailofbits/haybale
AFL++	https://github.com/AFLplusplus/AFLplusplus
LibAFL	https://github.com/AFLplusplus/LibAFL
libFuzzer	https://llvm.org/docs/LibFuzzer.html
cargo-fuzz	https://github.com/rust-fuzz/cargo-fuzz
rev.ng	https://rev.ng/
SWAN	https://github.com/S2-group/swan

fold internal docs

Doc	What it covers
docs/internal/binary-fuzz-corpus.md	Mach-O binary → ABI inference → dlopen harness pattern
docs/internal/swift-sil-z3-corpus.md	Swift SIL operations, Z3 API reference, detector map
docs/internal/rust-frontend.md	fold-rust architecture, subprocess wire format, known limits
docs/internal/m31-phase3-concolic.md	LibAFL+symcc-rt concolic execution plan
docs/internal/library-expansion-matrix.md	Z3 and Clang feature adoption scorecard
docs/positioning.md	fold vs peer tools, confidence tiers, when to choose fold
docs/research/prior-art.md	Key papers grounding fold's design
docs/research/frontier.md	Optimization and validation tiers (T0-T4 + future)

Key papers

Paper	Relevance to this landscape
Cadar et al. (2008) KLEE: Unassisted and Automatic Generation of High-Coverage Tests	KLEE architecture and design rationale
Poeplau & Francillon (2020) SymQEMU: Compilation-based symbolic execution for binaries	Binary-level symbolic execution; alternative to rev.ng
Fioraldi et al. (2020) AFL++: Combining Incremental Steps of Fuzzing Research	AFL++ architecture; LibAFL design
Jung et al. (2020) Stacked Borrows	Miri's pointer provenance model
Astrauskas et al. (2019) Leveraging Rust Types for Modular Specification and Verification	Prusti architecture; why deductive verifiers are outside fold's scope
Vanhatalo et al. (2021) Automatic Rust Unsafe Code Analysis (Rudra)	Rudra's detector design and ecosystem impact
Toman & Grossman (2021) Concrat: Symbolic Execution for Rust	Rust-specific symbolic execution; relevant to Haybale evaluation