Probity Substrate-Integrity Attestation, v1

predicateType: https://getprobity.dev/predicate/v1/substrate-integrity

Attestation A: a signed, offline-verifiable statement about the isolation substrate customer scans run on, rather than about any one scan. One is emitted per substrate release, NOT per customer scan, and every security-verdict (Attestation B) references it by digest.

This predicate rides the DSSE / in-toto envelope specified in signing-envelope.md without deviation. Read that document first; everything below concerns the predicate body and the checks a verifier performs after the envelope verifies.

The reference implementation is split across a Go half and a Python half. The Go producer and wire validators are its byte-identity package (the fold, clone, reseed, Merkle and oracle wire validators); the statement builder and the mirrored contract models are its verdict-bundle package (build_substrate_integrity_statement, emit_substrate_integrity, emit_clone_uniqueness, emit_vmgenid_reseed, and the _ByteIdentityProof / _CloneUniquenessProof / _VmgenidReseedProof models). The two validate the same gates so a producer and a consumer cannot diverge.

The key words MUST, MUST NOT, REQUIRED, SHOULD, MAY, and OPTIONAL are to be interpreted as in RFC 2119.

Purpose

Cryptographically proves the substrate that runs customer scans is deterministic and its differential-snapshot fold is byte-identity-verified: the folded guest-memory image (CAS-assembled from base + diff) is byte-identical to an independent same-instant Firecracker capture, modulo a disclosed set of virtio used-ring device-IO regions. This is what makes every security-verdict (Attestation B) trustworthy: B references A by digest. forkd (same-host probes + md5-of-blobs) structurally cannot produce this.

Acceptance bar (T0–T3 taxonomy)

The claim this predicate makes is calibrated against a four-tier byte-identity acceptance-criteria taxonomy, reproduced here so a reader can place the claim without an external reference:

This predicate carries the fold-correctness half of the T1 bar: the fold engine reconstructs, bit-for-bit, the exact memory image Firecracker would dump at the same instant, with the only exclusions being the virtio used-ring pages the Firecracker device-emulation thread legitimately advances during a paused snapshot (Firecracker pauses vCPU threads, not device emulation). The cross-resume entropy-uniqueness half (the two-sided anti-Brooker assertion) is a DISTINCT claim carried by a separate future attestation — see "Severed claim" below. The two are never conflated: a verifier reading this predicate learns the fold is correct, and must NOT infer entropy-uniqueness from it.

Subject

The FROZEN_SUT OCI digest — the pinned substrate the proof was computed against (rootfs OCI image; the SDK commit is recorded in the predicate). This reuses the existing FROZEN_SUT.lock.toml release-gating pin; the substrate-integrity attestation is the cryptographic CONSUMER of that pin.

"subject": [{"name": "probity-frozen-sut", "digest": {"sha256": "<frozen_sut_oci_digest>"}}]

Predicate

{
  "byte_identity_proof": {
    "proof_type":        "fold-correctness-v1",
    "base_merkle_root":  "<sha256>",
    "diff_merkle_root":  "<sha256>",
    "folded_merkle_root":"<sha256>",
    "exclude_profile":   ["virtio_used_ring"],
    "image_size_bytes":  "<uint64>",
    "exclude_coverage": {
      "virtio_used_ring": {"region_count": "<int>", "excluded_bytes": "<page-rounded int>"}
    },
    "exclude_derivation": {
      "vmstate_sha256":  "<sha256>"
    },
    "oracle_agreement":  true,
    "used_real_firecracker": true,
    "reference_oracle":  "firecracker-snapshot-editor@v<MAJOR>.<MINOR>.<PATCH>",
    "sdk_commit":        "<engine-sha>"
  }
}

Every member above is REQUIRED, and the member set is closed: the producer models narrow the body to exactly these keys and refuse to sign one carrying any other. An earlier revision of this document showed this block without image_size_bytes, exclude_coverage, or exclude_derivation. That example was not merely incomplete - a producer that emitted it verbatim would be REJECTED by both the Go wire validator and the Python contract model, because all three are required.

Field semantics

• proof_type — MUST be exactly fold-correctness-v1. The discriminator that severs this proof family from the clone-uniqueness, entropy-uniqueness and vmgenid-reseed families; a verifier MUST reject an artifact whose proof_type it does not recognize.
• base/diff/folded_merkle_root — root of a per-page (4 KiB-leaf) SHA-256 Merkle tree over the respective guest-memory image, 64 lowercase hex chars each. folded == fold(base, diff); verification = recompute the folded root and compare. O(log N) corrupt-page localization on mismatch. The folded_merkle_root is the value the paired signed-evidence predicate carries as its merkle_evidence.guest_memory_merkle_root.
• exclude_profile — the closed set of device-IO region types EXCLUDED from the byte-equality check. Each region's byte offsets are sourced from provenance (the virtqueue used-ring guest-physical addresses Firecracker recorded in the snapshot vmstate; gate = device activated AND queue ready), never from a per-run diff. virtio_used_ring is currently the only legal entry. The profile MAY be empty (a guest with no active virtqueues yields a pure byte-identity fold). Excluded regions carry NO uniqueness assertion: requiring a used ring to differ would bind the proof to a device-IO timing race. (Region-location method is trade-secret; the profile NAMES are public.)
• image_size_bytes — byte size of the compared guest-memory images, so a reader can bound the excluded fraction of the image from the artifact alone. MUST be a non-zero multiple of 4096.
• exclude_coverage — per-region byte counts (region_count, excluded_bytes) quantifying the excluded extent. Its keys MUST be exactly the region types exclude_profile names: a missing entry leaves a named exclusion unquantified, and an extra entry quantifies an exclusion the profile denies. virtio_used_ring's excluded_bytes MUST be page-rounded (used rings are page-rounded by construction). The coverage total MUST NOT exceed image_size_bytes. Names alone would leave the excluded magnitude unbounded, which is what this member exists to prevent.
• exclude_derivation — the exclude profile's provenance. For this family it carries vmstate_sha256 (64 lowercase hex) and NOTHING else: the used-ring addresses are sourced from the snapshot vmstate, and a snapshot_metadata_sha256 key MUST be rejected here. (The clone-uniqueness family's exclude_derivation differs — see that section.)
• oracle_agreement — true iff the producer's fold and Firecracker snapshot-editor edit-memory rebase produced byte-equal merged images on the same (base, diff) inputs. Differential reference oracle (Csmith/EMI-style): proves AGREEMENT, not absolute correctness; reference_oracle pins the FC version. The producer refuses to assemble a proof on disagreement rather than recording oracle_agreement: false, so a conforming artifact never carries the value false.
• used_real_firecracker — MUST be true for an attestable proof: the snapshots were produced by a real Firecracker VMM and the oracle comparison ran against the real snapshot-editor binary. An in-process-model run (simulated snapshots or a reimplemented fold model) is development-only and MUST NOT be signed into Attestation A.
• reference_oracle — the string MUST match firecracker-snapshot-editor@v<MAJOR>.<MINOR>.<PATCH>, optionally followed by a -<pre-release> suffix. The v-prefixed semantic version is normative, not illustrative: the producer enforces exactly this shape. The release tag MUST be the PROBED snapshot-editor --version output of the binary actually executed (not an assumed or configured value) and MUST equal the firecracker_version that produced the snapshots being verified.
• sdk_commit — 7–40 char lowercase-hex git commit of the producing SDK.

The fold-correctness property (what this proof asserts)

The folded image is byte-EQUAL to an INDEPENDENT same-instant Firecracker Full capture on the complement of the excluded regions. The witness is a reference capture taken at the same paused instant as the diff — NOT a second restore (a restore resumes the guest to agent-readiness, drifting hundreds of deterministic pages with no provenance-recoverable addresses; such a witness can never ground an honest equality claim). This is a CAS validation: it proves the differential engine and the fold reconstruct exactly the bytes Firecracker serialized, which is the property every downstream verdict's substrate reference depends on.

Severed claim: cross-resume entropy uniqueness (NOT asserted here)

The two-sided property — equality on the complement of a nondeterminism mask PLUS provable DIFFERENCE of entropy/VMGenID regions across successive resumes (the anti-snapshot-clone-entropy-reuse assertion, Brooker-class, arXiv:2102.12892) — is deliberately NOT part of this predicate. Overloading one proof family with both claims would let a verifier mistake "device-IO pages excluded" for "entropy proven unique".

The SUBSTRATE half of that claim ships as its own proof family, proof_type: "clone-uniqueness-v1" — see the predicate section below: two zero-execution paused restores of the same snapshot are byte-equal on the complement of {the VMGenID region (masked, MUST differ), the kvmclock wall-clock struct and virtio used rings (excluded device-IO, no uniqueness assertion)} while the VMGenID 16 bytes provably DIFFER — the substrate mints fresh clone entropy per restore. The GUEST-consumption half (the guest CSPRNG actually reseeded FROM the restore-minted signal) ships as the proof_type: "vmgenid-reseed-v1" family — the SOUND host-side base_crng differential — see the predicate section below. That family SUPERSEDES the earlier proof_type: "entropy-uniqueness-v1" getrandom witness, which is retained as a documented-unsound predecessor (its userspace draws can diverge with zero VMGenID involvement); live-run evidence for the sound reseed family is tracked in the producer's internal evidence ledger, not in this specification.

entropy-uniqueness-v1 proof family (guest CSPRNG consumption)

Carries the GUEST-consumption half of the severed claim: across two resumed restores of the same snapshot, the guest's CSPRNG reseed actually drew on the restore-minted generation signal, so the witnessed entropy draws DIFFER. Uniqueness-only semantics: this family asserts only that the named regions differ between the two captures. There is NO complement-equality clause (the captures are resumed restores — the guest executed, so no byte-equality claim over the rest of the image is honest) and NO oracle fields (there is no fold to police and no reference merge to agree with). A verifier MUST NOT infer fold correctness or complement equality from this proof, and MUST NOT infer entropy uniqueness from any other family.

{
  "byte_identity_proof": {
    "proof_type":          "entropy-uniqueness-v1",
    "image_a_merkle_root": "<sha256>",
    "image_b_merkle_root": "<sha256>",
    "mask_profile":        ["vmgenid_16b", "csprng_entropy"],
    "vmgenid_gpa":         "<uint64>",
    "image_size_bytes":    "<uint64>",
    "mask_coverage": {
      "vmgenid_16b":    {"region_count": 1, "excluded_bytes": 16},
      "csprng_entropy": {"region_count": 1, "excluded_bytes": "<draw length>"}
    },
    "draw_a": {"gpa": "<uint64>", "length_bytes": "<uint64>", "sha256": "<sha256>", "barrier_elapsed_ms": "<int64>"},
    "draw_b": {"gpa": "<uint64>", "length_bytes": "<uint64>", "sha256": "<sha256>", "barrier_elapsed_ms": "<int64>"},
    "sdk_commit":          "<engine-sha>"
  }
}

Field semantics and verifier gates (the producer validates the identical shape before any bytes hit disk):

• proof_type — MUST be exactly entropy-uniqueness-v1. A verifier MUST reject any artifact whose proof_type it does not recognize.
• image_a_merkle_root / image_b_merkle_root — per-page (4 KiB-leaf) SHA-256 Merkle roots of the two resumed-restore captures, 64 lowercase hex chars each. These are capture commitments with NO equality semantics. The two roots MUST differ: a passing uniqueness verdict requires the asserted-unique regions to differ, which forces a leaf — hence the root — to differ; equal roots are internally inconsistent with the claim and MUST be rejected.
• mask_profile — the closed per-family asserted-unique region vocabulary. For v1 it MUST be exactly the ordered pair ["vmgenid_16b", "csprng_entropy"]; any other length, entry, or order MUST be rejected. The closed per-family vocabulary keeps a verifier from ever inferring one family's claim from another's artifact.
• vmgenid_gpa — the guest-physical address of the 16-byte generation-id region (the same architecture constant in both images). MUST be non-zero and MUST place a 16-byte region inside the image (vmgenid_gpa + 16 <= image_size_bytes). A verifier additionally asserts the value equals its OWN architecture constant, so the proof demonstrably checked the SAME region the verifier's constant names.
• image_size_bytes — byte size of the compared capture images. MUST be a non-zero multiple of 4096.
• mask_coverage — per-region byte counts (region_count, excluded_bytes) quantifying the asserted-unique extent from the artifact alone. MUST contain exactly the two vocabulary entries: vmgenid_16b MUST be exactly one 16-byte span (region_count 1, excluded_bytes 16), and csprng_entropy MUST be exactly one span whose excluded_bytes equals the carried draw length.
• draw_a / draw_b — each capture's witness-draw provenance: gpa and length_bytes MUST be non-zero and place the region inside the image (overflow-checked); sha256 is the digest the captured bytes were checked against, 64 lowercase hex chars; barrier_elapsed_ms is how long the reseed barrier waited (the jitter bound for the causal-attribution argument) and MUST be non-negative. The two draws MUST have equal length_bytes (uniqueness is defined over equal-length byte strings) and their sha256 values MUST differ — identical draw digests are the snapshot-clone entropy-reuse failure this family exists to catch and MUST be rejected.
• sdk_commit — 7–40 char lowercase-hex git commit of the producing SDK.

vmgenid-reseed-v1 proof family (guest CSPRNG reseeded FROM the restore-minted VMGenID — the SOUND base_crng differential)

Carries the SOUND form of the guest-consumption claim and SUPERSEDES the entropy-uniqueness-v1 getrandom witness (which is unsound: a stale base_crng.birth timed reseed plus the per-extract RDSEED/RDRAND/RDTSC mix diverge the witnessed draws with ZERO VMGenID involvement, a false PASS — verified against linux-6.1.137 drivers/char/random.c). Instead of witnessing userspace draws, this family reads the kernel ROOT CSPRNG state (base_crng.{generation, key}) host-side via the VMI chain from FOUR paused captures of one snapshot S0, and proves the guest kernel CSPRNG reseeded FROM the restore-minted VMGenID. Differential semantics with a DEDUCTIVE attribution: the soundness rests not on a single negative control but on a kernel-lemma caller enumeration (below); the family asserts the four-leg base_crng relation and the genid change, and carries NO oracle fields and NO complement-equality clause. A verifier MUST NOT infer fold correctness, complement equality, or entropy uniqueness from this proof, and MUST NOT infer this claim from any other family.

The four captures: S0 — the pre-snapshot state after a forced RNDRESEEDCRNG (a fresh base_crng.birth + crng_init == CRNG_READY), carrying (gen0, key0) and VMGenID region value vmgen_a. CONTROL — S0 restored PAUSED and NEVER resumed (zero guest execution); its base_crng MUST still read (gen0, key0). This is the apparatus-fidelity baseline (the restore + VMI-read left base_crng untouched at zero execution); it is NOT a genid-held resume (Firecracker always re-mints the VMGenID on restore, and holding it would require an untrusted host write into guest RAM). TEST — S0 restored + briefly resumed; the restore-minted fresh VMGenID drives vmgenid_notify → add_vmfork_randomness → crng_reseed, so base_crng reads (gen0+1, key_test ≠ key0); its VMGenID region is vmgen_b. TEST2 — a SECOND independent restore + brief resume; the second restore mints a DISTINCT fresh VMGenID, so its reseed produces a DISTINCT key (gen0+1, key_test2 ≠ key_test ∧ ≠ key0) — the anti-snapshot-clone-entropy-reuse corroboration (Brooker-class, arXiv:2102.12892): a deterministic non-genid reseed would produce the SAME key on both restores.

Why it is sound (the load-bearing DEDUCTIVE attribution): base_crng.{generation, key} change ONLY in crng_reseed (random.c). Its callers in the sub-second measurement window are exhaustively: the TIMED/cold-start reseed — DEAD, because the pre-snapshot RNDRESEEDCRNG sets a fresh base_crng.birth (random.c:227) and the window « CRNG_RESEED_INTERVAL = 60·HZ = 60s (random.c:178-181); add_vmfork_randomness (random.c:947-955) — the vmfork, the only live reseed source on a brief resume; the RNDRESEEDCRNG ioctl — not invoked in the window. add_interrupt_randomness (random.c:1068-1092) only mixes the per-CPU fast_pool and NEVER calls crng_reseed. Therefore on a brief resume the SOLE reseed source is the vmfork, so the TEST/TEST2 reseeds are vmfork-caused; and the kernel lemma — add_vmfork_randomness calls add_device_randomness mixing the VMGenID into the input pool BEFORE crng_reseed extracts the new key (random.c:953-955) — proves each new key INCORPORATES that restore's distinct VMGenID. The zero-execution CONTROL is the apparatus baseline; this caller enumeration is the causation; TEST2 corroborates the per-restore genid dependence.

{
  "vmgenid_reseed_proof": {
    "proof_type":          "vmgenid-reseed-v1",
    "s0_merkle_root":      "<sha256>",
    "control_merkle_root": "<sha256>",
    "test_merkle_root":    "<sha256>",
    "test2_merkle_root":   "<sha256>",
    "gen0":                "<uint64>",
    "gen_control":         "<uint64>",
    "gen_test":            "<uint64>",
    "gen_test2":           "<uint64>",
    "key0_sha256":         "<sha256>",
    "key_control_sha256":  "<sha256>",
    "key_test_sha256":     "<sha256>",
    "key_test2_sha256":    "<sha256>",
    "vmgenid_a_sha256":    "<sha256>",
    "vmgenid_b_sha256":    "<sha256>",
    "base_crng_gpa":       "<uint64>",
    "image_size_bytes":    "<uint64>",
    "sdk_commit":          "<engine-sha>"
  }
}

Field semantics and verifier gates (the producer validates the identical shape before any bytes hit disk — pkg/byteident/reseedwire.go):

• proof_type — MUST be exactly vmgenid-reseed-v1. The discriminator that severs this family from the fold-correctness, clone-uniqueness, and entropy-uniqueness families; a verifier MUST reject any artifact whose proof_type it does not recognize.
• s0_merkle_root / control_merkle_root / test_merkle_root / test2_merkle_root — per-page (4 KiB-leaf) SHA-256 Merkle roots of the four paused captures, 64 lowercase hex chars each. These are capture commitments with NO equality semantics. The two RESEEDED roots MUST each differ from S0 and from each other (s0 ≠ test, s0 ≠ test2, test ≠ test2): a reseed forces a base_crng leaf — hence the root — to differ, and distinct per-restore keys force the two test roots to differ; equal roots there are internally inconsistent with the claim and MUST be rejected. The CONTROL root is NOT constrained equal to S0: a zero-execution restore re-mints the VMGenID region and KVM re-stamps the kvmclock wall-clock struct, so the whole-image root MAY legitimately differ even though base_crng reads identical.
• gen0 / gen_control / gen_test / gen_test2 — the base_crng.generation counters read from the four captures (verbatim little-endian unsigned long). gen_control MUST equal gen0 (the zero-execution baseline did not reseed); gen_test and gen_test2 MUST each equal gen0 + 1 (each resumed restore reseeded by exactly one generation — a jump of 2 would mean a second, non-vmfork reseed also fired and MUST be rejected). gen0 MUST NOT be at the generation-counter wrap boundary (gen0 + 1 would be the ULONG_MAX sentinel crng_reseed avoids, random.c:223-225).
• key0_sha256 / key_control_sha256 / key_test_sha256 / key_test2_sha256 — SHA-256 of each capture's base_crng.key (32 bytes), 64 lowercase hex chars. The raw key is NEVER carried — only its digest — so a signed proof leaks no live CSPRNG key material. key_control_sha256 MUST equal key0_sha256 (the zero-execution baseline did not change the key); key_test_sha256 MUST differ from key0_sha256 (the TEST reseed produced new key material); key_test2_sha256 MUST differ from BOTH key0_sha256 (it reseeded) AND key_test_sha256 (the two restores' distinct VMGenIDs drove distinct keys — the anti-Brooker corroboration; equal test/test2 keys are the deterministic-reseed failure this leg exists to catch and MUST be rejected).
• vmgenid_a_sha256 / vmgenid_b_sha256 — SHA-256 of the 16-byte VMGenID region read from S0 (vmgen_a) and the TEST capture (vmgen_b). They MUST differ — a fresh VMGenID was actually injected for the TEST leg; equal digests mean no fresh id was minted and MUST be rejected.
• base_crng_gpa — the direct-map-resolved guest-physical address base_crng was read at (the same static kernel symbol in all four captures). MUST be non-zero and MUST place the conservative 56-byte base_crng struct footprint inside the image (base_crng_gpa + 56 <= image_size_bytes); the proof reads only the key (32 B @0) and generation (8 B @40), both inside it.
• image_size_bytes — byte size of the compared capture images. MUST be a non-zero multiple of 4096.
• sdk_commit — 7–40 char lowercase-hex git commit of the producing SDK.

clone-uniqueness-v1 proof family (substrate per-restore VMGenID uniqueness)

Carries the SUBSTRATE half of the severed claim: two ZERO-execution paused restores of the same source snapshot are byte-equal on the complement of the disclosed device-IO exclude regions, while the 16-byte VMGenID region provably DIFFERS between them — the substrate mints fresh clone entropy per restore (the anti-snapshot-clone-entropy-reuse property, Brooker-class, arXiv:2102.12892, on the substrate side). Uniqueness-only semantics: this family asserts only that the named mask region differs between the two captures. There is NO complement-equality clause carried in the proof (the proof binds to its substrate via source_snapshot_merkle_root; the complement-byte-equal half is enforced by the producer before a proof is assembled, never re-asserted as a signed field) and NO oracle fields anywhere (there is no fold to police and no reference merge to agree with — unlike fold-correctness, this claim is about the substrate minting entropy, not about a differential fold). A verifier MUST NOT infer fold correctness or complement equality from this proof, and MUST NOT infer clone-uniqueness from any other family.

{
  "clone_uniqueness_proof": {
    "proof_type":                   "clone-uniqueness-v1",
    "image_a_merkle_root":          "<sha256>",
    "image_b_merkle_root":          "<sha256>",
    "source_snapshot_merkle_root":  "<sha256>",
    "mask_profile":                 ["vmgenid_16b"],
    "exclude_profile":              ["virtio_used_ring", "kvmclock_wallclock"],
    "vmgenid_gpa":                  "<uint64>",
    "image_size_bytes":             "<uint64>",
    "exclude_coverage": {
      "virtio_used_ring":  {"region_count": "<int>", "excluded_bytes": "<page-rounded int>"},
      "kvmclock_wallclock":{"region_count": 1, "excluded_bytes": 12}
    },
    "exclude_derivation": {
      "vmstate_sha256":            "<sha256>",
      "snapshot_metadata_sha256":  "<sha256>"
    },
    "sdk_commit":                   "<engine-sha>"
  }
}

Field semantics and verifier gates (the producer validates the identical shape before any bytes hit disk — pkg/byteident/clonewire.go):

• proof_type — MUST be exactly clone-uniqueness-v1. The discriminator that severs this family from the fold-correctness and entropy-uniqueness families; a verifier MUST reject any artifact whose proof_type it does not recognize.
• image_a_merkle_root / image_b_merkle_root — per-page (4 KiB-leaf) SHA-256 Merkle roots of the two zero-execution paused-restore captures, 64 lowercase hex chars each. These are capture commitments; the two roots MUST differ: a passing uniqueness verdict requires the VMGenID region to differ, which forces a leaf — hence the root — to differ, so equal roots are internally inconsistent with the claim and MUST be rejected.
• source_snapshot_merkle_root — the per-page SHA-256 Merkle root of the snapshot both captures were restored from, 64 lowercase hex chars. It binds the clone-uniqueness claim to a specific substrate state, so a verifier can confirm the captures derive from a known snapshot rather than from two unrelated images. There is no equality semantics among the three roots beyond the image_a≠image_b gate above.
• mask_profile — the closed per-family asserted-unique region vocabulary. For v1 it MUST be exactly ["vmgenid_16b"]; any other length, entry, or order MUST be rejected. The pvclock page is quiescent across paused restores and so is NOT asserted unique. The closed per-family vocabulary keeps a verifier from ever inferring one family's claim from another's artifact.
• exclude_profile — the disclosed device-IO regions EXCLUDED from the byte-equality check, drawn from the CLOSED clone-uniqueness exclude vocabulary {virtio_used_ring, kvmclock_wallclock}. The profile MAY be empty (a guest with no active virtqueues and no wall-clock record). virtio_used_ring covers the used rings the device-emulation thread may advance under a paused vCPU; kvmclock_wallclock covers the struct pvclock_wall_clock, which KVM re-stamps on every paused restore — this region is legal HERE but NOT in the fold-correctness proof (whose same-instant captures see an identical wall-clock page). Excluded regions carry NO uniqueness assertion.
• vmgenid_gpa — the guest-physical address of the 16-byte generation-id region (the same architecture constant in both images). MUST be non-zero and MUST place a 16-byte region inside the image (vmgenid_gpa + 16 <= image_size_bytes). A verifier additionally asserts the value equals its OWN architecture constant, so the proof demonstrably checked the SAME region the verifier's constant names (closing the cross-language constant-desync hole).
• image_size_bytes — byte size of the compared capture images. MUST be a non-zero multiple of 4096.
• exclude_coverage — per-region byte counts (region_count, excluded_bytes) quantifying the excluded extent from the artifact alone. Its keys MUST be exactly the region types exclude_profile names (a missing entry leaves a named exclusion unquantified; an extra entry quantifies an exclusion the profile denies). When present, virtio_used_ring's excluded_bytes MUST be page-rounded (used rings are page-rounded by construction), and kvmclock_wallclock MUST be exactly one 12-byte span (region_count 1, excluded_bytes 12 — there is exactly one struct pvclock_wall_clock per guest). The coverage total MUST NOT exceed image_size_bytes.
• exclude_derivation — the exclude profile's provenance: vmstate_sha256 (64 lowercase hex) is ALWAYS present (the virtio used-ring addresses are sourced from the snapshot vmstate). snapshot_metadata_sha256 (the wall-clock region's provenance) is present if and only if the profile excludes kvmclock_wallclock: a wall-clock exclusion with no snapshot-metadata digest is unprovenanced, and a snapshot-metadata digest with no wall-clock region claims provenance nothing uses — both MUST be rejected. (This differs from the fold family's exclude_derivation, which carries the vmstate digest alone and rejects snapshot_metadata_sha256 outright.)
• sdk_commit — 7–40 char lowercase-hex git commit of the producing SDK.

Cross-host scope (normative caveats)

The cross-host T1 claim covers: capture on host A, base+diff memory crossing ONLY via the content-addressed store, fold + this fold-correctness proof emitted on host B (real pinned oracle). SCOPE CAVEATS a verifier MUST respect: (i) guest restore requires a CPU-compatible host pair — a cross-vendor restore is refused at vCPU register restore (the fold and the proof still hold cross-vendor; only restore degrades, T1 fold-proof with T3-unavailable resume); (ii) the witness reference capture and the FC-native diff MUST travel as explicitly-labelled evidence over extent-preserving transport (the diff's sparse-extent map is semantic input to the reference oracle). The dated live-demonstration narrative (hosts, runs, vendor pairs, evidence SHAs) lives in the producer's internal evidence ledger, not in this specification: a verifier binds to the artifact in hand, never to a run narrative it cannot check.

Verification (third-party, offline)

The envelope-level procedure is signing-envelope.md §Verification procedure and is not restated here. In summary: confirm payloadType == application/vnd.in-toto+json, decode payload from base64 and keep the bytes verbatim (never re-serialize), resolve each signature's REQUIRED keyid against the configured trust anchor, and verify the raw ed25519 signature over PAE("application/vnd.in-toto+json", <payload bytes>). The Statement is canonicalized under RFC 8785 (JSON Canonicalization Scheme).

Two properties of the trust model are load-bearing here and a verifier MUST enforce both.

• A signing key is authorized per predicate type. A published verification key carries the set of predicate types it may sign. A verifier MUST reject a statement whose predicateType is not in the resolving key's authorized set, so a key issued for trace records cannot mint a substrate attestation even though both verify under ed25519. https://getprobity.dev/predicate/v1/substrate-integrity is in the authorized set of the producer's evidence-signing key.
• There is no transparency log, and its absence is deliberate. Signing does not upload to a public log, so there is no third-party inclusion proof, no independent timestamp, and no public record of the substrate digests an attestation binds. That is the point: the attestation stays exactly as private as the substrate it describes. A verifier MUST NOT treat the absence of a log entry as a defect, and MUST NOT be built to require one. An earlier revision of this document instructed a verifier to "check signature + Rekor inclusion"; no such entry has ever existed for this predicate, and a verifier that required one would reject every conforming artifact.

cosign verify-blob is NOT the verification path for this predicate. That command checks a detached signature over a blob, which is the kernel-substrate v1 wire form, not a DSSE envelope. A substrate-integrity attestation is verified by any DSSE-aware implementation over the PAE of its payload — the reference verifiers are the packages/verify TypeScript library and website/public/verify/probity-verify.py.

Once the envelope verifies, dispatch on proof_type FIRST; each proof_type's field gates in its own predicate section are normative for verification. The path below differs by family, and a verifier MUST NOT carry one family's gates onto another's artifact.

• fold-correctness-v1 — check proof_type is exactly fold-correctness-v1 → apply the "Field semantics" gates above (the closed member set, the closed exclude_profile vocabulary, exclude_coverage keys matching the profile exactly with a page-rounded used-ring total not exceeding image_size_bytes, exclude_derivation carrying vmstate_sha256 and no snapshot_metadata_sha256, and the reference_oracle shape) → optionally recompute the folded Merkle root against the pinned FROZEN_SUT substrate and compare to folded_merkle_root. No live VM, no hypervisor access, and no network access required. A verifier MUST reject any proof whose used_real_firecracker is not true, and MUST NOT treat a fold-correctness proof as evidence of entropy uniqueness.
• clone-uniqueness-v1 — after the signature check, verify against the "clone-uniqueness-v1 proof family" section's gates: the closed mask_profile (["vmgenid_16b"]) and exclude_profile (⊆ {virtio_used_ring, kvmclock_wallclock}) vocabularies, and the VMGenID-differs gate (image_a_merkle_root ≠ image_b_merkle_root, vmgenid_gpa placing a 16-byte region in the image and equal to the verifier's own architecture constant). No fold/oracle fields are present or expected.
• vmgenid-reseed-v1 — after the signature check, verify against the "vmgenid-reseed-v1 proof family" section's gates: the four-leg base_crng gen/key relation (gen_control == gen0 ∧ key_control == key0; gen_test == gen_test2 == gen0+1; key_test, key_test2 pairwise-distinct from each other and from key0) together with vmgenid_a_sha256 ≠ vmgenid_b_sha256. No mask_profile/exclude_profile and no oracle fields are present or expected.

The retired entropy-uniqueness-v1 getrandom witness is NOT a verification target — it is documented (above) only as an unsound predecessor of vmgenid-reseed-v1. A verifier MUST reject an entropy-uniqueness-v1 artifact rather than verify it.

What a verifier can and cannot independently check (honesty)

• A verifier CAN confirm the statement is authentic under a key it configured and authorized for this predicate type, that it binds exactly the FROZEN_SUT digest it intended, that the proof family is one it recognizes, and that every field gate for that family holds. All of that is offline from the statement and the public key alone.
• A verifier CAN recompute a Merkle root and compare it to a carried one only when it supplies the memory image — a real check, but relative to an anchor the auditor brings, never derivable from the statement alone.
• A verifier CANNOT, from the statement alone, confirm that the captures came from a real Firecracker run rather than being asserted, that the oracle comparison was actually performed, or that the excluded regions were located by the provenance the exclude_derivation digest names. oracle_agreement and used_real_firecracker are producer self-assertions carried under signature; the producer refuses to assemble a proof when either is false, so a conforming artifact never carries a negative — which means their presence records the producer's gate, not an independent check.

Status and maturity

• Format, producers, and wire validators: implemented. The Go wire validators (the byte-identity package) and the Python contract models (the verdict-bundle package) enforce the same per-family gates, and the chain harness in scripts/e2e_step0.py emits and offline-verifies substrate-integrity and clone-uniqueness bundles in one run.
• Verifier recognition: implemented. The predicate type is in the recognized set of both the packages/verify TypeScript library and website/public/verify/probity-verify.py, and in the authorized-predicate set of the published evidence-signing key.
• entropy-uniqueness-v1: retired. It is documented as an unsound predecessor and is a rejection target, not a verification target.
• Standardization status: wave 2. The standard README lists the uniqueness families as a wave-2 group. This document is normative for the type URI and is published so the URI resolves; wave-2 membership concerns the standardization track, not whether the format is stable.

Related standards

• signing-envelope.md - the DSSE / in-toto envelope, keyid derivation, trust root, and offline-verify procedure this predicate uses without deviation.
• signed-evidence - carries this predicate's folded_merkle_root as its merkle_evidence.guest_memory_merkle_root, plus the value-binding and fold pins.
• security-verdict - Attestation B, which references this attestation by digest. A verdict is only as trustworthy as the substrate attestation behind it.
• kernel-substrate - a different substrate statement with a different wire form. That one is a detached-signature bundle verified by byte-equality against a reconstructed pre-image; this one is a DSSE / in-toto Statement. Do not carry one's verification path onto the other.
• in-toto attestation - ALIGNED. The payload is an in-toto Statement v1; subject binding and predicateType routing are used as in-toto defines them.
• DSSE - ALIGNED, PAEv1 and ed25519, no deviation.
• Sigstore / cosign - NOT USED. There is no Fulcio certificate and no Rekor transparency-log entry; see Verification.
• SLSA provenance - RELATED, not overlapping. Provenance describes how an artifact was built; this predicate proves a property of the substrate it runs on.

Versioning

This is the substrate-integrity v1 predicate. Each proof family's member set is closed at the producer: a producer MUST NOT emit a member not defined in that family's section, and the producer models refuse to sign a body carrying one. Per the standard's forward-compatibility rule, a verifier MUST ignore a member it does not recognize rather than rejecting the statement; the vocabulary rule below is the deliberate exception, because an unknown enum VALUE for a known field is one a verifier cannot interpret and so cannot trust.

The exclude_profile vocabulary is a CLOSED registry: virtio_used_ring is the only legal v1 entry, and a verifier MUST reject any entry it does not recognize (fail-closed; no warn-mode verifier exists or is planned). Adding a name to the registry is a spec revision that ships a new published registry list — never a silent additive change a deployed verifier is expected to tolerate. The mask_profile vocabularies are likewise CLOSED per family: clone-uniqueness-v1 admits exactly vmgenid_16b, and entropy-uniqueness-v1 admits exactly the ordered pair vmgenid_16b, csprng_entropy; a verifier MUST reject any artifact carrying a different profile (same spec-revision rule applies to additions). The clone-uniqueness-v1 exclude_profile is a CLOSED vocabulary {virtio_used_ring, kvmclock_wallclock} (possibly empty); a verifier MUST reject any entry it does not recognize. Any change to the Merkle construction or the fold-correctness semantics → v2. Each uniqueness claim arrives as its own proof_type (and predicate section) — clone-uniqueness-v1, entropy-uniqueness-v1, and vmgenid-reseed-v1 did — never as a mutation of this one. The vmgenid-reseed-v1 family carries no mask_profile/exclude_profile vocabulary; its closed shape is the fixed four-leg base_crng relation (gen_control == gen0 ∧ key_control == key0; gen_test == gen_test2 == gen0+1; key_test, key_test2 pairwise-distinct from each other and from key0; vmgenid_a ≠ vmgenid_b), and any change to that relation or to the base_crng read geometry → a new proof_type, never a silent additive change a deployed verifier is expected to tolerate.