stella-ops.org/git.stella-ops.org
1
0
Fork 0
Code Issues Pull Requests Actions 2 Releases Wiki Activity
Files
e9aeadc04084353889b1c9dbf4487f5316f4421e
git.stella-ops.org/docs/features/checked/attestor/function-level-reachability-for-vex-decisions.md
master e9aeadc040 save checkpoint
2026-02-14 09:11:48 +02:00

2.6 KiB
Raw Blame History

Function-Level Reachability for VEX Decisions

Module

Attestor

Status

VERIFIED

Description

Multi-language call graph extraction (binary, Java, Python, Node, PHP, Ruby, JavaScript) is implemented with function-level evidence models (MicroWitness predicates, call path nodes, reachability witness payloads).

Implementation Details

  • MicroWitness Predicates: src/Attestor/__Libraries/StellaOps.Attestor.ProofChain/Predicates/ -- function-level evidence:
    • BinaryMicroWitnessPredicate.cs -- complete micro-witness with binary, CVE, and function refs
    • MicroWitnessBinaryRef.cs -- binary reference
    • MicroWitnessCveRef.cs -- CVE reference
    • MicroWitnessFunctionEvidence.cs -- function-level evidence with call-stack position
    • MicroWitnessSbomRef.cs -- SBOM component cross-reference
    • MicroWitnessTooling.cs -- analysis tool metadata
    • MicroWitnessVerdicts.cs -- function-level verdicts
  • Reachability Witness: Statements/ReachabilityWitnessPayload.cs (with .Path) -- call paths. ReachabilityWitnessStatement.cs -- in-toto wrapper.
  • Call Path Nodes: Statements/WitnessCallPathNode.cs, WitnessPathNode.cs -- path nodes with function details.
  • VEX Integration: Generators/VexProofIntegrator.cs (with .Helpers, .Metadata) -- integrates reachability evidence into VEX decisions. VexVerdictProofPayload.cs -- combined VEX + reachability proof.
  • Tests: __Tests/StellaOps.Attestor.ProofChain.Tests/BinaryMicroWitnessPredicateTests.cs

E2E Test Plan

  • Create a BinaryMicroWitnessPredicate with function evidence showing a vulnerable function is reachable and verify the micro-witness is well-formed
  • Create function evidence with MicroWitnessFunctionEvidence at different call-stack depths and verify depth tracking
  • Link micro-witness evidence to a VEX decision via VexProofIntegrator with status "not_affected" (function unreachable) and verify the proof payload
  • Link micro-witness evidence to a VEX decision with status "affected" (function reachable) and verify
  • Create witnesses from multiple language call graphs and verify MicroWitnessTooling captures per-language analysis tools
  • Verify MicroWitnessSbomRef correctly links function evidence to SBOM component entries
  • Create MicroWitnessVerdicts for multiple functions and verify per-function reachability verdicts

Verification

Check Result
Tier 0 - Source Verification PASS
Tier 1 - Build + Code Review PASS
Tier 2 - Behavioral Verification PASS
Verified Date 2026-02-13
Run ID run-001