# Sprint 20251226 · Function-Level Proof Generation (FuncProof)

## Topic & Scope
- Implement function-level proof objects for binary-level reachability evidence.
- Generate symbol digests, function-range hashes, and entry→sink trace serialization.
- Publish FuncProof as DSSE-signed OCI referrer artifacts linked from SBOM.
- **Working directory:** `src/Scanner/`, `src/BinaryIndex/`, `src/Attestor/`

## Dependencies & Concurrency
- Depends on: `BinaryIdentity` (complete), `NativeReachabilityGraphBuilder` (complete).
- No blocking dependencies; can start immediately.
- Enables: SPRINT_20251226_011_BE (auto-VEX needs funcproof for symbol correlation).

## Documentation Prerequisites
- `docs/modules/scanner/design/native-reachability-plan.md`
- `docs/modules/scanner/os-analyzers-evidence.md`
- `docs/product-advisories/25-Dec-2025 - Evolving Evidence Models for Reachability.md`
- `docs/product-advisories/26-Dec-2026 - Mapping a Binary Intelligence Graph.md`

## Context: What Already Exists

| Component | Location | Status |
|-----------|----------|--------|
| BinaryIdentity (Build-ID, sections) | `BinaryIndex/BinaryIdentity.cs` | COMPLETE |
| ELF/PE/Mach-O parsers | `Scanner.Analyzers.Native/` | COMPLETE |
| Disassemblers (ARM64, x86) | `Scanner.CallGraph/Extraction/Binary/` | COMPLETE |
| DWARF debug reader | `Scanner.CallGraph/Extraction/Binary/DwarfDebugReader.cs` | COMPLETE |
| Call graph snapshot | `Scanner.CallGraph/CallGraphSnapshot.cs` | COMPLETE |
| DSSE envelope support | `Attestor/` | COMPLETE |

This sprint adds **function-level granularity** on top of existing binary infrastructure.

## Delivery Tracker
| # | Task ID | Status | Key dependency / next step | Owners | Task Definition |
| --- | --- | --- | --- | --- | --- |
| 1 | FUNC-01 | TODO | None | Scanner Guild | Define `FuncProof` JSON model: buildId, sections, functions[], traces[] |
| 2 | FUNC-02 | TODO | FUNC-01 | Scanner Guild | Create `FuncProofDocument` PostgreSQL entity with indexes on build_id |
| 3 | FUNC-03 | TODO | FUNC-01 | Scanner Guild | Implement function-range boundary detection using DWARF/symbol table |
| 4 | FUNC-04 | TODO | FUNC-03 | Scanner Guild | Fallback: heuristic prolog/epilog detection for stripped binaries |
| 5 | FUNC-05 | TODO | FUNC-03 | Scanner Guild | Symbol digest computation: BLAKE3(symbol_name + offset_range) |
| 6 | FUNC-06 | TODO | FUNC-05 | Scanner Guild | Populate `symbol_digest` field in `FuncNodeDocument` |
| 7 | FUNC-07 | TODO | FUNC-03 | Scanner Guild | Function-range hashing: rolling BLAKE3 over `.text` subranges per function |
| 8 | FUNC-08 | TODO | FUNC-07 | Scanner Guild | Section hash integration: compute `.text` + `.rodata` digests per binary |
| 9 | FUNC-09 | TODO | FUNC-08 | Scanner Guild | Store section hashes in `BinaryIdentity` model |
| 10 | FUNC-10 | TODO | None | Scanner Guild | Entry→sink trace serialization: compact spans with edge list hash |
| 11 | FUNC-11 | TODO | FUNC-10 | Scanner Guild | Serialize traces as `trace_hashes[]` in FuncProof |
| 12 | FUNC-12 | TODO | FUNC-01 | Attestor Guild | DSSE envelope generation for FuncProof (`application/vnd.stellaops.funcproof+json`) |
| 13 | FUNC-13 | TODO | FUNC-12 | Attestor Guild | Rekor transparency log integration for FuncProof |
| 14 | FUNC-14 | TODO | FUNC-12 | Scanner Guild | OCI referrer publishing: push FuncProof alongside image |
| 15 | FUNC-15 | TODO | FUNC-14 | Scanner Guild | SBOM `evidence` link: add CycloneDX `components.evidence` reference to funcproof |
| 16 | FUNC-16 | TODO | FUNC-15 | Scanner Guild | CLI command: `stella scan --funcproof` to generate proofs |
| 17 | FUNC-17 | TODO | FUNC-12 | Scanner Guild | Auditor replay: `stella verify --funcproof <image>` downloads and verifies hashes |
| 18 | FUNC-18 | TODO | All above | Scanner Guild | Integration tests: full FuncProof pipeline with sample ELF binaries |

## FuncProof Schema (Target)

```json
{
  "buildId": "ab12cd34...",
  "sections": {
    ".text": "blake3:...",
    ".rodata": "blake3:..."
  },
  "functions": [
    {
      "sym": "libfoo::parse_hdr",
      "start": "0x401120",
      "end": "0x4013af",
      "hash": "blake3:..."
    }
  ],
  "traces": [
    "blake3(edge-list-1)",
    "blake3(edge-list-2)"
  ],
  "meta": {
    "compiler": "clang-18",
    "flags": "-O2 -fno-plt"
  }
}
```

## Execution Log
| Date (UTC) | Update | Owner |
| --- | --- | --- |
| 2025-12-26 | Sprint created from advisory analysis; implements FuncProof from "Evolving Evidence Models for Reachability". | Project Mgmt |

## Decisions & Risks
- Decision needed: Hash algorithm (BLAKE3 vs SHA256). Recommend: BLAKE3 for speed.
- Decision needed: Stripped binary handling (heuristics vs fail). Recommend: heuristics with `stripped=true` flag.
- Decision needed: Trace depth limit. Recommend: 10 hops max for compressed paths.
- Risk: Function boundary detection may be imprecise for heavily optimized code. Mitigation: mark confidence per function.
- Risk: Large binaries may produce huge FuncProof files. Mitigation: compress, limit to security-relevant functions.

## Next Checkpoints
- 2025-12-30 | FUNC-06 complete | Symbol digests populated in reachability models |
- 2026-01-03 | FUNC-12 complete | DSSE signing working |
- 2026-01-06 | FUNC-18 complete | Full integration tested |