# Verifying Binary Patches with Stella Micro-Witnesses

This guide explains how to use binary micro-witnesses to verify that shipped binaries contain specific security patches.

## Overview

Binary micro-witnesses provide cryptographic proof of patch status at the binary level. Unlike source-level attestations, they verify what's actually deployed, not what should be deployed.

### Use Cases

- **Procurement**: Verify vendor claims that CVEs are fixed in delivered binaries
- **Audit**: Provide evidence of patch status for compliance
- **Incident Response**: Quickly determine exposure across binary inventory
- **Supply Chain**: Validate that build outputs match expected patch state

## Quick Start

### Generate a Witness

```bash
stella witness generate /path/to/libssl.so.3 \
  --cve CVE-2024-0567 \
  --sbom sbom.cdx.json \
  --sign \
  --rekor \
  --output witness.json
```

### Verify a Witness

```bash
# Online verification (checks Rekor)
stella witness verify witness.json

# Offline verification (air-gapped)
stella witness verify witness.json --offline
```

### Create Portable Bundle

```bash
stella witness bundle witness.json --output ./audit-bundle
```

## Understanding Verdicts

| Verdict | Meaning |
|---------|---------|
| `patched` | Binary matches patched version signature |
| `vulnerable` | Binary matches vulnerable version signature |
| `inconclusive` | Unable to determine (insufficient evidence) |
| `partial` | Some functions patched, others not |

### Confidence Scores

Confidence ranges from 0.0 to 1.0:

- **0.95+**: High confidence - multiple functions matched with strong evidence
- **0.80-0.95**: Medium confidence - some functions matched
- **<0.80**: Low confidence - limited evidence or compiler variation

## Evidence Types

Micro-witnesses include function-level evidence:

```json
{
  "evidence": [
    {
      "function": "SSL_CTX_new",
      "state": "patched",
      "score": 0.97,
      "method": "semantic_ksg"
    }
  ]
}
```

### Match Methods

| Method | Description | Robustness |
|--------|-------------|------------|
| `byte_exact` | Exact byte-level match | Fragile to recompilation |
| `cfg_structural` | Control flow graph structure | Moderate |
| `semantic_ksg` | Semantic Key-Semantics Graph | Robust to optimization |
| `ir_semantic` | IR-level semantic comparison | Most robust |

## Offline Verification

For air-gapped environments:

1. **Create bundle** with Rekor proof included:
   ```bash
   stella witness bundle witness.json --output ./bundle
   ```

2. **Transfer bundle** to air-gapped system

3. **Verify offline**:
   ```bash
   # PowerShell
   .\verify.ps1

   # Bash
   ./verify.sh
   ```

The bundle includes:
- Witness predicate (JSON)
- Verification scripts (cross-platform)
- SBOM reference (if included)
- Rekor tile proof (when available)

## Integration with SBOMs

Micro-witnesses can reference SBOM components:

```json
{
  "sbomRef": {
    "sbomDigest": "sha256:...",
    "purl": "pkg:deb/debian/openssl@3.0.11",
    "bomRef": "openssl-3.0.11"
  }
}
```

This links binary verification to your software inventory.

## Predicate Schema

Full schema: `https://stellaops.dev/predicates/binary-micro-witness@v1`

```json
{
  "schemaVersion": "1.0.0",
  "binary": {
    "digest": "sha256:...",
    "purl": "pkg:...",
    "arch": "linux-amd64",
    "filename": "libssl.so.3"
  },
  "cve": {
    "id": "CVE-2024-0567",
    "advisory": "https://...",
    "patchCommit": "abc123"
  },
  "verdict": "patched",
  "confidence": 0.95,
  "evidence": [...],
  "deltaSigDigest": "sha256:...",
  "sbomRef": {...},
  "tooling": {
    "binaryIndexVersion": "2.1.0",
    "lifter": "b2r2",
    "matchAlgorithm": "semantic_ksg"
  },
  "computedAt": "2026-01-28T12:00:00Z"
}
```

## Limitations

### What Micro-Witnesses Prove
- A specific binary was analyzed
- Function signatures were compared against known patterns
- A verdict was computed with a confidence score

### What They Do NOT Prove
- Binary authenticity (use SBOM attestations)
- Absence of other vulnerabilities (only specific CVE)
- Build provenance (use SLSA attestations)

### Technical Limitations
- Heavy inlining may hide patched functions
- Stripped symbols reduce match accuracy
- Obfuscated binaries yield "inconclusive"
- Very old binaries may not have ground-truth signatures

## Transparency Logging

When `--rekor` is specified, witnesses are logged to the Rekor transparency log:

- Provides tamper-evidence
- Enables auditors to verify witness wasn't backdated
- Supports v2 tile-based inclusion proofs

Offline bundles include tile proofs for air-gapped verification.

## CLI Reference

### `stella witness generate`

```
stella witness generate <binary> --cve <id> [options]

Arguments:
  binary              Path to binary file to analyze

Options:
  -c, --cve <id>      CVE identifier (required)
  -s, --sbom <path>   Path to SBOM file
  -o, --output <path> Output file (default: stdout)
  --sign              Sign the witness
  --rekor             Log to Rekor transparency log
  -f, --format        Output format: json, envelope (default: json)
  -v, --verbose       Enable verbose output
```

### `stella witness verify`

```
stella witness verify <witness> [options]

Arguments:
  witness             Path to witness file

Options:
  --offline           Verify without network access
  -s, --sbom <path>   Validate SBOM reference
  -f, --format        Output format: text, json (default: text)
  -v, --verbose       Enable verbose output
```

### `stella witness bundle`

```
stella witness bundle <witness> --output <dir> [options]

Arguments:
  witness             Path to witness file

Options:
  -o, --output <dir>  Output directory (required)
  --include-binary    Include analyzed binary
  --include-sbom      Include SBOM file
  -v, --verbose       Enable verbose output
```

## Related Documentation

- [BinaryIndex Architecture](../modules/binaryindex/architecture.md)
- [Attestor Module](../modules/attestor/architecture.md)
- [Delta-Sig Predicate Schema](../schemas/predicates/deltasig-v2.schema.json)