trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
fold/docs/research/evaluation-foundation-literature-review-2026-07-13.md
trvon 2dcbdbc75d
 feat: harden Fold quality guard 
Preserve source, binary, and runtime evidence boundaries while making precision and performance regressions reproducible.

- decompose analysis orchestration into bounded modules
- add differential, metamorphic, organic, and Yams change-time gates
- fix detector, P-Code, fuzz sanitizer, and report identity precision
2026-07-13 15:05:35 -04:00

28 KiB
Raw Permalink Blame History

Evaluation Foundation and Code-Quality Engine Literature Review

Date: 2026-07-13 Scope: reliable evaluation, DAST/concolic confirmation, analyzer architecture, and decomposition priorities for Fold as a code-quality guard for Yams.

Executive decision

Fold should use one evaluation protocol across SAST, binary heuristics, symbolic analysis, and DAST, but it should not merge their evidence models. The protocol normalizes observations and metrics; source proof, binary heuristic evidence, and concrete runtime witnesses remain separate.

The implementation shape is:

runner adapter
    -> immutable run artifact
    -> normalized observation
    -> one-to-one oracle matcher
    -> sliced metrics + stability
    -> explicit gate policy
    -> report

This separation matters. Runners should only execute tools and retain artifacts. They should not each invent matching, precision/recall formulas, finding identity, or gate thresholds.

The first implementation slice now lives in scripts/benchmarks/fold_eval/. It centralizes classification metrics, one-to-one finding matching, SARIF identity, repeated-run drift, and deterministic bootstrap intervals. The source structure ratchet is scripts/check_source_structure.py, with budgets in tests/architecture/source_budgets.json.

The foundation is now executable rather than only prescriptive. All committed benchmark manifests use schema version 1, runners can emit hash-addressed run artifacts, classification reports include micro and macro slices, and A/B performance reports use paired repetition samples when available. Two new Meson gates exercise source metamorphic relations, UBSan and ASan runtime pairs, Clang Static Analyzer differential pairs, and a provenance-pinned organic CVE subset. Runtime confirmation records reached, triggered, detected, and replayed as distinct monotonic states. The Yams runner now consumes a reviewed stable-ID disposition baseline and reports change-time deltas.

Paperbridge search record

The literature pass used Paperbridge on 2026-07-13. Searches covered “testing static analyses precision soundness,” “differential testing static analyzers,” “metamorphic testing program analyzers,” “DART directed automated random testing,” “ground-truth fuzzing reached triggered detected,” “fuzzer benchmark statistical evaluation,” and semantic clone benchmarks. Crossref and OpenAlex returned usable metadata consistently. Research/arXiv/DBLP providers timed out on part of the pass, and several publisher full-text endpoints were unavailable or returned 403 responses. Magma full text was available; other conclusions were kept to the claims supported by the retrieved abstracts and metadata.

This availability record matters for reproducibility: references below are not presented as an exhaustive systematic review. They are the directly relevant papers used to choose benchmark contracts and immediate implementation work.

Clarifying “Dart's DAST”

The relevant work is DART—Directed Automated Random Testing—not the Dart programming language. DART combines automatically generated drivers and random concrete execution with path constraints that are negated and solved to explore new paths. Its important lesson for Fold is not “symbolically execute everything.” It is to use concrete execution as the default and invoke focused constraint solving when random exploration needs help.

Fold already has the correct integration point: a static finding can become a FindingConfirmationTask. A DART-style adapter can use the finding's function, input channel, hazard, and source-side path facts to create a targeted harness. Only a replayable sanitizer violation should promote the finding to concrete-witness.

Literature findings and direct implications

Work Finding relevant to Fold Engineering implication
DART, PLDI 2005 Concrete runs and generated path constraints can cooperate to systematically explore program paths. Start with random concrete execution; selectively flip a path predicate for a targeted confirmation task.
KLEE, OSDI 2008 Symbolic execution can generate high-coverage tests and expose deep faults, but it pays for path and environment modeling. Keep KLEE/concolic work behind the confirmation-task adapter rather than making it the default source scan.
Driller, NDSS 2016; QSYM, USENIX Security 2018 Hybrid systems reserve symbolic reasoning for barriers that fuzzing does not cross efficiently. Trigger concolic assistance on a plateau or a high-priority static obligation, with a bounded solver budget.
Checkification, 2025 Static analyzer assertions can become dynamically checked runtime properties driven by random tests. Treat a Fold finding as an executable claim with an explicit runtime oracle, not merely as a location to fuzz near.
Differential Testing of Soundness and Precision of Static Analyzers, ISSTA 2019 Generated programs and assertions can expose analyzer soundness and precision defects by comparing analyzer behavior. Add a differential lane against Clang SA, compiler diagnostics, sanitizers, and selected verifiers; retain disagreements as artifacts.
Testing Static Analyses for Precision and Soundness, CGO 2020 Analyzer-testing transformations can expose both missed reports and imprecise reports without requiring a complete real-program oracle. Treat transformation validity and expected alert mapping as first-class case data; retain the transformed program and disagreement.
DynaBoost, ESEC/FSE 2021 Instrumented test executions can observe predicted dataflow behavior and improve probabilistic static-alarm ranking. Preserve dynamic observations separately from static proof, then use them to prioritize review and confirmation work.
AnnaTester, 2024 A study of 246 annotation-induced issues derived three metamorphic relations; the resulting framework found 43 new faults, 20 fixed at publication time. Add language-feature transformations derived from real analyzer failures, and test preprocessing/reporting as well as detector kernels.
Testing Dafny, ISSTA 2022 Property-based and differential techniques can test a verifier whose own proof verdict is the subject under test. Add small generated semantic programs with independently checkable runtime or compiler oracles; archive verifier disagreements.
Metamorphic Testing of Datalog Engines, ESEC/FSE 2021 Semantics-preserving transformations reveal logic-engine defects even without a complete output oracle. Add transformations such as alpha-renaming, dead safe statements, equivalent guards, and TU ordering; findings should transform predictably.
SemanticCloneBench, IWSC 2020 Semantic-clone evaluation requires labeled behavioral similarity rather than only token overlap. Report clone and equivalence quality separately and label Yams clone families before making either a blocking rule.
Evaluating Fuzz Testing, CCS 2018 Weak experimental design, insufficient trials, and unsuitable statistics can reverse apparent fuzzer conclusions. Separate PR smoke runs from comparative claims; record seeds and use repeated independent trials, robust summaries, and intervals.
SoK: Prudent Evaluation Practices for Fuzzing, IEEE S&P 2024 Fuzzing studies remain vulnerable to statistical and systematic error. Version the target, harness, tool, timeout, machine facts, and seed set in every campaign artifact.
FuzzBench, ESEC/FSE 2021 Reproducible infrastructure and common experiment definitions make fuzzer comparisons maintainable. Define a versioned Fold experiment manifest; keep runners replaceable and results comparable.
Magma, 2020 Ground-truth bug identity and reached/triggered/detected states are more informative than raw crash counts. Track bug/fact IDs and confirmation state transitions; do not equate unique crash hashes with unique vulnerabilities.
Evaluating Synthetic Bugs, 2022 Synthetic and organic bugs differ materially in difficulty and behavior. Never pool Juliet/SARD and real CVE/project results into one headline score.
CVEfixes, 2021 Vulnerability/fix pairs provide scalable real-world candidates with repository provenance. Build a small, reproducible C/C++ project subset and evaluate vulnerable and fixed revisions as paired cases.
PrimeVul, 2024 Duplication, weak labels, and unrealistic splits can make vulnerability metrics misleading. Deduplicate by project/function lineage, use chronological or project-disjoint splits, and report realistic class imbalance.
Tricorder, ICSE 2015; Lessons from Building Static Analysis Tools at Google, 2018 A common analyzer interface and change-time feedback support an analysis ecosystem developers will use. Keep detector contracts small, make findings actionable, and gate new findings at review time instead of flooding developers with repository history.
Scaling Static Analyses at Facebook, CACM 2019 Compositional per-procedure summaries enable parallel and incremental analysis at large scale. Compute shared immutable facts once, cache per-function summaries, and let detectors declare their required facts.
In Defense of Soundiness, 2015 Practical analyzers must state deliberate unsoundness and unsupported semantics explicitly. Attach modeling limitations, bailout reasons, and evidence tier to results and metric slices.

What the current Fold foundation gets right

  • Source Clang/Z3 and binary radare2/P-Code paths have distinct provenance.
  • Findings have stable IDs, confidence tiers, and confirmation-task concepts.
  • The benchmark tree includes semantic micro cases, safe near-misses, Juliet, SARD-oriented work, SV-COMP adapters, real-project runs, and resource profiles.
  • The Yams runner records the selected TU set, scan configuration, wall time, peak RSS, detector cost, Z3 queries/timeouts, and finding fingerprints.
  • Existing source golden tests put precision regressions beside recall cases.
  • Every committed benchmark manifest validates against BenchmarkCase schema version 1, and runners can retain commands, hashes, logs, reports, timing, environment, and exit status as immutable RunArtifact records.
  • The source metamorphic suite now pins alpha-renaming, harmless insertion, equivalent early-return guards, TU ordering, process fanout, and evidence ceilings. The sanitizer differential suite pins vulnerable/fixed division and signed-overflow behavior against UBSan plus OOB/UAF behavior against ASan, including deterministic replay.
  • The Clang SA differential lane retains independent analyzer logs and classifications for division and null-dereference pairs.
  • The organic lane pins adapted GStreamer, libssh2, and OpenSSL vulnerable/fixed slices with project revisions, upstream paths, licenses, references, and local hashes. Its current origin-separated recall is 1/3 with no fixed-case reports; the two misses are explicit nullable-flow gaps, not hidden passes.
  • The reviewed Yams baseline classifies 31 stable results with rationale and reports new/persisting/resolved IDs, disposition trends, changed-file scope, review coverage, and alert density.

Evaluation defects found in the review

Duplicated evaluator semantics

Several scripts independently implemented precision, recall, F1, SARIF normalization, and finding matching. This lets metrics drift while all scripts continue to “pass.” The shared fold_eval package is now the canonical home for those policies.

Inflated recall from many-to-many matching

The old group scorer allowed one finding group to satisfy multiple gold cases. The evaluator now uses deterministic maximum bipartite matching, so one emitted group receives credit at most once.

Ambiguous basename matching

The old scorer collapsed all paths to basenames. a/item.cpp could therefore match b/item.cpp. The canonical matcher preserves path suffixes when a gold case supplies a directory and retains basename compatibility only for legacy gold cases that explicitly name only a basename.

Fabricated negative populations

Many SAST corpora enumerate known positive cases but not every safe source location. Such a corpus supports TP, FP, FN, precision, and recall; it does not support a true-negative count, specificity, or false-positive rate. The shared metric API leaves TN absent unless the corpus explicitly provides it and marks undefined denominators.

Exact-hash-only reliability

An exact fingerprint says whether two result sets are identical, but says nothing about the size of partial drift. The Yams benchmark schema now includes intersection, union, churn, per-run count, and pairwise Jaccard summaries while retaining the exact fingerprint gate.

Monolith growth had no executable constraint

The production audit identified large files, but nothing prevented them from growing. The new source budget test fails if an existing monolith exceeds its ratchet or a new production C++ file exceeds 1,000 lines. The budget also emits the ranked next-extraction surface.

Evidence promotion was not detector-specific

The first executable metamorphic run found local division findings incorrectly marked as summary-backed and cross-TU corroborated. Common annotation was overwriting detector proof modes and bailout reasons, which inflated triage scores. Evidence decoration now preserves detector-specific proof metadata and only sets summary/cross-TU flags at the callsite that supplied that evidence. Unit, cross-TU, and metamorphic tests pin the distinction.

Early-return summary flow was inverted

The sanitizer vulnerable/fixed differential lane found a false positive for an ordinary if (denominator == 0) return 0; guard. Summary encoding retained the condition path instead of its fallthrough negation when an if had no else. The branch merge is corrected, and symbolic-summary, detector, cross-TU, and Fold-versus-UBSan tests retain the fixed program as an explicit negative.

Host timing could replace the child's exit status

On macOS, /usr/bin/time -l can fail while reading restricted kernel data even when the child succeeds. Benchmark runners now use portable time -p on macOS, preserve the analyzed process status, and report external RSS as unavailable instead of fabricating it. Fold's internal profile remains the Yams RSS source.

Fold Evaluation Protocol v2

1. Case types

Every benchmark case must declare one of these oracle forms:

Case type Oracle
Positive semantic micro-case exact expected fact/finding identity and allowed evidence tiers
Negative near-miss explicitly safe construct and forbidden finding family
Vulnerable/fixed pair finding expected on vulnerable revision and absent or refuted on fixed revision
Metamorphic case transformation plus expected identity/location mapping or invariant metric
Differential case expected agreement, or an intentionally unresolved disagreement artifact
Dynamic confirmation hazard oracle, input channel, sanitizer/runtime checker, and replay command
Real-project advisory reviewed outcome: actionable, duplicate, accepted risk, unsupported, or false positive

2. Case metadata

A versioned case should preserve:

case_id
corpus_id and corpus_version
origin: synthetic | organic | revived | mutated | metamorphic
language and frontend
backend under evaluation
CWE/property/detector
positive or enumerated-negative oracle
expected file/function/range or artifact address
expected evidence floor and allowed confidence ceiling
vulnerable/fixed lineage when applicable
unsupported-language/model features

Synthetic, organic, and transformed cases are reported as separate strata even when they exercise the same detector.

3. Immutable run artifact

The runner records inputs and execution; it does not score them:

experiment_id and schema version
Fold revision/build configuration
target revision and compile-database fingerprint
full command and detector configuration
machine/OS/compiler/sanitizer versions
timeout, memory, process, and solver budgets
seed or seed-set identity
stdout/stderr, raw JSON/SARIF, profile, witnesses, and crashes
start/end time and exit status

4. Observation and matching

Normalize each result into an observation with backend, rule, confidence, artifact, function/address, source region when present, message, fact/finding ID, and evidence links. Matching is one-to-one between observations/groups and gold cases. Locationless binary and crash observations use artifact, function, kind, and address/input identity instead of being discarded.

5. Metrics

Always report counts next to ratios. Required slices are detector/property, backend, confidence tier, corpus origin, language/frontend, and confirmation state.

  • TP, FP, FN, precision, recall, F1 where the oracle supports them.
  • TN, specificity, and FPR only for explicitly enumerated negatives.
  • Micro and macro averages; never only a pooled headline.
  • Unsupported, timeout, bailout, and unknown counts outside TP/FP/FN.
  • Exact stability plus intersection, union, churn, and pairwise Jaccard.
  • Wall time, peak RSS, frontend time, detector time, query count, timeout count, and cache hit rate.
  • For dynamic runs: reached, triggered, detected, replayed, time to each state, and unique ground-truth bug IDs.
  • For developer workflow: new alerts/KLOC, accepted/fixed/dismissed counts, time to disposition, and change-time finding density.

6. Randomized experiment policy

PR smoke runs may use three fixed seeds to catch crashes and gross regressions, but they make no comparative performance claim. Nightly or release comparisons use at least 20 independent seeds per target/configuration as the initial Fold policy, publish every seed, and report median, IQR, and a bootstrap interval. Where two configurations are compared, add an effect size and a test chosen before examining the results. A timeout is an observation, not silently missing data.

7. Gates are separate from measurements

Gate policy consumes metric output. It does not live in runners or scorers. Suggested Yams gates are:

  • no new proved or concrete-witness finding in changed code;
  • no regression on curated negative near-misses;
  • no loss of an existing positive golden without an explicit baseline review;
  • exact deterministic finding identity for non-random source runs;
  • no backend-provenance loss;
  • no increase in Z3 timeouts beyond the declared budget;
  • no source-size ratchet violation;
  • performance regression thresholds only against the same TU/configuration fingerprint.

DART-style confirmation design for Fold

static finding
  -> confirmation task
  -> harness/input model
  -> seeded concrete execution under sanitizer/runtime oracle
  -> branch trace and reached/triggered state
  -> [plateau or targeted barrier] negate one relevant predicate
  -> bounded solve and new concrete input
  -> replay in a fresh process
  -> concrete-witness | refuted-under-model | timeout | unsupported

The first adapter should target div-by-zero and signed integer overflow because their runtime oracles map directly to UBSan and their inputs are easier to model than arbitrary pointer graphs. ASan remains enabled for memory hazards. The fuzz compiler should therefore support an explicit sanitizer set instead of a hard-coded fuzzer/address pair.

Precision rules:

  • A crash is not automatically the predicted finding. Correlation uses the confirmation task's finding/fact ID plus kind and artifact/function evidence.
  • A witness is promoted only after deterministic replay with the same input.
  • A source task may corroborate a binary heuristic, but raw binary P-Code evidence alone remains heuristic.
  • Refutation is scoped to the harness and bounds; it must not silently erase the static finding.
  • Solver-derived inputs, seeds, branch choices, sanitizer output, and replay command are retained as artifacts.

Modular production architecture

Scan runner
  |- source pipeline
  |    |- TU runner
  |    |- immutable AnalysisFacts
  |    |- detector plan/registry
  |    |- local detector workers
  |    `- global/cross-TU aggregators
  |- binary pipeline (separate facts/evidence)
  `- report/profile decorators

AnalysisFacts should expose immutable CFG, call graph, summary, def-use, fingerprint, and reusable range/alias facts. A detector declares its required facts, expected cost class, evidence policy, and whether it is local or global. This permits sharing computations without merging detector semantics or source and binary lanes.

Decomposition sequence

  1. Done: extract BatchSafetyObserver from security_walker.cpp; test deferred hooks, immediate stateful hooks, and deadline behavior.
  2. Done: backend enrichment/dispatch now lives in backend_shard_runner.cpp, incremental source fingerprinting lives in incremental_fingerprint.cpp, symbolic-summary SCC/fixpoint priming lives in source_summary_pipeline.cpp, call-graph collection and conservative virtual/indirect resolution live in source_call_graph.cpp, TU quarantine persistence lives in tu_quarantine.cpp, and per-TU detector execution lives in source_tu_runner.cpp. A shared SourceTuRunState replaces the 17-counter constructor chain, while finding_evidence.cpp centralizes deterministic evidence annotation. Together these seams reduce scan_runner.cpp from 3,266 to 850 lines, below the 1,000-line gate.
  3. Done: security_walker.cpp is a 355-line facade over analysis, contracts, refinement, engine-core, and engine-control modules. The batch observer remains independent, and direct analysis tests pin guard/loop helpers in addition to the detector regressions.
  4. Done: encoder.cpp is a 215-line dispatcher over foundation, operator, expression, and expression-arm modules. Symbolic encoder and detector tests preserve bailout, array, non-null, phi, and summary behavior.
  5. Done: r2_backend.cpp is an 827-line orchestrator over session/command transport, serialization/classification, pure disassembly state machines, and extraction. Binary findings remain heuristic at the assembly boundary.
  6. Done: div-by-zero, null-deref, integer-overflow, and OOB files are below the 1,000-line target with candidate/fact or analysis helpers extracted. tests/architecture/source_budgets.json now has no exceptions.

Each extraction must be behavior-preserving under source goldens, safe near-misses, finding fingerprints, profile counters, and the full suite. New capability work should enter through the extracted contract rather than adding another branch to a monolith.

The final binary-golden pass converted two integration defects into permanent guards. A guarded machine division had been reintroduced by an inverted high P-Code branch predicate even though the raw lift was safe; instruction-level null/arithmetic findings now originate only from the raw lane. A broad security scan also classified the same embedded secret through both binary-security and hardcoded-string; the latter now runs only when selected explicitly (or under the default all-detector scan). The portable guarded-div and hardcoded-secret goldens pin both policies.

Near-term benchmark backlog

  1. Done: add versioned BenchmarkCase and RunArtifact schemas; migrate all committed benchmark manifests while retaining a legacy-reader boundary.
  2. Done for the first organic slice: add adapted vulnerable/fixed GStreamer, libssh2, and OpenSSL cases with pinned project revisions, source paths, references, licenses, and local hashes. Expand with buildable full-project snapshots separately; do not relabel adaptations as pristine sources.
  3. Done: add source metamorphic tests for identifier renaming, harmless statement insertion, equivalent guard rewriting, TU order, and process count.
  4. Done for the first comparator classes: Fold-versus-UBSan, Fold-versus-ASan, and Fold-versus-Clang-SA vulnerable/fixed assertions are executable and retain independent commands, logs, timing, and classifications.
  5. Done for the first runtime oracle classes: the fuzzer compiler supports UBSan, division/signed-overflow fixtures preserve sanitizer class, and the ASan lane covers stack OOB and heap UAF with deterministic replay.
  6. Done: confirmation results distinguish reached, triggered, detected, and replayed states and report time/count summaries.
  7. Pending: add DART-style predicate flipping only for targeted confirmation tasks or campaigns that have plateaued.
  8. Done for the reviewed metadata slice: Yams change-time reporting includes new, persisting, and resolved IDs, alert density, per-finding disposition, changed-file scope, and resolved/disposition trends. Broader Yams paths still require review before becoming blocking.

References