trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix audit findings: soundness, coverage reporting, docs, and review follow-ups #1

Merged
trevon merged 18 commits from fix/audit-findings into master 2026-09-25 06:48:08 +00:00
Conversation 0 Commits 18 Files changed 81 +17 -12
1 changed files with 17 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files
Showing only changes of commit c785a6acee - Show all commits

docs(positioning): drop claims the code and evidence do not support

Prev Next 
Problem: docs/positioning.md claimed four confidence tiers (there are
five, including Latent) and defined Proved as any Z3 SAT, which
contradicts soundness.md's exact-model requirement. It claimed "fold
scans a 100k-LOC codebase in minutes" with no committed benchmark (the
audit measured 2 files in 5.9 s at 407 MB RSS). It described CBMC as
asking Z3/MathSAT (its default back end is SAT) and as scaling poorly
past a few thousand lines, without support. It claimed a scan-to-fuzz
loop "no other open-source analyzer covers" and "no commercial vendor
ships" (directed and hybrid fuzzers such as AFLGo and SAVIOR cover
related ground, and prior-art.md cites that line of work). It said most
analyzers "stop at SAT", ignoring the Clang Static Analyzer's Z3
refutation.

Fix: five tiers with Latent defined; Proved requires an exact bounded
model; the CBMC comparison describes the method and fold's real scope
(per-sink, mostly intraprocedural, unroll 5) instead of speed; the
uniqueness claims now describe the loop without exclusivity; CSA's Z3
refutation is acknowledged. The README is left for a separate docs pass.
trvon 2026-09-24 20:58:26 -06:00
commit c785a6acee
Signed by: trevon
GPG key ID: 38686EA797D7A8A7

29
docs/positioning.md
View file

@ -11,20 +11,23 @@ sink with a Z3-produced witness, then optionally runs that witness
through libFuzzer + ASan to promote findings from "the solver says SAT"
to "we observed the crash."
Most static analyzers stop at "the solver says SAT." Most fuzzers don't
know what they're aiming at. fold links the two so the report says
Solver-backed analyzers (for example the Clang Static Analyzer's
optional Z3 refutation) use SMT to prune infeasible paths, but their
reports stop at a static verdict. Most fuzzers don't know what they're
aiming at. fold links the two so the report says
which findings are confirmed observable failures, not just satisfiable
path predicates.
## Confidence tiers fold reports
Findings are not all equal. fold reports four confidence tiers:
Findings are not all equal. fold reports five confidence tiers:
| Tier | Source | Example |
|------------------|--------------------------------------------------------------|-------------------------------------------------|
| `Syntactic` | AST pattern match, no solver | "function name matches `strcpy`" |
| `Heuristic` | Solver gave up or path was over-approximated | "interval analysis can't bound `len`" |
| `Proved` | Z3 returned SAT on (path ∧ hazard); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" |
| `Latent` | Proved in the callee, modulo a caller obligation not discharged | "`p` is dereferenced; no caller shown to pass null" |
| `Proved` | Z3 returned SAT on (path ∧ hazard) over an exact bounded model (no over-approximated operation on the path; see `docs/research/soundness.md`); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" |
| `ConcreteWitness`| Z3 model was packaged as a seed and ASan observed the crash | "libFuzzer crashed on `seed_8f3c.bin`" |
The ordering is explicit in `include/fold/report/finding.hpp::confidenceRank()`
@ -100,7 +103,7 @@ source, closed methodology, opaque false-positive rates.
**fold differs by:** open source (GPL-3.0 when stable), open
methodology (`docs/research/soundness.md`), and a closed loop with
libFuzzer that no commercial vendor currently ships. fold is also
libFuzzer in the same report. fold is also
substantially less mature on the heuristic-refinement side — Coverity
has had two decades of FP-tuning effort that fold has not.
@ -133,15 +136,16 @@ is already your CI surface.
### Bounded model checkers (CBMC, ESBMC)
Unroll loops to a configurable depth, encode the bounded program
as an SMT formula, ask Z3 / MathSAT whether any sink is reachable.
as a SAT/SMT formula (CBMC's default back end is a SAT solver) and
ask whether any assertion can fail.
Sound for the unrolling depth chosen; report concrete
counterexamples; usable as software-verification competitors
(SV-COMP). Slow on large codebases — full-program BMC scales
poorly past a few thousand lines.
(SV-COMP). Whole-program BMC cost grows with program size and
unwinding depth.
**fold differs by:** scope and product shape. CBMC verifies one
property of one bounded program; fold scans a 100k-LOC codebase
in minutes, flagging per-sink findings with per-sink witnesses,
property of one bounded program; fold runs per-sink, mostly
intraprocedural queries with a small loop unroll (5 by default),
trading verification rigor for breadth. They are
complementary: a fold finding worth deep verification can be
re-checked under CBMC.
@ -227,8 +231,9 @@ for protocol parsers and other constrained-input APIs.
## Where fold's closed scan→fuzz loop matters
The Phase 1+2 work in M31 closed a gap that no other open-source
analyzer covers: every SAT finding is automatically packaged as a
The Phase 1+2 work in M31 closes the loop inside one tool (directed
fuzzers such as AFLGo and hybrid tools such as SAVIOR explore related
ground; see `docs/research/prior-art.md`): every SAT finding is automatically packaged as a
libFuzzer seed, run under ASan, and (if a crash is observed)
promoted from `Proved` to `ConcreteWitness` in the same JSON
report. The user sees one Finding with `confidence: