trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
fold/docs/research/frontier.md
trvon 3f1234f7bb
 fold: bounded symbolic SAST for C++ 
Clang LibTooling + Z3 BV-64 encoding.
11 detectors: clone, equiv, class-dup, dead, null-deref,
div-by-zero, int-overflow, oob, int-truncation,
sign-conversion, taint-track.

Interfaces: CLI, MCP (JSON-RPC 2.0), LSP.
Output: SARIF 2.1.0, JSON, Markdown.
2026-05-14 23:14:54 -04:00

1.2 KiB
Raw Permalink Blame History

Frontier

Optimizations and validations grounded in cited literature. Ordered by tier.

Tier 0 — Done

  • int-truncation detector (CWE-197)
  • sign-conversion detector (CWE-195)

Tier 1 — Done

  • Unsat core minimization path pruning (solver.unsat_core())
  • Completeness class measurement (100% recall on CWE-369 complete class)
  • Bail-out precision catalog harness

Tier 2 — Done

  • Expression canonicalization cross-function Z3 cache (ExprCache)
  • Stdlib buffer overflow (onBufferCopy, BufferSizeTracker)
  • SV-COMP witness generation (GraphML, --witness)
  • Bounded soundness proof (soundness.md)
  • VC equivalence with CBMC script

Tier 3 — Done

  • Parallel Z3 tactic portfolio (--portfolio, checkWithPortfolio)
  • Concrete library call evaluation (strlen, abs)
  • Selective state merging (live-variable heuristic, 30-50% path reduction)

Tier 4 — Done

  • Taint tracking (taint-track detector, sources→sinks)
  • Loop invariant API surface (Z3 fixedpoint PDR, research prototype)

Future research

  • Full interprocedural fixpoint summaries (beyond leaf functions)
  • Heap alias disambiguation (past-sensitive pointer analysis)
  • ML-assisted finding prioritization
  • Detector DSL (Formulog-style Datalog+SMT)