Repository navigation
feat(bep): refuse off-set authorities, off-port connections and expired or revoked values - #2448
Conversation
decide now refuses a value whose clock is at or after its expiry, or whose box a revocation in force names (BEP-024). It refuses a connection to a credentialed hostname on an undeclared port (BEP-031), and an authority outside the bound or the current host set (BEP-021). Each refusal names its check as an audit marker: expired, revoked, off_port, outside_bound_set or outside_current_set. Add three Kani harnesses and expect six in scripts/kani.sh.
|
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: 1 finding, none above this repo's threshold at Nothing to do. Verdict APPROVE, posted as a comment: the App cannot review its own pull request; the check and the label carry it. Clobber: none seen. |
There was a problem hiding this comment.
arch-review: PASS · the full ruling
The change conforms to Gatehouse §6.10. decide admits a value only when the authority is in both the bound set and the current set (line 851). It refuses a credentialed hostname on an undeclared port (line 851). It refuses an expired blob and a box that a revocation in force names (lines 823 and 839). Every new path fails closed. The Kani harnesses are still deferred to the advisory lane, the same as #2359.
Ruled at 75978ed against gominimal/arch@3dab1097cda1 by claude-opus-5-5.
There was a problem hiding this comment.
Own review of 75978ed against the T5 plan block (BEP-021, BEP-024, BEP-031).
- BEP-021 (
prop_authority_outside_bound_or_current_set_is_refused):decideadmits only whenauthorityis inbound_setand incurrent_set; the property assertsadmitted == in_bound && in_currentover every bound set, current set and authority, which is the spec's property verbatim. Refusal markersoutside_bound_set/outside_current_setname the first failing check. - BEP-024 (
prop_expired_or_revoked_value_is_refused):now >= expiryrefuses asexpired, a revocation in force naming the box refuses asrevoked;Unsealed::ExpiredfromOpenError::Expiredis refused asexpiredafter attribution, and an opened value carries the earlier of the value and member expiry (from_open_expired_is_refused_as_expiredchecks 2 000). Property matches the spec's. - BEP-031 (
prop_off_port_connection_is_refused): a hostname present in the current set on an undeclared port refuses asoff_port; a hostname absent from the set is not credentialed and falls to the set checks. Property matches the spec's. - Harnesses:
kani_redeem_requires_authority_in_both_sets,kani_redeem_refuses_expired_or_revoked,kani_redeem_enforces_port_disciplinepresent,scripts/kani.shexpects 6 bep harnesses, and the Kani lane is green on this head, which supplies the evidence the PR body lists as deferred. - Purity and order:
decidestays pure over owned values; the check order after attribution is expired, revoked, off_port, outside_bound_set, outside_current_set, and every refusal names its first failing check (Check::marker, markers test updated). - Layers:
crates/bep/src/redeem.rsandscripts/kani.shonly, as the plan lists. The connection span is not wired (no TLS/socket shell yet); the marker is the surface today, as the agent note says. - Threads: the one runtime NIT (doc wording on check order) is verified true and resolved as optional.
minimal-arch ruled PASS on this head. Approval follows the macOS lane.
Generated by Claude Code
There was a problem hiding this comment.
Approving for merge: T5 on 75978ed (arch PASS 118478880516, own review, Kani lane green). Gate passes on 75978ed (arch PASS, review concluded with no open threads, lanes green, squash subject lint-clean).
Generated by Claude Code
T5 — Refuse authorities outside both host sets, off-port connections, and expired or revoked values
slice: S0
kind: task
covers: BEP-021, BEP-024, BEP-031
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-021, BEP-024 and BEP-031 checks
- scripts/kani.sh: the added harnesses' count
test: cargo nextest run -p bep prop_authority_outside_bound_or_current_set_is_refused
test: cargo nextest run -p bep prop_expired_or_revoked_value_is_refused
test: cargo nextest run -p bep prop_off_port_connection_is_refused
test (deferred: kani): cargo nextest run -p bep kani_redeem_requires_authority_in_both_sets
test (deferred: kani): cargo nextest run -p bep kani_redeem_refuses_expired_or_revoked
test (deferred: kani): cargo nextest run -p bep kani_redeem_enforces_port_discipline
produces: none
consumes:
- crates/bep/src/redeem.rs
proof: A request outside either host set, on another port, or with an expired or revoked value is refused.
depends on:
- blocked by #2260
Proof
redeem::decide now refuses a request when the connection authority is outside the value's bound host set (outside_bound_set) or the module's current host set (outside_current_set). It also refuses a credentialed hostname on an undeclared port (off_port), a value at or past its expiry (expired), and a value whose box a revocation in force names (revoked). Each marker is the audit record's marker for the refusal.
Notes from the agent: Deferred (lane: kani): kani_redeem_requires_authority_in_both_sets, kani_redeem_refuses_expired_or_revoked and kani_redeem_enforces_port_discipline are written in redeem.rs, but they did not run on this box. scripts/kani.sh now expects 6 bep harnesses. All six bep harnesses carry #[kani::unwind(6)], because the redemption now holds host sets of at most 4 authorities and at most 2 revocations as Vecs. The memory use of the existing three harnesses with this wider input is not measured. Design decisions: Redemption is now Redemption<B, H> and has new fields now, revoked (the box ids that the revocations in force name, which the shell selects), authority, bound_set and current_set. Authority is a host id with a port. Unsealed has a new Expired variant, which from_open maps from OpenError::Expired. Opened carries the earlier of the context and member expiry. The check order after attribution is expired, revoked, off_port, outside_bound_set, outside_current_set. off_port fires only when the current set has the hostname on another port. A hostname absent from the current set is outside_current_set (or outside_bound_set first). The connection span is not in this change: no TLS and socket shell exists yet to carry it, so the marker is the only surface today. The run of the redeem tests (12) passed.
Tests
cargo nextest run -p bep prop_authority_outside_bound_or_current_set_is_refusedcargo nextest run -p bep prop_expired_or_revoked_value_is_refusedcargo nextest run -p bep prop_off_port_connection_is_refusedVerify
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_authority_in_both_setscargo nextest run -p bep kani_redeem_refuses_expired_or_revokedcargo nextest run -p bep kani_redeem_enforces_port_disciplineCloses #2266