4.3 KiB
Research
Architecture
fold is a bounded symbolic SAST built on a backend-neutral scan shell plus the source-analysis stack:
- Analysis backend:
AnalysisBackenddiscovers analysis units and extractsFunctionIR.ClangBackendwraps the source path;R2Backendis the prototype binary path using radare2. - Clang frontend: LibTooling parses C++ into AST. Frontend actions fan out to all enabled detectors in a single TU pass.
- Symbolic encoder: translates AST expressions to Z3 BV-64. Path predicate accumulates through branches. BV-64 signedness-aware widening (zext unsigned, sext signed). SSA renaming per function. Phi symbols at if/else joins.
- Observer detectors: encoder fires hooks (
onBinaryArith,onPointerDeref,onLibraryCall,onCallExpr,onBufferCopy) on hazard-relevant IR nodes. Detectors implement observers and query Z3 under path constraints.
The backend seam lives in include/fold/core/analysis_backend.hpp. Source scans
still delegate to the mature Clang detector pipeline. Binary scans currently
produce heuristic findings directly from radare2-discovered strings, calls, and
pseudocode; they do not yet lift binary functions into the symbolic source IR.
The planned source/binary scan router and hybrid CLI contract are specified in
docs/research/cli-router.md.
radare2 integration prefers linked libr_core (-Dradare2=enabled) and falls
back to invoking r2 when the development libraries are absent. This gives a
path to pinned/vendored radare2 builds without coupling normal source scans to a
large third-party tree.
Cross-function: CrossTUCache shares callee properties (deref params, null-return,
divisor params) across TUs. SummaryStore provides leaf-function symbolic return
substitution. IncrementalCache fingerprints functions for --incremental skip.
Heap model: HeapModel tracks per-malloc regions with freed state, byte offsets,
and allocation-site metadata. UaF/double-free through OOB observer.
Key design decisions: QF_BV logic only, assumption-based check(1, &hazard),
push/pop branch scoping, k=3 default loop unroll with post-loop havoc, per-function
solver lifetime, expression canonicalization cache.
Crash isolation: non-incremental, non-profile source scans use an OS worker
process even when --processes 1 is requested. Workers emit a file_finished
record after each TU. If a worker exits or receives a fatal signal, the parent
retains findings from completed TUs, quarantines the first unfinished TU, and
restarts the remaining shard in a clean process. Quarantine records use
<path>\tworker-exit:<status> or <path>\tsignal:<number> so ordinary frontend
failures are not mislabeled as timeouts. The loader remains compatible with the
legacy <path>:<signal> form. Incremental and profile scans currently retain
the in-process per-TU runWithSignalIsolation fallback because their shared
index/profile state is not worker-mergeable yet. The set of known asserting
Clang APIs and installed precondition gates is catalogued in
docs/research/clang-quirks.md.
Juliet Benchmarks (2026-05-15 final, with all optimizations)
| CWE | Detector | Gold | TP | Precision | Recall | CSA Recall | Queries |
|---|---|---|---|---|---|---|---|
| 476 | null-deref | 364 | 184 | 68.7% | 50.5% | 56.0% | 876 |
| 369 | div-by-zero | 938 | 576 | 57.5% | 61.4% | 5.8% | 3222 |
| 190 | int-overflow | 4178 | 1851 | 57.6% | 44.3% | 0.0% | 8849 |
| 121 | oob-access | 5252 | 466 | 61.2% | 8.9% | 6.2% | 5855 |
Total scan time: 741s (12m 21s). Total TP: 3,077.
Soundness
BV-64 encoding sound for the bounded model (k-unrolled). Every BailReason
replaces the expression with an unconstrained fresh symbol — sound but imprecise.
Completeness class: loop-free, integer-only, no-heap, no-call leaf functions.
Within this class, fold has zero false negatives. Proof in soundness.md.
Yams Audits
- 2026-05-13 (baseline, 8 detectors): 55K raw findings, 0 TPs on manual review. clone: 6833, equiv: 12, dead: 4, class-dup: 0, dead-statement: 3184, unused-function: 181.
- 2026-05-14: FP roadmap quick-wins (type filter, per-emission dedup, constant-fold literal divisors, null-deref observer rewrite). Findings dropped ~50%. Encoder recursion discovered and fixed via RAII depth guard.