3f1234f7bb
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.
34 lines
1.2 KiB
Markdown
34 lines
1.2 KiB
Markdown
# 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)
|