# Proof-Carrying Reachability Evidence

## Module
Attestor

## Status
VERIFIED

## Description
Reachability evidence as portable, signed attestation bundles containing witness paths (call-path subgraphs from entrypoint to vulnerable node), gate conditions, and assumptions.

## Implementation Details
- **Reachability Witness Payload**: `src/Attestor/__Libraries/StellaOps.Attestor.ProofChain/Statements/ReachabilityWitnessPayload.cs` (with `.Path`) -- witness payload containing the complete call path from entrypoint to vulnerable function.
- **Reachability Witness Statement**: `Statements/ReachabilityWitnessStatement.cs` -- in-toto statement wrapping the witness payload for DSSE signing.
- **Witness Call Path Node**: `Statements/WitnessCallPathNode.cs` -- individual node in the call path with function name, file, line number, and module.
- **Witness Path Node**: `Statements/WitnessPathNode.cs` -- generic path node in the reachability subgraph.
- **Witness Gate Info**: `Statements/WitnessGateInfo.cs` -- gate condition along the path (e.g., input validation, sanitization check, authentication guard).
- **Witness Evidence Metadata**: `Statements/WitnessEvidenceMetadata.cs` -- metadata about the analysis: tool, language, confidence, timestamp, assumptions.
- **Reachability Subgraph Predicate**: `Predicates/ReachabilitySubgraphPredicate.cs` -- minimal subgraph predicate for the reachability evidence.
- **Reachability Subgraph Statement**: `Statements/ReachabilitySubgraphStatement.cs` -- in-toto statement for subgraph attestation.
- **DSSE Signing**: `Signing/ProofChainSigner.cs` (with `.Verification`) -- signs reachability evidence into portable DSSE envelopes.
- **Attestation Bundler**: `__Libraries/StellaOps.Attestor.Bundling/AttestationBundler.cs` -- bundles reachability evidence with related attestations for portability.
- **Tests**: `__Tests/StellaOps.Attestor.ProofChain.Tests/ReachabilityWitnessTests.cs`

## E2E Test Plan
- [ ] Create a `ReachabilityWitnessPayload` with a 5-node call path (entrypoint -> service -> helper -> library -> vulnerable_func) and verify path structure
- [ ] Sign the witness as a `ReachabilityWitnessStatement` via `ProofChainSigner` and verify the DSSE envelope
- [ ] Add `WitnessGateInfo` entries for security checks along the path and verify gates are captured with condition descriptions
- [ ] Verify `WitnessEvidenceMetadata` captures analysis assumptions (e.g., "static analysis only, no runtime data")
- [ ] Bundle reachability evidence with related SBOM and VEX attestations via `AttestationBundler` and verify the bundle is self-contained
- [ ] Verify the signed bundle is portable: export, import to a different environment, and verify all signatures
- [ ] Create evidence for an unreachable path (no path from entrypoint to vulnerable function) and verify the witness payload captures the negative result

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