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
478 lines
28 KiB
Markdown
478 lines
28 KiB
Markdown
# 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:
|
|
|
|
```text
|
|
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:
|
|
|
|
```text
|
|
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:
|
|
|
|
```text
|
|
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
|
|
|
|
```text
|
|
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
|
|
|
|
```text
|
|
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
|
|
|
|
- Patrice Godefroid, Nils Klarlund, and Koushik Sen. “DART: Directed Automated
|
|
Random Testing.” PLDI 2005. https://doi.org/10.1145/1065010.1065036
|
|
- Cristian Cadar, Daniel Dunbar, and Dawson Engler. “KLEE: Unassisted and
|
|
Automatic Generation of High-Coverage Tests for Complex Systems Programs.”
|
|
OSDI 2008. https://www.usenix.org/conference/osdi-08/klee-unassisted-and-automatic-generation-high-coverage-tests-complex
|
|
- Nick Stephens et al. “Driller: Augmenting Fuzzing Through Selective Symbolic
|
|
Execution.” NDSS 2016. https://doi.org/10.14722/ndss.2016.23368
|
|
- Insu Yun et al. “QSYM: A Practical Concolic Execution Engine Tailored for
|
|
Hybrid Fuzzing.” USENIX Security 2018.
|
|
https://www.usenix.org/conference/usenixsecurity18/presentation/yun
|
|
- Daniela Ferreiro, Ignacio Casso, Jose F. Morales, Pedro López-García, and
|
|
Manuel V. Hermenegildo. “Checkification: A Practical Approach for Testing
|
|
Static Analysis Truths.” 2025. https://doi.org/10.1017/S1471068425100069
|
|
- Christian Klinger, Maria Christakis, and Valentin Wüstholz. “Differential
|
|
Testing of Soundness and Precision of Static Analyzers.” ISSTA 2019.
|
|
https://doi.org/10.1145/3293882.3330553
|
|
- Jubi Taneja, Zhengyang Liu, and John Regehr. “Testing Static Analyses for
|
|
Precision and Soundness.” CGO 2020.
|
|
https://doi.org/10.1145/3368826.3377927
|
|
- Tianyi Chen, Kihong Heo, and Mukund Raghothaman. “Boosting Static Analysis
|
|
Accuracy with Instrumented Test Executions.” ESEC/FSE 2021.
|
|
https://doi.org/10.1145/3468264.3468626
|
|
- Huaien Zhang, Yu Pei, Shuyun Liang, and Shin Hwei Tan. “Understanding and
|
|
Detecting Annotation-Induced Faults of Static Analyzers.” FSE 2024.
|
|
https://doi.org/10.1145/3643759
|
|
- Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamarić, Neha Rungta, and
|
|
Emina Torlak. “Testing Dafny (Experience Paper).” ISSTA 2022.
|
|
https://doi.org/10.1145/3533767.3534382
|
|
- Numair Mansur, Maria Christakis, and Valentin Wüstholz. “Metamorphic Testing
|
|
of Datalog Engines.” ESEC/FSE 2021. https://doi.org/10.1145/3468264.3468573
|
|
- Farouq Al-Omari, Chanchal K. Roy, and Tonghao Chen. “SemanticCloneBench: A
|
|
Semantic Code Clone Benchmark Using Crowd-Source Knowledge.” IWSC 2020.
|
|
https://doi.org/10.1109/IWSC50091.2020.9047643
|
|
- George Klees et al. “Evaluating Fuzz Testing.” CCS 2018.
|
|
https://doi.org/10.1145/3243734.3243804
|
|
- Moritz Schloegel et al. “SoK: Prudent Evaluation Practices for Fuzzing.” IEEE S&P 2024.
|
|
https://doi.org/10.1109/SP54263.2024.00137
|
|
- Jonathan Metzman et al. “FuzzBench: An Open Fuzzer Benchmarking Platform and
|
|
Service.” ESEC/FSE 2021. https://doi.org/10.1145/3468264.3473932
|
|
- Ahmad Hazimeh et al. “Magma: A Ground-Truth Fuzzing Benchmark.”
|
|
https://doi.org/10.1145/3428334
|
|
- Joshua Bundt, Andrew Fasano, Brendan Dolan-Gavitt, William Robertson, and Tim
|
|
Leek. “Evaluating Synthetic Bugs.”
|
|
https://doi.org/10.1145/3433210.3453096
|
|
- Guru Bhandari, Amara Naseer, and Leon Moonen. “CVEfixes.”
|
|
https://doi.org/10.1145/3475960.3475985
|
|
- Yangruibo Ding et al. “Vulnerability Detection with Code Language Models: How
|
|
Far Are We?” https://arxiv.org/abs/2403.18624
|
|
- Caitlin Sadowski et al. “Tricorder: Building a Program Analysis Ecosystem.”
|
|
ICSE 2015. https://doi.org/10.1109/ICSE.2015.76
|
|
- Caitlin Sadowski et al. “Lessons from Building Static Analysis Tools at
|
|
Google.” https://doi.org/10.1145/3188720
|
|
- Dino Distefano et al. “Scaling Static Analyses at Facebook.”
|
|
https://doi.org/10.1145/3338112
|
|
- Michael D. Ernst and Anders Møller. “In Defense of Soundiness.”
|
|
https://doi.org/10.1145/2644805
|