Repository navigation
feat(bep): refuse undeclared egress and host mismatches, admit only when every check passes - #2450
Conversation
decide now checks the box's declared egress (BEP-022) and pins the Host header and absolute-form target to the connection authority (BEP-023), and admits only when every check passes (BEP-025). decide_plain applies both checks to a request with no sealed value. Three Kani harnesses cover the new checks, so scripts/kani.sh expects nine for bep.
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
|
Approved: no findings at Nothing to do. Clobber: none seen: the diff only adds checks to |
There was a problem hiding this comment.
Own review of a8e49e0 against the T6 plan block (BEP-022, BEP-023, BEP-025).
- BEP-022 (
prop_undeclared_egress_authority_is_refused):request_checkrefuses asoutside_declared_egresswhen the resolved egress list lacks the connection authority, indecideand indecide_plain, so the check holds with and without a sealed value, as the spec's property says. The third arm (any other facts, an admission has a declared authority) is the harness property in test form. Wildcard matching of the egress declaration is left to the shell, which the agent note records;bepdoes not depend onboxes. - BEP-023 (
prop_host_header_mismatch_is_refused):RequestAuthority::pinsrequiresHost(or:authority) equal to the connection authority and an absolute-form target, when present, equal too; a missingHostnever pins. That is the spec's "all three are equal", origin-form counting as the connection authority. Refusalhost_mismatchbefore substitution, in bothdecideanddecide_plain. - BEP-025 (
prop_admit_iff_every_check_passes): the oraclefailures()lists the checks of BEP-019 to BEP-024, BEP-031 and BEP-058 indecide's order, independently ofdecide, and the test asserts Admit exactly when none fails and Refuse naming the first otherwise, over a fullany_redemption()plus the two "reaching" variants that drive the earlier checks.kani_redeem_admits_iff_all_checks_passstates the same iff. BEP-064 (store-handle checks) is named by the spec property but is outside this task's covers and not built in this module; the oracle omits it and the agent note says so. The task that builds BEP-064 extends the oracle and the harness; no new issue, it is already a task in this epic's slice plan. - Order and purity: checks 9 and 10 run after the host-set checks, the earlier harnesses are unchanged,
decideanddecide_plainstay pure over owned values, and the markers test carriesoutside_declared_egressandhost_mismatch. - Layers:
crates/bep/src/redeem.rsandscripts/kani.sh(bep harness count 6 to 9) only, as planned. The connection span is still not wired (no TLS/socket shell), the same interim as T5.
Approval follows the arch ruling, the runtime review and the lanes (Kani lane supplies the deferred harness evidence).
Generated by Claude Code
There was a problem hiding this comment.
arch-review: CONDITIONS · 1 condition · the full ruling
The new egress and Host checks are in the right place, and they fail closed. The order is wrong. decide runs the egress check after the bound-set, current-set, expiry and revocation checks. Gatehouse §6.10 line 823 orders egress declaration as step 3, before the step 4 invariants. So a request outside both egress and the current set gets the audit marker outside_current_set, not outside_declared_egress. Move the egress check to directly after attribution, as C1 says.
Ruled at a8e49e0 against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
|
/revise minimal-arch ruled CONDITIONS on a8e49e0 (arch_rulings 81): one condition, C1, on the order of the egress check. Take it and nothing else:
The runtime review approved with no findings; arch accepted the placement, the fail-closed Generated by Claude Code |
Gatehouse makes egress declaration step 3, before the expiry, revocation, port and host-set checks. decide() now refuses OutsideDeclaredEgress after the BEP-020 attribution, and before Expired for a value open refused as expired. HostMismatch stays last. The module doc and the test oracle follow the new order.
|
Round 1 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A redemption whose authority is outside the box's declared egress is refused as outside_declared_egress right after attribution, before the expiry, revocation, port and host-set checks. A mismatched Host is still refused last. decide() admits only when every check passes, in the order the module doc lists. Notes from the agent: Revise round 1 (arch C1) in commit ede2b5f. decide() refuses Check::OutsideDeclaredEgress directly after the BEP-020 attribution match. In the Unsealed::Expired arm it refuses OutsideDeclaredEgress before Expired once attribution passes. NoLiveBox and CrossBox stay as they were. HostMismatch is now a direct request.pins() check after OutsideCurrentSet. decide_plain() and request_check() do not change. The module-doc list is renumbered: egress is check 4, request authority stays check 10, and the OffPort note now points to check 9. The Unsealed::from_open doc now says Expired applies once the attribution and the declared egress pass. The oracle failures() moves the egress entry to after CrossBox. The whole bep suite passes (67 tests). Kani harnesses are unchanged. kani_redeem_requires_egress_admission, kani_redeem_pins_request_authority and kani_redeem_admits_iff_all_checks_pass are deferred to the kani lane and were not run. scripts/kani.sh did not change this round. |
There was a problem hiding this comment.
arch-review: PASS · the full ruling
The compare fixes the step order. decide now checks the declared egress right after attribution, before expiry and the host sets. Section 6.10 gives this order. The pinning check is the last check before substitution, and a missing Host is refused. BEP-022, BEP-023 and BEP-025 conform, and no condition stays open. The new Kani harnesses are deferred to the advisory Kani lane and did not run.
Ruled at ede2b5f against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
There was a problem hiding this comment.
minimal-review — approval withheld
Verdict COMMENT — APPROVE withheld: 3 unresolved threads — minimal-arch[bot] crates/bep/src/redeem.rs, minimal-arch[bot] crates/bep/src/redeem.rs, minimal-arch[bot] crates/bep/src/redeem.rs. No findings.
Panel: 3 of 3 personas ran (correctness, security, supply-chain).
There was a problem hiding this comment.
minimal-review — approved
Verdict APPROVE — every review thread is resolved; @norrietaylor closed the last one. The review of ede2b5f65aa3 withheld this approval on the threads open then. Posted as a comment: the App cannot approve its own pull request; the check and the label carry it.
There was a problem hiding this comment.
Own review of ede2b5f (round 1 on arch C1). The one commit moves the BEP-022 egress refusal to directly after attribution, in the opened path and in the Unsealed::Expired arm, renumbers the module-doc list (egress 4, request authority 10) and moves the oracle entry to match. Nothing else changed: decide_plain, the three property tests' bodies and the Kani harnesses are as reviewed at a8e49e0, and the admit-iff property now follows the design's order. minimal-arch ruled PASS on this head. The three arch threads are resolved with the verification above. Approval follows the lanes.
Generated by Claude Code
There was a problem hiding this comment.
Approving for merge: T6 on ede2b5f (arch PASS 118521752109, review approved with no findings, three arch threads verified). Gate passes on ede2b5f (arch PASS, review concluded with no open threads, lanes green, squash subject lint-clean).
Generated by Claude Code
There was a problem hiding this comment.
arch-review: PASS · the full ruling
The new head is a merge of main. It does not change crates/bep/src/redeem.rs or scripts/kani.sh. Their diff against the base is the same as at ede2b5f6, which had a PASS. The new bep::http parser checks that Host is well-formed. It does not pin the request authority, so check 10 still owns the §6.10 pin. The ruling stays PASS.
Ruled at eb3e7f6 against gominimal/arch@109541a48c31 by claude-opus-5-5.
|
Round 2 of 10 on a failed check suite: the coder changed nothing. every commit this round put on the branch above eb3e7f6 is a merge of the base branch, so it carries no work of its own |
|
The red The same leaked gvproxy fails main's own run (39464338657) and #2457's, and 32 of the 39 harnesses never ran. This head is a merge of main over a diff in Generated by Claude Code |
T6 — Pin the request authority, re-check the box's egress, and admit only when every check passes
slice: S0
kind: task
covers: BEP-022, BEP-023, BEP-025
size: L
est: 150 code, 360 tests
executor: agent
difficulty: needs care
model: strongest
diagnostics: every refusal names its first failing check in the audit record's marker, which
min box audit <box>showsobservability: the connection span and the audit marker name a refusal's first failing check
layers:
- decide:
- crates/bep/src/redeem.rs: the BEP-022 and BEP-023 checks, and Admit iff every check passes, else Refuse naming the first failing one
- scripts/kani.sh: the added harnesses' count
test: cargo nextest run -p bep prop_undeclared_egress_authority_is_refused
test: cargo nextest run -p bep prop_host_header_mismatch_is_refused
test: cargo nextest run -p bep prop_admit_iff_every_check_passes
test (deferred: kani): cargo nextest run -p bep kani_redeem_requires_egress_admission
test (deferred: kani): cargo nextest run -p bep kani_redeem_pins_request_authority
test (deferred: kani): cargo nextest run -p bep kani_redeem_admits_iff_all_checks_pass
produces: none
consumes: none
proof: A mismatched Host or an egress-denied authority is refused, and the decision admits only when every check passes.
depends on:
- blocked by #2266
Proof
In crates/bep/src/redeem.rs, decide refuses a request to an authority outside the box's declared egress as outside_declared_egress. It refuses a request whose Host header or absolute-form target differs from the connection authority as host_mismatch. decide_plain makes the same two checks for a request with no sealed value. A property test and a Kani harness show that decide admits exactly when every check passes, and otherwise names the first failing check.
Notes from the agent: Deferred (lane: kani): kani_redeem_requires_egress_admission, kani_redeem_pins_request_authority and kani_redeem_admits_iff_all_checks_pass are written in the #[cfg(kani)] module, and scripts/kani.sh now expects 9 bep harnesses. I ran none of them. The new checks run last, as checks 9 (egress) and 10 (request authority). That order leaves the existing Kani harnesses unchanged. The decision gets the declared egress as a list of authorities that the shell resolves (Redemption::egress, Plain::egress). bep does not depend on boxes, and its Cargo.toml is outside the layers, so wildcard matching of an egress declaration is a job for the shell. A missing Host header (RequestAuthority::host = None) is refused as host_mismatch. The new audit markers are outside_declared_egress and host_mismatch. The spec fixes no wording for them. The task's observability line asks for the connection span to name the check. No TLS or socket shell exists in bep yet, so no span records it. The shell task needs to put Check::marker on its span. BEP-025's property also names BEP-064 (store-handle checks). BEP-064 is not built in this module and is not in this task's covers, so the oracle in prop_admit_iff_every_check_passes leaves it out.
Tests
cargo nextest run -p bep prop_undeclared_egress_authority_is_refusedcargo nextest run -p bep prop_host_header_mismatch_is_refusedcargo nextest run -p bep prop_admit_iff_every_check_passesVerify
min task run agent-verifypassed ([tasks.verify]).Deferred
The plan marked these test lines deferred: the executor lacks the lane, so nothing here ran them and they still owe evidence.
cargo nextest run -p bep kani_redeem_requires_egress_admissioncargo nextest run -p bep kani_redeem_pins_request_authoritycargo nextest run -p bep kani_redeem_admits_iff_all_checks_passCloses #2268