# 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](security-verdict.md) (Attestation B) references it by digest. This predicate rides the DSSE / in-toto envelope specified in [signing-envelope.md](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](https://www.rfc-editor.org/rfc/rfc2119). ## 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: | Tier | Bar | Who publishes it | Verification primitive | |---|---|---|---| | **T0** | Byte-identical, no exceptions | Reproducible Builds (artifacts) | crypto hash of full artifact | | **T1 (Probity product bar)** | **Masked-byte-identical** — bit-for-bit modulo a declared, closed, minimal nondeterminism mask | **Probity** (live demonstration evidence is tracked in the producer's internal evidence ledger, not in this specification) | hash-and-compare after masking; mask published as a closed set | | **T2** | Output-equivalent — same inputs ⇒ same observable outputs | differential testing (Csmith/EMI) | compare outputs / checksums | | **T3** | Functional-resume — continues correctly, no equality claim | CRIU, QEMU/GCE migration, Firecracker (CRC), forkd probes | liveness/probe/CRC | 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. ```json "subject": [{"name": "probity-frozen-sut", "digest": {"sha256": ""}}] ``` ## Predicate ```json { "byte_identity_proof": { "proof_type": "fold-correctness-v1", "base_merkle_root": "", "diff_merkle_root": "", "folded_merkle_root":"", "exclude_profile": ["virtio_used_ring"], "image_size_bytes": "", "exclude_coverage": { "virtio_used_ring": {"region_count": "", "excluded_bytes": ""} }, "exclude_derivation": { "vmstate_sha256": "" }, "oracle_agreement": true, "used_real_firecracker": true, "reference_oracle": "firecracker-snapshot-editor@v..", "sdk_commit": "" } } ``` 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](signed-evidence.md) 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..`, optionally followed by a `-` 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. ```json { "byte_identity_proof": { "proof_type": "entropy-uniqueness-v1", "image_a_merkle_root": "", "image_b_merkle_root": "", "mask_profile": ["vmgenid_16b", "csprng_entropy"], "vmgenid_gpa": "", "image_size_bytes": "", "mask_coverage": { "vmgenid_16b": {"region_count": 1, "excluded_bytes": 16}, "csprng_entropy": {"region_count": 1, "excluded_bytes": ""} }, "draw_a": {"gpa": "", "length_bytes": "", "sha256": "", "barrier_elapsed_ms": ""}, "draw_b": {"gpa": "", "length_bytes": "", "sha256": "", "barrier_elapsed_ms": ""}, "sdk_commit": "" } } ``` 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. ```json { "vmgenid_reseed_proof": { "proof_type": "vmgenid-reseed-v1", "s0_merkle_root": "", "control_merkle_root": "", "test_merkle_root": "", "test2_merkle_root": "", "gen0": "", "gen_control": "", "gen_test": "", "gen_test2": "", "key0_sha256": "", "key_control_sha256": "", "key_test_sha256": "", "key_test2_sha256": "", "vmgenid_a_sha256": "", "vmgenid_b_sha256": "", "base_crng_gpa": "", "image_size_bytes": "", "sdk_commit": "" } } ``` 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. ```json { "clone_uniqueness_proof": { "proof_type": "clone-uniqueness-v1", "image_a_merkle_root": "", "image_b_merkle_root": "", "source_snapshot_merkle_root": "", "mask_profile": ["vmgenid_16b"], "exclude_profile": ["virtio_used_ring", "kvmclock_wallclock"], "vmgenid_gpa": "", "image_size_bytes": "", "exclude_coverage": { "virtio_used_ring": {"region_count": "", "excluded_bytes": ""}, "kvmclock_wallclock":{"region_count": 1, "excluded_bytes": 12} }, "exclude_derivation": { "vmstate_sha256": "", "snapshot_metadata_sha256": "" }, "sdk_commit": "" } } ``` 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](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", )`. 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](kernel-substrate.md) 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](README.md) 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](signing-envelope.md)** - the DSSE / in-toto envelope, `keyid` derivation, trust root, and offline-verify procedure this predicate uses without deviation. - **[signed-evidence](signed-evidence.md)** - carries this predicate's `folded_merkle_root` as its `merkle_evidence.guest_memory_merkle_root`, plus the value-binding and fold pins. - **[security-verdict](security-verdict.md)** - Attestation B, which references this attestation by digest. A verdict is only as trustworthy as the substrate attestation behind it. - **[kernel-substrate](kernel-substrate.md)** - 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](https://github.com/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](https://github.com/secure-systems-lab/dsse)** - ALIGNED, PAEv1 and ed25519, no deviation. - **[Sigstore / cosign](https://docs.sigstore.dev/)** - NOT USED. There is no Fulcio certificate and no Rekor transparency-log entry; see Verification. - **[SLSA provenance](https://slsa.dev/spec/v1.0/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](README.md), 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.