81 lines
4.3 KiB
Markdown
81 lines
4.3 KiB
Markdown
# 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.
|