# Binary Reachability Proofs / Binary Diff Analysis

## Module
Attestor

## Status
IMPLEMENTED

## 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