stella-ops.org/git.stella-ops.org
1
0
Fork 0
Code Issues Pull Requests Actions 2 Releases Wiki Activity
Files
ac544c00643ca073d363fc53f7e3ce2ce4c2f060
git.stella-ops.org/docs/features/checked/attestor/binary-reachability-proofs-binary-diff-analysis.md
master e9aeadc040 save checkpoint
2026-02-14 09:11:48 +02:00

2.7 KiB
Raw Blame History

Binary Reachability Proofs / Binary Diff Analysis

Module

Attestor

Status

VERIFIED

Description

Full binary diff analysis pipeline with schema validation, DSSE-verified predicates, normalization, and fingerprint evidence generation.

Implementation Details

  • BinaryDiff Pipeline: src/Attestor/__Libraries/StellaOps.Attestor.StandardPredicates/BinaryDiff/ -- complete pipeline:
    • IBinaryDiffPredicateBuilder.cs / BinaryDiffPredicateBuilder.cs (with .Build) -- constructs diff predicates
    • IBinaryDiffPredicateSerializer.cs / BinaryDiffPredicateSerializer.cs (with .Normalize) -- deterministic serialization
    • IBinaryDiffDsseVerifier.cs / BinaryDiffDsseVerifier.cs (with .Helpers) -- DSSE verification
    • BinaryDiffDsseSigner.cs -- DSSE signing
    • BinaryDiffSchema.cs (with .SchemaJson) -- JSON schema validation
    • BinaryDiffSectionModels.cs -- section-level models (ELF/PE)
    • BinaryDiffFinding.cs -- individual findings
    • BinaryDiffMetadataBuilder.cs -- metadata construction
  • Fingerprint Evidence: src/Attestor/__Libraries/StellaOps.Attestor.ProofChain/Generators/BinaryFingerprintEvidenceGenerator.cs (with .Helpers) -- generates reachability-aware fingerprint evidence.
  • Reachability Integration: Binary diff evidence feeds into ReachabilityWitnessPayload (statements) and BinaryMicroWitnessPredicate (predicates) for reachability proof chains.
  • Tests: __Tests/StellaOps.Attestor.StandardPredicates.Tests/BinaryDiff/ -- builder, serializer, signer, schema validation tests. __Tests/StellaOps.Attestor.ProofChain.Tests/BinaryMicroWitnessPredicateTests.cs

E2E Test Plan

  • Run the full binary diff pipeline: build predicate from findings, normalize/serialize, sign with DSSE, verify signature, validate against schema
  • Create diff findings for a patched vulnerability (binary changed in .text section) and verify the predicate captures the patch as a security-relevant change
  • Normalize the same diff predicate twice and verify byte-for-byte output equality
  • Validate a well-formed predicate against BinaryDiffSchema and verify it passes
  • Validate a predicate missing required fields and verify schema validation fails with specific error
  • Generate fingerprint evidence from a binary diff result and verify it links to the diff attestation
  • Feed binary diff evidence into a BinaryMicroWitnessPredicate and verify the reachability proof chain includes the diff evidence

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