226 lines
9.5 KiB
Markdown
226 lines
9.5 KiB
Markdown
# 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 `<workdir>/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.
|