fold/docs/research/architecture.md

4.3 KiB

Research

Architecture

fold is a bounded symbolic SAST built on a backend-neutral scan shell plus the source-analysis stack:

  1. Analysis backend: AnalysisBackend discovers analysis units and extracts FunctionIR. ClangBackend wraps the source path; R2Backend is the prototype binary path using radare2.
  2. Clang frontend: LibTooling parses C++ into AST. Frontend actions fan out to all enabled detectors in a single TU pass.
  3. 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.
  4. 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.