Repository navigation
feat(bep): record a revocation when a live box is destroyed (T20) - #2548
norrietaylor merged 17 commits into
Conversation
The control socket takes record_mint and revoke_box. Both append to the proxy's one audit log, and a revocation goes into the set the redeemer reads, so a revoked box's values are refused before any resolution (BEP-043, BEP-067, BEP-071). bep serve wires the set and the log.
After the client key registration, the client sends record_mint for each grant it minted, so the proxy appends a mint record to its audit log. A failed record is a warning and the mint stands.
When the creator withdraws a live box with a credentialed lane, minvmd sends revoke_box and then forget_box to the Box Egress Proxy control socket, on a thread of its own. The destroy does not wait. With the proxy unreachable it logs one warning, and the withdrawn attachment refuses the box's values.
Two live proxy cases: with the proxy up, min box audit shows the destroyed box's revocation record within 60 s, and the copied value is refused. With the proxy down, the destroy completes, minvmd warns, and the value is refused after the proxy returns.
…evocation-when-a-live-box-is-destroyed # Conflicts: # crates/bep/src/control.rs
|
Important Review skippedBot user detected. To trigger a single review, invoke the
|
|
Reviewed: no findings; approval withheld, 2 threads unresolved at APPROVE withheld: 2 unresolved threads — minimal-arch[bot] scripts/session-e2e.sh:12095, minimal-arch[bot] scripts/session-e2e.sh:12165. Resolving the last thread releases the approval on this head. Resolve the open threads. Resolving the last one releases the approval on this head; no new review is required. Clobber: none seen in the changed hunks. |
…evocation-when-a-live-box-is-destroyed
There was a problem hiding this comment.
arch-review: CONDITIONS · 3 conditions · the full ruling
The revocation path is in the right owner, and it does what Gatehouse §6.10 line 839 requires. minvmd revokes a live box at its destroy, the proxy is the log's one writer, and a revoked value is refused before any renewal. Three items stay open. Run the two e2e legs on the macOS lane (C1), because both print NOT RUN. Correct the interim comments in crates/bep/src/redeemer.rs that say nothing writes a revocation (C2). Make the redeemer use revoke::in_force_for, so the BEP-071 property proves the redemption path (C3).
Ruled at dff3308 against gominimal/arch@109541a48c31 by claude-opus-5-5.
The connect-site inventory test failed in CI because the new mint_and_destroy_append_audit_records test opens a proxy control socket that the inventory did not list.
|
Round 1 of 10 on a failed check suite, pushed as
Verify After Notes from the agent: The CI |
There was a problem hiding this comment.
arch-review: CONDITIONS · 2 conditions · the full ruling
The code conforms to Gatehouse §6.10 line 839. The creator in minvmd records the revocation at the destroy of a live box. The proxy is the only writer of the log, and a revoked value is refused before any resolution. Two items stay open. The interim notes in crates/bep/src/redeemer.rs still say that nothing writes a revocation until T20, and this PR is T20 (C1). Both BEP-043 e2e legs recorded NOT RUN, so the T0 proof is open. Run them on the macOS lane at this head (C2).
Outside the diff
crates/bep/src/redeemer.rs:107: C1 · This interim note is now false.bep serverecords revocations throughrevoke_box(main.rswire). Rewrite it to name only the T33 restore-on-start (#2290) as the open interim and its flip. Make the same change at lines 223–224 infacts.
Ruled at b75eb97 against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
/revise Round 2 of #2548, on the arch ruling at dff3308 and the review findings left open. No round is in flight. T20's layers were widened on 2026-10-25:
One or two commits, Conventional Commits subjects, body lines at most 100 characters. Generated by Claude Code |
Build the revoked set with revoke::in_force_for for the box id the value names, so decide reads only the revocations that cover it. The doc comments now say that revoke_box puts a revocation in force, and that the empty set at start is the one interim left until #2290.
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The change conforms to Gatehouse §6.10 line 839. The destroy of a live box records one revocation in the proxy's single audit log. The redeemer reads only the revocations for the value's own box id. With the proxy down, the destroy completes and the withdrawn attachment refuses the values. Both BEP-043 e2e cases recorded NOT RUN, and NOT RUN is not a pass. C1 asks the macOS lane to record both cases as passed on this head.
Ruled at 1ff95e4 against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
Round 2 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
After Notes from the agent: Round 2 changes only crates/bep/src/redeemer.rs (commit 1ff95e4). C3: the revoked set is now built with crate::revoke::in_force_for. The filter key is the box id the value opened under (Unsealed::Opened box_id), not the source's box id. For a host_ip cohort member these two ids are different, and decide compares against the value's id. A value that did not open gets an empty set, because decide refuses it before it reads the set. C2: both doc comments are rewritten as the directive asks. NOT RUN: ./scripts/session-e2e.sh bep_destroyed_box_values_refused_within_60s and ./scripts/session-e2e.sh bep_destroy_with_proxy_down_refuses_by_attachment. Both need a live proxy and a GitHub sign-in on the Apple Silicon runner, and the epic owner runs that leg by hand. Finding 4369576614 ( |
…evocation-when-a-live-box-is-destroyed # Conflicts: # crates/bep/src/control.rs # crates/bep/src/main.rs
Each control request now has its own connection, so forget_box is sent when revoke_box is refused or times out. The warn line names the step that failed. bep's handle_line now refuses record_mint and revoke_box, since it keeps no record, and the minimal stubs answer those two.
|
A merge of main before round 3, not counted against the cap (1 of 3), pushed as Resolved conflicts in:
Verify Review threads the coder judged:
After Notes from the agent: Conflict round: control.rs and main.rs conflicted with main's signing-CA rotation (with_rotation, RotationRequest in serve). I kept both sides. Control keeps its Records and also carries the rotation into serve. main.rs calls .control(&control, log).with_rotation(ca). Committed as the merge. bep suite passes (159). Extra checks: cargo nextest run -p minvmd destroy_ (3 passed, includes the new destroy_forgets_the_box_when_the_revocation_is_refused), -p minimal mint (13 passed). NOT RUN: ./scripts/session-e2e.sh bep_destroyed_box_values_refused_within_60s and ./scripts/session-e2e.sh bep_destroy_with_proxy_down_refuses_by_attachment. This Linux box has no /dev/kvm and is not macOS, so it cannot boot the microVM. The macOS or linux-kvm lane still owes that evidence. The spec rejects a client-side revocation queue (spec rationale: 'holding the record in the client would add a queue that protects nothing the withdrawal does not'), so I did not add one. |
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The compare conforms to Gatehouse §6.10 line 839. A failed revoke_box no longer stops forget_box, and handle_line refuses the two requests it cannot record. The work that stays open is the e2e evidence. Both e2e cases recorded NOT RUN on Linux, and NOT RUN is not a pass. Run them on the macOS lane at this head, as C1 says. Restore at start stays with #2290.
Ruled at 97ccc6e against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
/revise Round 3 of #2548, on the two review findings opened at 97ccc6e. No round is in flight. Arch C1, the two macOS end-to-end cases (
One commit, Conventional Commits subject, body lines at most 100 characters. Generated by Claude Code |
BoxRegistry::new no longer reads cfg!(test). It sets no proxy control socket, so a test's or any other build's registry never sends a revocation to a developer's running proxy. The supervisor's start path builds its registry through supervisor_registry, which 8 sets the 10BC8 home-directory socket with with_proxy_control. Move the Clone doc comment back onto impl Clone for BoxRegistry, below the new consts and spawn_revocation. Tests: new_registry_sends_no_revocation, supervisor_registry_sends_revocations_to_the_home_proxy.
There was a problem hiding this comment.
minimal-review — approval withheld
Verdict COMMENT — APPROVE withheld: 6 unresolved threads — minimal-arch[bot] scripts/session-e2e.sh:12090, minimal-arch[bot] scripts/session-e2e.sh:12157, minimal-arch[bot] scripts/session-e2e.sh:12090, minimal-foundry[bot] crates/minvmd/src/box_registry.rs:4554, minimal-foundry[bot] crates/minvmd/src/box_registry.rs:2922, …. No findings.
Panel: 3 of 3 personas ran (correctness, security, supply-chain).
|
Round 6 of 10 on a /revise note, pushed as
Verify Outside the task's
Converted to a draft: something above needs a person before review. Review threads the coder judged:
After Notes from the agent: Round 6. Finding 4369995984 is invalid, and the code shows why. In production only withdraw_expired_detached reaches withdraw_where. The public withdraw has callers only in tests. A live client row always has a standing creation, because register_client_box_as refuses a name a live row holds (NameAlreadyHeld). So withdraw_where makes that creation dormant (creation_rowless), and resume_client_box can bring the box back under the same box id. A revocation refuses that id for good (BEP-071). A revocation at expiry will then refuse the values of the resumed box. BEP-043 makes the destroy of a live box the one revocation event, and its rationale says the withdrawn attachment refuses a stopped box's values. Commit f5e53bf adds no revocation. It adds a doc paragraph on withdraw_where and the test expired_credentialed_box_sends_no_revocation_and_stays_resumable, which pins the expiry path. Thread 4369995982 stays as ruled: spawn_revocation's retry behaviour is unchanged, per the directive. The two session-e2e.sh cases are NOT RUN: they are macOS microVM cases, and they are the epic owner's run under the manual-only stance. The C1 and C2 threads stay open for that reason. Clippy on minvmd showed one warning, in minimald-rpc, which is outside this diff. |
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The compare conforms to Gatehouse §6.10 line 839. When a detached box expires, its creation becomes dormant and the creator can resume it. So the expiry is not a destroy, and minvmd correctly sends no revocation. BEP-043, BEP-067 and BEP-071 conform in code. Both live e2e legs recorded NOT RUN, so C1 stays open: record PASS for both on the macOS lane, or file an issue for them. Restore at start remains the T33 residual (#2290).
Ruled at f5e53bf against gominimal/arch@109541a48c31 by claude-opus-5-5.
…evocation-when-a-live-box-is-destroyed # Conflicts: # scripts/session-e2e.sh
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
This head merges main into the branch. The PR's own changes are the same as at f5e53bf2, and the earlier ruling stands. Revocation on a live destroy, exact-id coverage and the shared audit log conform to Gatehouse §6.10 line 839. The two macOS e2e legs still record NOT RUN, so the 60 s bound (§6.10 line 823) has no live proof. Run both cases on the macOS lane and record them as passed (C1). Restore at start stays a residual for T33 (#2290).
Ruled at 74e011b against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
A merge of main before round 7, not counted against the cap (2 of 3), pushed as Resolved conflicts in:
Verify Outside the task's
Converted to a draft: something above needs a person before review. After Notes from the agent: This round resolved the merge conflict in scripts/session-e2e.sh only. The conflict was in the case dispatch list and in the usage text. Both sides added cases there: this branch added the two bep_destroy cases, and main added bep_dns_steering_fails_closed_end_to_end. The resolution keeps all three. The whole-lane order merged cleanly and also lists all three. The other files in the merge commit come from main. The two e2e cases print NOT RUN on this Linux host and exit 0. That is not a pass. The macOS lane still owes their evidence, as the earlier threads (C1, C2) ask. No verdict on an earlier thread changed this round. |
There was a problem hiding this comment.
Babysitter approval at 74e011b: every merge gate passes at this head (arch's conditions are the macOS legs, filed as residual #2564 by the epic owner's decision; zero open threads; every lane aggregator green). Squash title feat(bep): record a revocation when a live box is destroyed (T20) and the squashed message pass commitlint. Queued for squash merge.
Generated by Claude Code
…evocation-when-a-live-box-is-destroyed # Conflicts: # scripts/session-e2e.sh
…evocation-when-a-live-box-is-destroyed
There was a problem hiding this comment.
arch-review: PASS_WITH_CONDITIONS · 1 condition · the full ruling
The PR's own hunks did not change since 74e011bb. The two merges from main keep both sides of the scripts/session-e2e.sh conflict. The ruling on 74e011bb stands. A revocation is recorded only on a live destroy, covers exactly its box id, and is checked before any resolution (Gatehouse §6.10 line 839). The two macOS e2e legs recorded NOT RUN, so C1 keeps them open under #2564 until they pass on the macOS lane.
Ruled at 20f42cf against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
A merge of main before round 7, not counted against the cap (3 of 3), pushed as Resolved conflicts in:
Verify Outside the task's
Converted to a draft: something above needs a person before review. After Notes from the agent: This round resolves the merge conflict with main in scripts/session-e2e.sh. Both sides added new e2e cases at the same place. The resolution keeps this branch's destroy-revocation helpers and its two cases, and then adds main's proof_bep_signing_rotation_keeps_running_box_working in full. Git aligned the two blocks on a few shared seed lines, so each side was rebuilt in full with those lines. The script passes bash -n, and every line from both sides is present. The other files from main (crates/bep/src/lib.rs, store.rs, crates/minimal cli.rs, cmd/mod.rs, cmd/secret.rs) merged without conflict. Those changes come from main and are not work for this task. The two e2e cases report NOT RUN on this Linux box with no /dev/kvm, because the proxy cases run on macOS only. They still owe their evidence on the macOS lane. |
Pull request was converted to draft
There was a problem hiding this comment.
Babysitter approval at 20f42cf: every merge gate passes at this head (arch PASS at 20f42cf, zero open threads, every lane aggregator green). Squash title feat(bep): record a revocation when a live box is destroyed (T20) and the squashed message pass commitlint. Queued for squash merge.
Generated by Claude Code
T20 — Record a revocation when a live box is destroyed and refuse its values within a minute
slice: S1
kind: task
covers: BEP-043, BEP-067, BEP-071
size: L
est: 380 code, 440 tests
executor: agent
difficulty: needs care
model: strongest
diagnostics:
min box audit <box>shows the box'srevocationrecord and each later refusal of its valuesobservability: one info log line per revocation recorded, naming the box id; one warn line when a destroy completes with the proxy unreachable
layers:
- proxy:
- crates/bep/src/revoke.rs (new): revocations by box id, consulted before any resolution (BEP-071)
- crates/bep/src/control.rs: takes mint and revocation submissions and appends them to the one log
- crates/bep/src/lib.rs: module line
test: cargo nextest run -p bep prop_revocation_covers_exactly_its_box
test: cargo nextest run -p bep revoked_value_never_triggers_renewal
- client:
- crates/minimal/src/mint.rs: submits a
mintrecord per member- crates/minvmd/src/box_registry.rs: on a live box's destroy submits its revocation and sends
forget_boxover the control socket, so the proxy attributes the id to no live box (T41, #2483), completing the destroy when the proxy is down- crates/bep/src/main.rs: drops the box-egress interim from the
bep servestartup warning and thewirecomment if T14 has not already, since this task is the destroy half of that fliptest: cargo nextest run -p minimal mint_and_destroy_append_audit_records
- e2e:
- scripts/session-e2e.sh: adds two cases
test: ./scripts/session-e2e.sh bep_destroyed_box_values_refused_within_60s
test: ./scripts/session-e2e.sh bep_destroy_with_proxy_down_refuses_by_attachment
produces:
- crates/bep/src/revoke.rs
consumes:
- crates/bep/src/control.rs
- crates/minimal/src/mint.rs
proof: After
min session destroy web, a value copied from web is refused within a minute, even if the proxy was down.depends on:
- blocked by #2271
- blocked by #2273
- blocked by #2276
Proof
After
min session destroy web, minvmd sends revoke_box for web's box id to the proxy. The proxy puts the revocation in force at once and appends onerevocationrecord, whichmin box audit webshows. Later requests that carry web's sealed value are refused before any sign-in is resolved or renewed. With the proxy down, the destroy still completes, minvmd logs one warning, and the withdrawn attachment refuses the value. On this branch, the two bep tests and the minimal test show this in code. The two e2e cases that show it on a live macOS host are written, but they recorded NOT RUN on this Linux box.Notes from the agent: The e2e cases recorded NOT RUN here because bep_live_gate needs macOS, gvproxy and a GitHub sign-in. The macOS lane still owes that evidence. The decision checks cross_box before revoked, so a value copied into another box is refused as cross_box even with a revocation in force. For that reason the e2e case checks two things: the
revocationrecord in web's audit within 60 s, and the refusal. Therevokedmarker itself is proved by revoked_value_never_triggers_renewal. Changes in tests.rs: the mint tests and their stub control servers live there, so the new test went there, and the two stub servers got match arms for the new record_mint and revoke_box requests. minvmd: the revocation runs on a thread of its own, so the destroy never waits, and the stop path (withdraw_where) sends none, because the spec says that reaping a stopped box is not a revocation. minvmd also gets a unit test, destroy_revocation_sends_revoke_then_forget (passes). In unit tests the registry has no proxy socket (cfg!(test)). Its builder is with_proxy_control. Outside the layers and not changed: the doc comments in crates/bep/src/redeemer.rs (lines ~107-113 and ~170) still say that nothing writes revocations until T20. They are now out of date. Revocations recorded before a proxy start are not restored: that is T33 (#2290), and thebep servewarning says so…[truncated]Tests
cargo nextest run -p bep prop_revocation_covers_exactly_its_boxcargo nextest run -p bep revoked_value_never_triggers_renewalcargo nextest run -p minimal mint_and_destroy_append_audit_records./scripts/session-e2e.sh bep_destroyed_box_values_refused_within_60s./scripts/session-e2e.sh bep_destroy_with_proxy_down_refuses_by_attachmentVerify
min task run agent-verifyexited 101 under rustc 1.98.1, which the repository does not pin (1.97.0 in rust-toolchain.toml); the PR is not a draft on that alone — CI, which honours the pin, is the gate.Base
The base branch moved while the coder worked and was merged in before the tests ran. These files changed on BOTH sides since the branch point — read them first, because a rewrite from a stale reading can undo a merge without a conflict:
crates/bep/src/control.rscrates/minimal/src/mint.rscrates/minimal/src/tests.rsOut of scope
Layer exception
The task's layers were widened on 2026-10-25 in the plan comment and in #2277:
crates/minimal/src/tests.rs(the mint tests and their stub control servers live there),crates/bep/src/redeemer.rs(arch C2 and C3),crates/minvmd/src/cmd/run.rs(the supervisor start path sets the proxy control socket throughwith_proxy_control, review finding 4369790164),crates/bep/src/proxy.rs(AuditWriter::try_writereports an append failure so a lost revocation record is never silent, review finding 4369863226), andcrates/bep/src/lib.rs(the onemod revoke;line; it left the layer list on 2026-10-25 so the task stays within the runtime's ten-file cap). Each is required by the task's own proof and is accepted under the epic owner's layer-exception rule, so the PR is not a draft for them.These files are outside the task's
layers:, so this PR is a draft:crates/minimal/src/tests.rsResiduals
mainon the manual macOS lane of T82 — Run the Box Egress Proxy legs on the macOS lane #2500 (epic owner's decision, 2026-10-25; arch's conditions on the legs).Closes #2277
Generated by Claude Code