# M31 Phase 3 — Concolic execution scoping ## Goal Close the last gap in fold's symbolic-execution + fuzzer loop. M31 Phase 1+2 ships: - **Scan-time symbolic execution.** Z3 produces a satisfying model for every flagged sink; the model is packed as concrete bytes and written to the libFuzzer corpus. - **Runtime fuzzing.** libFuzzer mutates the seed bytes, ASan reports crashes, fold ingests the crash and promotes the corresponding Finding to `Confidence::ConcreteWitness`. What we don't do today: when libFuzzer takes a *new* path the encoder never explored (because the encoder bailed, or because the real path depends on an environmental input fold didn't model), there is no feedback. The fuzzer keeps mutating the bytes it has; fold never learns the new path predicate. Concolic execution (DART, KLEE, SymCC) closes that gap. As the target binary runs on a concrete input, a parallel symbolic interpreter tracks the path predicate. At each branch the runtime asks Z3 to negate the last branch and emit a new input that would take the sibling edge. That input goes back into the corpus. Phase 3's question is not "should we add concolic." That's the right direction once Phase 2 stabilizes. The question is **which runtime do we adopt**, given: - License: fold will be GPL-3.0 when OSS'd. LGPL runtimes are compatible if dynamically linked. - Toolchain: fold builds against LLVM 22 (Homebrew `llvm@22`). - Architecture: fold already orchestrates fuzzer children via `posix_spawn` (`src/fuzz/runner.cpp`). A concolic runtime needs to attach to the same child process. - Maintenance posture: fold is a one-developer project. Vendoring a 30k-LOC pass we'd then have to maintain against every LLVM release is not free. ## Option A — Vendor symcc-rt + write our own LLVM-22 pass [eurecom-s3/symcc](https://github.com/eurecom-s3/symcc) splits into two halves: 1. **Compiler pass** (`symcc_pass`): a clang LLVM pass that instruments each LLVM IR instruction with a call into the runtime. Currently capped at LLVM 18. 2. **Runtime** (`symcc-rt`): a shared library that maintains the symbolic shadow store, asks Z3 to solve at branches, and emits new inputs. License: the runtime is LGPL-3.0; the pass is GPL-3.0. Both compatible with fold's planned GPL-3.0. **The work this option requires:** - Port `symcc_pass` from LLVM 18 to LLVM 22. New TypedPointerType, removal of `getInt8PtrTy`, opaque pointers everywhere — a real rewrite of every `IRBuilder` call that materializes a pointer. Conservatively: 2-3 weeks of focused work, then maintenance every LLVM release. - Vendor `symcc-rt` into `third_party/symcc-rt/` and link dynamically (LGPL-compliant). - Add a meson option `-Dwith-concolic=true` that builds the pass as a `.dylib` (or `.so`) loaded via `-fpass-plugin=`. - Extend `runner.cpp` to compile the target through the instrumenting pass when `--concolic` is set, and to pick up symcc's `SYMCC_OUTPUT_DIR` so the new inputs land in the corpus. **Wins:** - Full control over instrumentation. We could specialize the pass for fold's specific needs (e.g. skip instrumentation in code reached only by paths the encoder already proved sat). - No new runtime dependency beyond what we already have (LLVM 22, Z3). - One language (C++) end-to-end. Reviewable by anyone fluent in the rest of fold. **Costs:** - 2-3 weeks of porting work plus ongoing per-LLVM-release maintenance. fold's M30 refactor took 12 sessions; this is a comparable commitment with worse ROI because the upstream doesn't move. - We absorb every SymCC bug into our issue tracker. ## Option B — LibAFL `symcc_runtime` bridge [LibAFL](https://github.com/AFLplusplus/LibAFL) is the modern AFL++ successor written in Rust. It ships a `libafl_targets::symcc_runtime` module that talks to symcc-rt over a well-defined IPC interface, plus a `concolic` feature flag and a `ConcolicTracingStage` that drives the runtime from a Rust harness. License: LibAFL is Apache-2.0/MIT dual-licensed; symcc-rt is LGPL-3.0. Both compatible with our GPL-3.0 (Apache-2.0 + GPL-3.0 = GPL-3.0; LGPL-3.0 dynamically linked stays clear). **The work this option requires:** - Add a Rust harness crate `tools/fold-concolic/` that wraps LibAFL's `ConcolicTracingStage` and exposes a CLI compatible with fold's existing `runner.cpp` argv shape. - Vendor or `Cargo.toml`-depend on `symcc-rt`. (LibAFL's docs show both vendored and FFI-build patterns.) - Extend `runner.cpp` to invoke the Rust harness as a subprocess when `--concolic` is set; ingest the inputs it produces from a designated output directory. - Manage the Rust toolchain dependency in CI (cargo + a pinned toolchain version). **Wins:** - Zero LLVM-pass maintenance. LibAFL and symcc-rt upstreams handle the toolchain churn. - LibAFL's `ConcolicTracingStage` already implements branch flipping, input minimization, and corpus integration — features we would otherwise rewrite. - Active upstream (LibAFL releases monthly; AFL++ maintainer is primary author). Bug reports flow to people who care. - Side benefit: opens a path to swap libFuzzer for LibAFL's own fuzzer in Phase 4 if we want richer scheduling. **Costs:** - A second language in the build. fold becomes "C++ for analysis, Rust for the runtime loop." CI gets a Rust toolchain. Reviewers need to know both. - Coarser instrumentation. We get whatever LibAFL+symcc-rt do — no path-aware specialization without contributing upstream. - IPC overhead between the Rust harness and the C++ fold binary. Probably negligible (the dominant cost is Z3 itself), but needs to be measured before committing. ## Recommendation **Adopt Option B (LibAFL bridge), staged in three steps.** The decisive factor is maintenance leverage. fold has one maintainer. The encoder already eats most of the available bandwidth. Owning an LLVM pass that requires forklift work every LLVM release would, over a 2-year horizon, cost more than the specialization wins. The two-language cost is real but bounded: the Rust harness is a single CLI binary the fold C++ code shells out to. The interface is argv + a directory of new inputs — the same shape `runner.cpp` already uses for libFuzzer. We do not need to learn Rust to *use* the harness, only to extend it. If specialization later becomes the bottleneck (we have evidence LibAFL+symcc-rt's default instrumentation is hurting us), the escape hatch is to upstream patches to LibAFL — much cheaper than re-porting the whole pass. ### Staging **P3.1 — Plumbing.** Wire `--concolic` through `runner.cpp` as a no-op flag. Document the contract: when set, after libFuzzer's deadline expires, fold runs a second campaign with the concolic harness, ingests new inputs from `/concolic-out/`, and adds them to the libFuzzer corpus for a final round. **P3.2 — LibAFL harness.** Add `tools/fold-concolic/` (Rust crate). One binary `fold-concolic` taking the same harness path, seed dir, and output dir as the libFuzzer runner. Wraps `ConcolicTracingStage` against symcc-rt. **P3.3 — Promotion path.** When the concolic harness produces an input that triggers an ASan crash, the existing crash-ingest pipeline (`fuzz_run_runner.cpp`) promotes the Finding to ConcreteWitness — no new ingest code; the seed source is already opaque to that stage. Each step is independently revertable and testable: P3.1 lands without LibAFL, P3.2 lands without integration, P3.3 reuses existing code. ## Scope explicitly excluded - **Replacing libFuzzer with LibAFL's own fuzzer.** Bigger rewrite, no proven win at fold's scale. Defer to Phase 4. - **Symbolic memory model upgrades** (granular byte tracking on pointer parameters). Orthogonal; tracked separately in `docs/research/frontier.md` follow-ups. - **KLEE adoption.** KLEE is GPL-2.0 (incompatible with our planned GPL-3.0 without legal review), interprets its own LLVM IR rather than running natively, and would not slot into our posix_spawn child-process model without significant glue. Re-evaluate only if symcc-rt becomes unmaintained. ## Verification checklist - [ ] License audit: confirm LibAFL Apache-2.0/MIT + symcc-rt LGPL-3.0 against fold's planned GPL-3.0. Document in `docs/licensing.md`. - [ ] Toolchain probe: confirm `cargo` is available in CI and pick a pinned Rust toolchain version (likely the latest stable; matches LibAFL's MSRV). - [ ] Build proof: `cargo build --release` of a minimal LibAFL `ConcolicTracingStage` harness against the same fixture (`tests/integration/fuzz_fixtures/null_behind_magic.c`) that Phase 1+2 already covers. - [ ] Latency baseline: measure end-to-end wall-clock for one concolic campaign on that fixture. Must not exceed a conservative budget (e.g. 30s) before we commit to wiring it into the default `fold fuzz-run` pipeline. - [ ] Reproducibility: same fixture must produce the same Finding promotion under `--concolic` as it does today under plain libFuzzer, given the same time budget. ## Open questions 1. **Determinism.** symcc-rt branches the symbolic store on every conditional. Two runs of the same harness produce different input *orders*. Does our crash-ingest pipeline care about the ordering? It shouldn't — Finding promotion matches by `finding_id` — but worth verifying with a small reproducibility test. 2. **LibAFL version pin.** LibAFL's API has historically been unstable. We should pin a specific tag in `Cargo.toml` and only bump deliberately, not on `cargo update`. 3. **Build-time impact.** Adding Rust to the build raises CI from one toolchain to two. Worth quantifying before P3.2 lands.