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.

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:

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:

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.