73 lines
3.3 KiB
Markdown
73 lines
3.3 KiB
Markdown
# Z3 Surface Vendor Decision Record
|
|
|
|
> Date: 2026-05-31; updated after Ghidra/P-Code integration work.
|
|
> Reading list: `docs/research/vendor-library-study-2026-05-31.md`.
|
|
|
|
## Problem
|
|
|
|
Fold's Z3-backed source path already has observer hooks and bounded symbolic
|
|
queries. The binary path historically relied on r2 metadata and heuristics. The
|
|
risk was adding multiple vendor IRs directly to detectors, creating duplicated
|
|
logic and unclear provenance.
|
|
|
|
## Decision
|
|
|
|
Use a small, explicit vendor surface:
|
|
|
|
1. **Ghidra/SLEIGH for binary semantics.** Map raw/high P-Code into Fold's binary
|
|
hazard and summary path.
|
|
2. **LIEF for binary metadata, if/when r2 metadata becomes the bottleneck.** LIEF
|
|
should produce file-structure facts only.
|
|
3. **Souffle for derived facts after stable MidIR/fact IDs.** It should consume
|
|
Fold-owned facts, not vendor-specific ASTs or LLVM objects.
|
|
|
|
RetDec, Remill/McSema, PhASAR, and Crab/Clam stay deferred until a fixture proves
|
|
that the active lanes cannot close a specific precision or recall gap.
|
|
|
|
## Current Fold surface
|
|
|
|
| Surface | Current owner | Vendor implication |
|
|
|---|---|---|
|
|
| Source symbolic checks | Clang AST/CFG + Fold Z3 encoder | no new vendor needed now |
|
|
| Binary metadata | r2 session/CLI fallback | LIEF can replace/supplement this later |
|
|
| Binary semantics | Ghidra raw/high P-Code | primary active vendor lane |
|
|
| Cross-function facts | native summaries/graphs | Souffle candidate after stable facts |
|
|
| Numeric invariants | native summaries/ranges | Crab/Clam deferred until a concrete gap |
|
|
|
|
## Why not add all candidate libraries now?
|
|
|
|
- More IRs do not improve findings unless Fold can normalize provenance,
|
|
location, value IDs, and precision.
|
|
- Heavy LLVM-based lanes duplicate Ghidra's current role while adding build and
|
|
version constraints.
|
|
- Fact engines are only safe after stable fact IDs exist; otherwise derived facts
|
|
cannot round-trip into reports or suppressions reliably.
|
|
|
|
## External references
|
|
|
|
- Ghidra P-Code reference: https://ghidra.re/ghidra_docs/languages/html/pcoderef.html
|
|
- Ghidra SLEIGH manual: https://ghidra.re/ghidra_docs/languages/html/sleigh.html
|
|
- LIEF C++ API: https://lief.re/doc/latest/api/cpp/index.html
|
|
- LIEF binary abstraction parser: https://lief.re/doc/stable/api/binary_abstraction/cpp.html
|
|
- Souffle C++ interface: https://souffle-lang.github.io/interface
|
|
- Souffle execution modes: https://souffle-lang.github.io/execute
|
|
|
|
Deferred references are listed in `docs/research/vendor-library-study-2026-05-31.md`.
|
|
|
|
## Next implementation checkpoints
|
|
|
|
1. Keep Ghidra findings provenance-tagged as `ghidra-raw` or `ghidra-ssa`.
|
|
2. Add LIEF only as a read-only metadata adapter; compare it against current r2
|
|
metadata outputs before replacing anything.
|
|
3. Define `FunctionId`, `BlockId`, `OpId`, and `ValueId` before Souffle.
|
|
4. Prototype Souffle with TSV + `.dl` before generated C++ embedding.
|
|
5. Require a fixture-backed revisit trigger before adding RetDec, Remill/McSema,
|
|
PhASAR, or Crab/Clam scaffolding again.
|
|
|
|
## Guardrails
|
|
|
|
- Do not widen `core::AnalysisBackend` for vendor-specific payloads.
|
|
- Do not decompile binaries to C and run source detectors on that output.
|
|
- Keep source, binary metadata, binary semantics, and derived facts separately
|
|
measurable in profiles.
|
|
- Reports must preserve per-finding backend and lane provenance.
|