sandbox: make the tier true, make it checkable, and let S7 locality be falsified #57

Merged

dcharlot merged 3 commits from sandbox/honest-tier into main 2026-08-29 03:09:32 -04:00

Conversation 0 Commits 3 Files changed 15 +1176 -21

dcharlot commented 2026-08-24 23:34:10 -04:00

Owner

Copy link

sandbox-build sealed every command step as Tier::S5, but the step is run by ProcessVmm::new — a bare Command::spawn. No VMM, no guest kernel, no dedicated vCPU, and no /dev/kvm check anywhere on the path. The honest rung is S0 ("process only; trusted code"), the floor. Build receipts were claiming hardware isolation for work that ran as an ordinary child process on the host.

SPEC already forbids this — "A host MUST NOT seal a tier a run did not execute at" — so this is a conformance fix, not a change of meaning.

Why structural rather than a /dev/kvm check at the call site

The bug shape is the caller asserts a tier. A check bolted onto the one site leaves the next caller free to repeat it. Now the executor reports the tier instead:

• Vmm::attained_tier() defaults to Tier::S0. The floor is the default deliberately: an implementor who forgets to override under-claims, which is survivable, rather than over-claiming, which makes a receipt a lie.
• ProcessVmm is genuinely dual-use — supervising firecracker really is S5, supervising cargo build is not — and that cannot be inferred from a program name. So it is declared: new is S0, supervising_vmm may claim S5, and even then only where the host exposes hardware virtualization.
• MicroVmExecutor::tier() delegates to its VMM instead of returning a static S5, so Host::run_and_seal's executor-vs-required cross-check can no longer be satisfied by a run that never touched a hypervisor.
• sandbox-proof::prove_microvm supervises the real firecracker binary behind an existing /dev/kvm guard, so it declares supervising_vmm and correctly keeps S5. That path is unchanged in behaviour.

Verification

• 188 workspace tests pass; conformance passes with no skips, C5 tier.json included.
• Exactly one existing test changed — the one that encoded the bug in its name (a_command_step_runs_in_the_microvm_and_seals_at_s5). It failed with left: S0, right: S5, which is the fix working.
• Two new contract tests pin the invariants: a supervised process never claims a virtualization tier, and the trait default is the floor.

Blast radius

Contained to sandbox-rs; no other workspace path-depends on these crates. Build receipts from this path now read S0 instead of S5 — that is the point, and it is a downgrade of a claim, never of enforcement: nothing that ran before stops running.

---

Second commit: §7.9 enforcement mechanism

The first commit made the sealed tier true. It did not make it checkable — §7.5 says outright that S0–S5 carry no in-band evidence, so the honest S0 it now produces is still just the host'''s word.

§7.9 adds an optional mechanism: the enforcement runtime (name and version) plus a commitment to the policy profile applied and the egress allowlist installed. Carrying one makes the attestation sandbox.attestation/2; without one it stays /1 and canonicalizes to byte-identical JSON — the same add-field/bump-profile/dispatch shape used for payload_hash.

What it deliberately does not claim. A mechanism is not proof of isolation, and both the SPEC text and the type docs say so. A host willing to misstate its tier can misstate its profile. What changes is the shape of the claim: an unadorned tier label is unfalsifiable, a profile_id is checkable against a known-good profile. A party needing proof still requires S6+.

Notable decisions:

• Length-prefixed commitment, not concatenation — "seatbelt/14"+"5;deny-net" and "seatbelt/145"+";deny-net" would otherwise collide. C11 asserts they do not.
• Relying-party requirement, not producer obligation — mandating it would retroactively invalidate every honest attestation sealed before §7.9. Lives in require_mechanism_evidence().
• S0 refuses a mechanism — unconfined by definition, so describing a boundary is incoherent, not redundant.
• Executor::mechanism() defaults to None — as with attained_tier(), the component that did the work describes it; silence beats invention.
• WasmExecutor is a real producer, so the field is not decorative. It commits to fuel metering, fuel budget and memory cap — deliberately not uj_per_million_fuel, an accounting coefficient that confines nothing.
• WASMTIME_VERSION is drift-tested against Cargo.lock — wasmtime exposes no version constant, and a stale value would attest confinement to a runtime that did not run.

Verified: 194 workspace tests pass; conformance passes with no skips across all 11 classes. C4 attestation.json — a published vector — still passes untouched, which is the backward-compatibility claim holding in practice rather than in argument.

The two commits are one arc (make the tier true, then make it checkable) and are independent of each other — say the word if you'''d rather they were separate PRs.

Third commit: S7 locality (§7.7)

Locality { region: String, jurisdiction: String } — two free-text strings, supplied by the party under audit, checked for presence and nothing else, at the one tier whose entire purpose is jurisdictional. §7.7 already said a host "MUST NOT seal an S7 run whose execution it cannot bind to the stated locality" — an obligation with no mechanism behind it, and the first thing a data-residency auditor attacks.

The physics, and its limit

RTT to an anchor of known position bounds distance: a signal cannot outrun light, so rtt/2 × c is the farthest the host can be from it. The asymmetry is what makes it worth anything — latency is trivial to add and impossible to remove — so a host can always appear farther away than it is, never closer than physics permits.

That yields a test that falsifies but does not verify:

• It can refute a claim. If the claimed position is farther from an anchor than light could travel in the observed time, the claim is impossible, and that conclusion rests on trusting no one.
• It can never confirm one. Surviving every bound means "not excluded" and nothing more — the feasible region is an intersection of discs routinely spanning several jurisdictions.

So the passing verdict is named NotRefuted, there is deliberately no is_proven, and §7.7 forbids reporting a surviving claim as proven, verified, or attested.

Three rules that matter more than the arithmetic

• Only an independent anchor's signed observation counts. An RTT the host measured about itself is the same unchecked assertion as the region string it was meant to improve on, now with a number attached. Unsigned observations return Unsubstantiated — and that holds even when they would refute, because the rule is about provenance, not about which answer they happen to give.
• A host cannot seal an attestation its own evidence refutes. Not a marginal judgement about trust: a physical impossibility the host itself just recorded.
• The bound uses vacuum c, not a fibre constant. Costs sensitivity, buys certainty in the only direction that matters — a refutation under vacuum-c cannot be argued away by an unusual path.

It is timing-derived, so by this codebase's own rule (TimingIsNotAShunt, §6.3) it is its own evidence class: never the standing of the verified tee evidence at S6, and carrying no Provenance at all.

Verification

203 workspace tests; conformance passes all 12 classes with no skips (new C12 locality-evidence pins refutation, the unsigned rule, below-S7 rejection, and byte-identical absence); published vectors unchanged on disk; no clippy warnings in the new file.

`sandbox-build` sealed every command step as `Tier::S5`, but the step is run by `ProcessVmm::new` — a bare `Command::spawn`. No VMM, no guest kernel, no dedicated vCPU, and no `/dev/kvm` check anywhere on the path. The honest rung is `S0` ("process only; trusted code"), the floor. Build receipts were claiming hardware isolation for work that ran as an ordinary child process on the host. SPEC already forbids this — *"A host MUST NOT seal a tier a run did not execute at"* — so this is a conformance fix, not a change of meaning. ### Why structural rather than a `/dev/kvm` check at the call site The bug shape is **the caller asserts a tier**. A check bolted onto the one site leaves the next caller free to repeat it. Now the executor reports the tier instead: - `Vmm::attained_tier()` defaults to `Tier::S0`. The floor is the default deliberately: an implementor who forgets to override **under**-claims, which is survivable, rather than **over**-claiming, which makes a receipt a lie. - `ProcessVmm` is genuinely dual-use — supervising `firecracker` really is S5, supervising `cargo build` is not — and that cannot be inferred from a program name. So it is declared: `new` is S0, `supervising_vmm` may claim S5, and even then only where the host exposes hardware virtualization. - `MicroVmExecutor::tier()` delegates to its VMM instead of returning a static S5, so `Host::run_and_seal`'s executor-vs-required cross-check can no longer be satisfied by a run that never touched a hypervisor. - `sandbox-proof::prove_microvm` supervises the real firecracker binary behind an existing `/dev/kvm` guard, so it declares `supervising_vmm` and correctly keeps S5. **That path is unchanged in behaviour.** ### Verification - 188 workspace tests pass; conformance passes with no skips, **C5 `tier.json` included**. - Exactly one existing test changed — the one that encoded the bug in its name (`a_command_step_runs_in_the_microvm_and_seals_at_s5`). It failed with `left: S0, right: S5`, which is the fix working. - Two new contract tests pin the invariants: a supervised process never claims a virtualization tier, and the trait default is the floor. ### Blast radius Contained to `sandbox-rs`; no other workspace path-depends on these crates. Build receipts from this path now read S0 instead of S5 — that is the point, and it is a **downgrade of a claim, never of enforcement**: nothing that ran before stops running. --- ## Second commit: §7.9 enforcement mechanism The first commit made the sealed tier **true**. It did not make it **checkable** — §7.5 says outright that S0–S5 carry no in-band evidence, so the honest `S0` it now produces is still just the host'''s word. §7.9 adds an optional `mechanism`: the enforcement runtime (name **and** version) plus a commitment to the policy profile applied and the egress allowlist installed. Carrying one makes the attestation `sandbox.attestation/2`; without one it stays `/1` and canonicalizes to **byte-identical JSON** — the same add-field/bump-profile/dispatch shape used for `payload_hash`. **What it deliberately does not claim.** A mechanism is *not* proof of isolation, and both the SPEC text and the type docs say so. A host willing to misstate its tier can misstate its profile. What changes is the shape of the claim: an unadorned tier label is unfalsifiable, a `profile_id` is checkable against a known-good profile. A party needing proof still requires S6+. Notable decisions: - **Length-prefixed commitment**, not concatenation — `"seatbelt/14"+"5;deny-net"` and `"seatbelt/145"+";deny-net"` would otherwise collide. C11 asserts they do not. - **Relying-party requirement, not producer obligation** — mandating it would retroactively invalidate every honest attestation sealed before §7.9. Lives in `require_mechanism_evidence()`. - **S0 refuses a mechanism** — unconfined by definition, so describing a boundary is incoherent, not redundant. - **`Executor::mechanism()` defaults to `None`** — as with `attained_tier()`, the component that did the work describes it; silence beats invention. - **`WasmExecutor` is a real producer**, so the field is not decorative. It commits to fuel metering, fuel budget and memory cap — deliberately *not* `uj_per_million_fuel`, an accounting coefficient that confines nothing. - **`WASMTIME_VERSION` is drift-tested against Cargo.lock** — wasmtime exposes no version constant, and a stale value would attest confinement to a runtime that did not run. **Verified:** 194 workspace tests pass; conformance passes with no skips across all 11 classes. **C4 `attestation.json` — a published vector — still passes untouched**, which is the backward-compatibility claim holding in practice rather than in argument. *The two commits are one arc (make the tier true, then make it checkable) and are independent of each other — say the word if you'''d rather they were separate PRs.* --- ## Third commit: S7 locality (§7.7) `Locality { region: String, jurisdiction: String }` — two free-text strings, supplied by the party under audit, checked for **presence and nothing else**, at the one tier whose entire purpose is jurisdictional. §7.7 already said a host "MUST NOT seal an S7 run whose execution it cannot bind to the stated locality" — an obligation with no mechanism behind it, and the first thing a data-residency auditor attacks. ### The physics, and its limit RTT to an anchor of known position bounds distance: a signal cannot outrun light, so `rtt/2 × c` is the farthest the host can be from it. The asymmetry is what makes it worth anything — **latency is trivial to add and impossible to remove** — so a host can always appear *farther* away than it is, never *closer* than physics permits. That yields a test that **falsifies but does not verify**: - It can **refute** a claim. If the claimed position is farther from an anchor than light could travel in the observed time, the claim is impossible, and that conclusion rests on trusting no one. - It can **never confirm** one. Surviving every bound means "not excluded" and nothing more — the feasible region is an intersection of discs routinely spanning several jurisdictions. So the passing verdict is named `NotRefuted`, there is deliberately **no `is_proven`**, and §7.7 forbids reporting a surviving claim as proven, verified, or attested. ### Three rules that matter more than the arithmetic - **Only an independent anchor's signed observation counts.** An RTT the host measured about itself is the same unchecked assertion as the region string it was meant to improve on, now with a number attached. Unsigned observations return `Unsubstantiated` — and that holds **even when they would refute**, because the rule is about provenance, not about which answer they happen to give. - **A host cannot seal an attestation its own evidence refutes.** Not a marginal judgement about trust: a physical impossibility the host itself just recorded. - **The bound uses vacuum `c`, not a fibre constant.** Costs sensitivity, buys certainty in the only direction that matters — a refutation under vacuum-c cannot be argued away by an unusual path. It is timing-derived, so by this codebase's own rule (`TimingIsNotAShunt`, §6.3) it is **its own evidence class**: never the standing of the verified `tee` evidence at S6, and carrying no `Provenance` at all. ### Verification 203 workspace tests; conformance passes **all 12 classes** with no skips (new **C12 locality-evidence** pins refutation, the unsigned rule, below-S7 rejection, and byte-identical absence); published vectors unchanged on disk; no clippy warnings in the new file.

dcharlot added 1 commit 2026-08-24 23:34:10 -04:00

sandbox: seal the tier a run actually reached, never the one it intended ... 2aca070ef3

`sandbox-build` sealed every command step as `Tier::S5`. The step is run by
`ProcessVmm::new`, which is a bare `Command::spawn` — no VMM, no guest kernel,
no dedicated vCPU, and no `/dev/kvm` check anywhere on the path. The rung it
actually reaches is `S0` ("process only; trusted code"), the floor. Build
receipts were therefore claiming hardware isolation for work that ran as an
ordinary child process on the host.

SPEC already forbids this — "A host MUST NOT seal a tier a run did not execute
at" — so this is a conformance fix, not a change of meaning.

The fix is structural rather than a `/dev/kvm` check bolted onto the one call
site, because the bug's shape is "the caller asserts a tier". Now the executor
reports one:

- `Vmm::attained_tier()` defaults to `Tier::S0`. The default is the floor on
  purpose: an implementor who forgets to override under-claims, which is
  survivable, instead of over-claiming, which makes a receipt a lie.
- `ProcessVmm` is genuinely dual-use — supervising `firecracker` really is S5,
  supervising `cargo build` is not — and that cannot be inferred from a program
  name. It is now declared: `new` is S0, `supervising_vmm` may claim S5, and
  even then only where the host exposes hardware virtualization.
- `MicroVmExecutor::tier()` delegates to its VMM instead of returning a static
  S5, so `Host::run_and_seal`'s executor-vs-required cross-check can no longer
  be passed by a run that never touched a hypervisor.
- `sandbox-proof::prove_microvm` supervises the real firecracker binary behind
  an existing `/dev/kvm` guard, so it declares `supervising_vmm` and keeps S5.

Verified: 188 workspace tests pass, conformance passes with no skips (C5
tier.json included). The one test that changed is the one that encoded the bug
in its name.

dcharlot changed title from sandbox: seal the tier a run actually reached, never the one it intended to sandbox: make the sealed tier true, then make it checkable (§7.9) 2026-08-24 23:59:09 -04:00

dcharlot added 1 commit 2026-08-24 23:59:09 -04:00

sandbox: let an S1-S5 attestation say how it confined the run (SPEC §7.9) ... 41dcdb9484

The previous commit made the sealed tier true. It did not make it checkable.
Below S6 the standard requires no evidence at all — §7.5 says so outright, and
`validate_structure` enforces evidence only at S6 (TEE) and S7 (locality) — so
`tier = "S2"` is the host's word with a signature around it, and the honest
`S0` the last commit produced is equally just the host's word.

§7.9 adds an optional `mechanism`: the enforcement runtime (name AND version)
plus a commitment to the policy profile applied and the egress allowlist
installed. An attestation carrying one is `sandbox.attestation/2`; without one
it stays `/1` and canonicalizes to byte-identical JSON, so every attestation
sealed before this section — and every published vector — verifies unchanged.
That is the same add-field/bump-profile/dispatch shape used for `payload_hash`.

What this is careful not to claim: a mechanism is NOT proof of isolation, and
both the SPEC text and the type docs say so. A host willing to misstate its
tier can misstate its profile; a commitment made by the party under scrutiny
cannot bootstrap its own trustworthiness. What changes is the shape of the
claim — an unadorned tier label is unfalsifiable, while a profile_id is
checkable against a known-good profile a relying party already trusts, and a
false one is a specific, attributable lie about a named artifact. A party that
needs proof rather than assertion still requires S6+.

Design notes:

- The commitment length-prefixes each field rather than concatenating them.
  Bare concatenation is not injective: "seatbelt/14" + "5;deny-net" and
  "seatbelt/145" + ";deny-net" would collide. C11 asserts they no longer do.
- Requiring a mechanism is a *relying-party* check, not a producer obligation.
  Making it mandatory would retroactively invalidate every honest attestation
  sealed before §7.9, and a standard does not get to make historical records
  non-conformant. It lives in `require_mechanism_evidence()`, the same posture
  §7.5 already takes for isolation proof.
- A mechanism at S0 is rejected, not ignored. S0 is unconfined; describing a
  boundary that does not exist is incoherent rather than merely redundant.
- `Executor::mechanism()` defaults to `None` — as with `attained_tier()`, the
  component that did the work is the one that gets to describe it, and silence
  beats invention. `run_and_seal` takes it from the executor; the bare
  `seal_run` primitive keeps its old signature and passes `None`.
- `WasmExecutor` is a real producer, so the field is not decorative: it commits
  to fuel metering, the fuel budget and the memory cap — deliberately NOT
  `uj_per_million_fuel`, an accounting coefficient that confines nothing and
  would make two identically-confined runs disagree when someone retunes it.
- wasmtime exposes no version constant and Cargo gives no compile-time access
  to a dependency's resolved version, so `WASMTIME_VERSION` is hand-maintained
  and a test fails the build if it drifts from Cargo.lock. A stale value would
  attest confinement to a runtime that did not run.

Verified: 194 workspace tests pass, conformance passes with no skips across all
11 classes. C4 attestation.json — a published vector — still passes untouched,
which is the backward-compatibility claim holding in practice rather than in
argument.

dcharlot added 1 commit 2026-08-26 11:52:34 -04:00

sandbox: give the S7 locality claim something that can falsify it (SPEC §7.7) ... 9ea6705110

`Locality { region: String, jurisdiction: String }` — two free-text strings,
supplied by the party under audit, checked for presence and nothing else, at the
one tier whose entire purpose is jurisdictional. SPEC §7.7 already said a host
"MUST NOT seal an S7 run whose execution it cannot bind to the stated locality",
which was an obligation with no mechanism behind it. It is the weakest normative
claim in the ladder and the first thing a data-residency auditor attacks.

Round-trip time to an anchor of known position bounds distance: a signal cannot
outrun light, so `rtt/2 × c` is the farthest the host can be from that anchor.
The asymmetry is what makes it worth anything — **latency is trivial to add and
impossible to remove** — so a host can always appear farther away than it is and
never closer than physics permits.

What that buys is narrow, and the code is named for it. The evidence
**falsifies; it does not verify**:

- It can refute a claim. If the claimed position is farther from an anchor than
  light could travel in the observed time, the claim is impossible, and that
  conclusion does not rest on trusting anyone.
- It can never confirm one. Surviving every bound means "not excluded" and
  nothing more: the feasible region is an intersection of discs that routinely
  spans several jurisdictions. So the passing verdict is `NotRefuted`, there is
  deliberately no `is_proven`, and §7.7 forbids reporting a surviving claim as
  proven, verified, or attested.

Three rules that matter more than the arithmetic:

- **Only an independent anchor's signed observation counts.** A round-trip time
  the host measured about itself is the same unchecked assertion as the region
  string it was meant to improve on — now with a number attached. Unsigned
  observations return `Unsubstantiated` rather than being blended in, and that
  holds even when they would *refute*: the rule is about provenance, not about
  which answer they happen to give.
- **A host cannot seal an attestation its own evidence refutes.** That is not a
  marginal judgement about trust; it is a physical impossibility the host itself
  just recorded.
- **The bound uses vacuum c, not a fibre constant.** This costs sensitivity and
  buys certainty in the only direction that matters: a refutation under vacuum-c
  cannot be argued away by an unusual path.

It is timing-derived, so by this codebase's own rule (`TimingIsNotAShunt`, §6.3)
it is its own evidence class — it never reaches the standing of the verified
`tee` evidence at S6 and carries no `Provenance` at all.

Absent, the field is omitted and the canonical bytes are unchanged, so S7
attestations sealed before this section still verify — C12 asserts that
alongside the refutation, the unsigned-observation rule, and the below-S7
rejection.

Verified: 203 workspace tests pass, conformance passes all 12 classes with no
skips, published vectors unchanged on disk, no clippy warnings in the new file.

dcharlot changed title from sandbox: make the sealed tier true, then make it checkable (§7.9) to sandbox: make the tier true, make it checkable, and let S7 locality be falsified 2026-08-26 11:52:55 -04:00

dcharlot merged commit 71377d9d99 into main 2026-08-29 03:09:32 -04:00

dcharlot referenced this pull request from a commit 2026-08-29 03:09:34 -04:00

sandbox: make the tier true, make it checkable, and let S7 locality be falsified (#57)

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!57

No description provided.