Files
git.stella-ops.org/docs/guides/binary-micro-witness-verification.md

5.9 KiB

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

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

Verify a Witness

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

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

Create Portable Bundle

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:

{
  "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:

    stella witness bundle witness.json --output ./bundle
    
  2. Transfer bundle to air-gapped system

  3. Verify offline:

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

{
  "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

{
  "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