3.8 KiB
Here’s a crisp way to think about “reachability” that makes triage sane and auditable: treat it like a cryptographic proof—a minimal, reproducible chain that shows why a vuln can (or cannot) hit runtime.
The idea (plain English)
- Reachability asks: “Could data flow from an attacker to the vulnerable code path during real execution?”
- Proof-carrying reachability says: “Don’t just say yes/no—hand me a proof chain I can re-run.” Think: the shortest, lossless breadcrumb trail from entrypoint → sinks, with the exact build + policy context that made it true.
What the “proof” contains
-
Scope hash: content digests for artifact(s) (image layers, SBOM nodes, commit IDs, compiler flags).
-
Policy hash: the decision rules used (e.g., “prod disallows unknowns > 0”; “vendor VEX outranks distro unless backport tag present”).
-
Graph snippet: the minimal subgraph (call/data/control edges) that connects:
- external entrypoint(s) → user-controlled sources → validators (if any) → vulnerable function(s)/sink(s).
-
Conditions: feature flags, env vars, platform guards, version ranges, eBPF-observed edges (if present).
-
Verdict (signed): A → {Affected | Not Affected | Under-Constrained} with reason codes.
-
Replay manifest: the inputs needed to recompute the same verdict (feeds, rules, versions, hashes).
Why this helps
- Auditable: Every “Not Affected” is defensible (no hand-wavy “scanner says so”).
- Deterministic: Same inputs → same verdict (great for change control and regulators).
- Compact: You store only the minimal subgraph, not the whole monolith.
Minimal proof example (sketch)
- Artifact:
svc.payments:1.4.7(image digestsha256:…) - CVE:
CVE-2024-XYZinlibyaml 0.2.5 - Entry:
POST /import, body →YamlDeserializer.Parse - Guards: none (no schema/whitelist prior to parse)
- Edge chain:
HttpBody → Parse(bytes) → LoadNode() → vulnerable_path() - Condition: feature flag
BULK_IMPORT=true - Verdict: Affected
- Signed DSSE envelope over {scope hash, policy hash, graph snippet JSON, conditions, verdict}.
How to build it (practical checklist)
-
During build
- Emit SBOM (source & binary) with function/file symbols where possible.
- Capture compiler/linker flags; normalize paths; include feature flags’ default state.
-
During analysis
- Static: slice the call graph to the shortest source→sink chain; attach type-state facts (e.g., “validated length”).
- Deps: map CVEs to precise symbol/ABI surfaces (not just package names).
- Backports: require explicit evidence (patch IDs, symbol presence) before downgrading severity.
-
During runtime (optional but strong)
- eBPF trace to confirm edges observed; store hashes of kprobes/uprobes programs and sampling window.
-
During decisioning
- Apply merge policy (vendor VEX, distro notes, internal tests) deterministically; hash the policy.
- Emit one DSSE/attestation per verdict; include replay manifest.
UI that won’t overwhelm
- Default card: Verdict + “Why?” (one-line chain) + “Replay” button.
- Expand: shows the 5–10 edge subgraph, conditions, and signed envelope.
- Compare builds: side-by-side proof deltas (edges added/removed, policy change, backport flip).
Operating modes
- Strict (prod): Unknowns → fail-closed; proofs required for Not Affected.
- Lenient (dev): Unknowns tolerated; proofs optional but encouraged; allow “Under-Constrained”.
What to measure
- Proof generation rate, median proof size (KB), replay success %, proof dedup ratio, and “unknowns” burn-down.
If you want, I can turn this into a ready-to-ship spec for Stella Ops (attestation schema, JSON examples, API routes, and a tiny .NET verifier).