fold/docs/research/sast-dast-symbolic-roadmap.md

# Fold SAST / DAST / Symbolic Roadmap

> Date: 2026-06-02
> Scope: roadmap after recent Ghidra/P-Code, gadget, ROP-chain, and vendor-pruning work.

Fold should evolve as a **three-lane vulnerability engine** rather than one monolithic analyzer.
The lanes share reports and provenance, but keep their evidence separate.

```text
Source C/C++ ── Clang AST/CFG ──▶ Source facts ─┐
                                                │
Binary ── LIEF/r2 metadata + Ghidra P-Code ───▶ Binary facts ─┐
                                                              ▼
                         Fold fact/graph layer + symbolic obligations
                                                              │
                                                              ▼
                                  Z3 bounded proof / heuristic finding
                                                              │
                                                              ▼
                         Existing + generalized confirmation layer
                         confirm runner / libFuzzer+ASan / KLEE / SymCC / angr
```

## Lane 1 — Source SAST

Keep Clang as the source of truth for C/C++ semantics. Detectors should move toward
this pipeline:

1. cheap AST/fact prefilter;
2. graph/data-flow query;
3. bounded Z3 proof obligation;
4. optional dynamic confirmation.

References:

- Clang Static Analyzer: https://clang.llvm.org/docs/ClangStaticAnalyzer.html
- Clang data-flow analysis intro: https://clang.llvm.org/docs/DataFlowAnalysisIntro.html
- CodeQL C/C++ library/data flow: https://codeql.github.com/docs/codeql-language-guides/codeql-library-for-cpp/
- Code Property Graphs: https://www.ieee-security.org/TC/SP2014/papers/ModelingandDiscoveringVulnerabilitieswithCodePropertyGraphs.pdf

## Lane 2 — Binary SAST

Keep binary evidence separate from source evidence.

| Tool | Fold role |
|---|---|
| r2 | fast fallback extraction: functions, strings, xrefs, rough metadata |
| LIEF | stable ELF/PE/Mach-O metadata candidate |
| Ghidra/SLEIGH | binary instruction semantics through raw/high P-Code |
| Capstone | gadget byte-window discovery only; not semantic proof |

References:

- Ghidra P-Code: https://ghidra.re/ghidra_docs/languages/html/pcoderef.html
- Ghidra SLEIGH: https://ghidra.re/ghidra_docs/languages/html/sleigh.html
- LIEF C++ API: https://lief.re/doc/latest/api/cpp/index.html
- radare2 book: https://book.rada.re/intro/overview.html

## Lane 3 — DAST / concolic confirmation

Fold already has two concrete confirmation surfaces:

- `fold confirm`: deeper bounded symbolic confirmation for selected findings,
  with optional SV-COMP GraphML witnesses.
- `fold fuzz prep` + `fold fuzz run`: emits `findings.predicted.json`, compiles
  libFuzzer/ASan harnesses, matches ASan crashes back to `Finding.id`, and
  promotes matching findings to `Confidence::ConcreteWitness`.

Fold should not become KLEE, angr, or a web scanner. The shipped confirmation
paths now also have a shared machine-readable `FindingConfirmationTask` /
`FindingConfirmationResult` model, plus compatibility sidecars for the fuzz path.
The remaining design work is to deepen adapter coverage and attach stable fact
IDs at more detector emission sites.

Suggested schema:

```text
FindingConfirmationTask {
  finding_id: string
  backend: source | binary | hybrid
  lane: clang | ghidra-pcode | r2-heuristic | lief-metadata
  target: { file_or_binary, function, source_location?, binary_address? }
  input_channel: argv | stdin | file | env | socket | harness | unknown
  controlled_values: [name_or_register]
  path_predicate: textual-or-SMTLIB summary
  hazard: div-by-zero | null-deref | overflow | oob | uaf | taint-sink | rop-reachable
  expected_violation: string
  suggested_adapter: klee | symcc | libfuzzer | afl | angr | triton | manual
  artifacts: [seed, harness, compile_db, binary]
}
```

Result states should align with Fold's existing confidence model:

```text
syntactic -> heuristic -> proved -> concrete-witness
                         ↘ refuted | timeout | unsupported
```

`ConcreteWitness` is already first-class: a SAT-feasible/static finding was run
under ASan/libFuzzer and produced a matching crash. New adapters should preserve
that semantics instead of creating a parallel confidence vocabulary.

KLEE is the next source-confirmation adapter family. A narrow optional prototype
now consumes a `FindingConfirmationTask`, compiles a source artifact to LLVM
bitcode, runs KLEE when installed, and writes a `FindingConfirmationResult`.
Absent KLEE skips cleanly. The current smoke path is
`tests/confirmation/klee/run_klee_smoke.sh`.

References:

- KLEE: https://www.usenix.org/conference/osdi-08/presentation/klee-unassisted-and-automatic-generation-high-coverage-tests-complex
- SymCC: https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau
- S2E: https://dl.acm.org/doi/10.1145/2110356.2110358
- Driller: https://www.ndss-symposium.org/wp-content/uploads/2017/09/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf
- QSYM: https://www.usenix.org/conference/usenixsecurity18/presentation/yun
- angr: https://docs.angr.io/en/latest/
- Triton: https://triton-library.github.io/

## Benchmark plan

| Benchmark | Purpose |
|---|---|
| Juliet C/C++ | source SAST CWE recall/precision |
| SV-COMP | verifier discipline and witness style |
| CGC | binary/concolic exploration |
| Magma | fuzz/DAST reached-vs-triggered bug metrics |

References:

- Juliet/SARD: https://samate.nist.gov/SARD/test-suites/112
- SV-COMP benchmarks: https://sv-comp.sosy-lab.org/2025/benchmarks.php
- Magma: https://hexhive.epfl.ch/magma/

## Near-term implementation order

1. Harden the current ROP planner correctness issues. **Done.**
2. Guard executable-section extraction by host memory, not fixed byte caps, so gadget scans preserve precision whenever the hardware can support the image. **Done.**
3. Add `FindingConfirmationTask` as a report/schema concept over the existing
   `confirm` and `fuzz prep/run` paths. **Done: see `include/fold/confirm/confirmation_task.hpp`.**
4. Add optional KLEE/SymCC/angr adapters that consume the same task schema.
   **KLEE smoke prototype done; SymCC/angr remain open.**
5. Define stable fact IDs before Souffle. **Done for the model: see
   `include/fold/ir/fact_id.hpp`; broader detector emission-site population remains open.**
6. Harden binary P-Code false-positive controls for common libc and guarded-arithmetic cases.
   **Done for the first curl-derived regressions and follow-up path-order cases:** P-Code call
   semantics now preserve fortified `_chk` wrappers, SSA sink naming trusts raw call-site
   correlation instead of synthesized target fallbacks, raw div/rem findings are gated by machine
   division instruction addresses, and bounded forward P-Code path exploration forks `CBRANCH`
   taken/fallthrough paths while stopping local fallthrough on forward `BRANCH`/`RETURN`. A full
   basic-block CFG with joins remains future precision work.

## Status audit — 2026-06-03

Completed or substantially implemented:

- Source, binary, and confirmation lanes remain separate in implementation and report provenance.
- Confirmation task/result schema exists and is used by `confirm` and `fuzz prep/run` sidecars.
- KLEE smoke adapter exists and skips cleanly when unavailable.
- Stable fact ID model exists.
- ROP planner/gadget extraction has focused regression coverage.
- Binary P-Code curl-smoke false positives from `memchr`/`memcpy`, fortified `strncpy_chk`,
  guarded `udiv`, taken-target ordering, and branch-skipped fallthrough hazards are covered by
  unit tests and the `/usr/bin/curl` smoke scan.
- Latent/precondition evidence is now produced by null/div detector paths, not only serialized in
  JSON/SARIF.
- Hybrid profile merging preserves lane timing/counter fields, keeping source and binary lanes
  separately measurable in merge-only hybrid mode.

Future expansion ideas, not required for the current shipped scope:

- SymCC and angr adapters over the shared confirmation task/result schema. The shipped
  confirmation lane is already useful with `confirm`, `fuzz prep/run`, and optional KLEE smoke.
- Broader fact ID population at additional detector emission sites. The current fact ID model is
  in place; expanding coverage is incremental provenance work.
- Reproducible benchmark harness scripts for Juliet, SV-COMP, CGC, and Magma. These are evaluation
  infrastructure, not core feature blockers.
- Full P-Code basic-block CFG/path exploration with join policies. The shipped binary lane now has
  bounded forward path exploration for observed false positives and block-order regressions; full
  CFG joins remain a precision upgrade, not a prerequisite.

## Guardrails

- Do not route decompiled C from binaries through source detectors.
- Do not let dynamic confirmation erase unconfirmed static findings; report it as a separate state.
- Keep binary metadata, binary semantics, source semantics, and dynamic witnesses separately measurable.
- Every finding and confirmation task must preserve backend/lane provenance.
- Keep `confirmation.tasks.json` and `confirmation.results.json` sidecars compatible with legacy `findings.predicted.json` and augmented findings JSON.