Repository navigation
T31 — Resolve and reach sibling boxes by name under both boxes' rules - #1766
norrietaylor merged 13 commits into
Conversation
… scan The egress verdict's infrastructure scan refused every address in the switch's reserved plane, including the box-zone addresses a guest must reach. Move the plane out of the always-refused set so a box-zone answer declared as such is scanned against the fixed infrastructure addresses only, while every other answer keeps the plane refused.
…0s ran out the coder's uncommitted work as it stood when its 7200s ran out The coder was stopped at the end of its time with these changes not committed. The runtime committed its working tree as it stood so the work is kept: this commit is a snapshot, not a finished step, and may not build or pass its tests.
…d-reach-sibling-boxes-by-name-under-bo
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Comment |
…d-reach-sibling-boxes-by-name-under-bo
|
Round 1 of 10 on a failed check suite: the coder changed nothing. every commit this round put on the branch above |
The snapshot's NET-073 connect-time check was left with three compile errors: a `HashMap` built in a `const` item, which needs a `LazyLock` static instead, and the source lookup passing `&Ipv4Addr` where the table is keyed by value. The whole PR's check suite was red on the build, so nothing could run.
The daemon layer's half of T31: two proofs for NET-072 and NET-073 against the real relays. `box_zone_resolution_needs_no_allow_entry` (dns_gate) drives a box that allows `github.com` and, by address, nothing else through a resolution of its sibling's zone name: the query rides the resolver carve-out, the reply passes through to the box, and the sibling's lease is pinned and reachable with no allowlist entry naming it and no subnet declaring it. The carve-out is then proved to be the zone's alone — an ordinary name with no entry resolves but admits nothing, and a lookalike that merely ends in the zone's words (a distinct address, since the admission table is keyed by address) pins nothing either. `box_zone_connection_enforced_at_connect` (switch) puts two boxes' relays live at once and decides the same connection four ways at the target's relay, on the SYN itself: refused by the source's own egress rules before the resolution; admitted by both halves after it (the source's pin beside the target's declared port); refused by the target's ingress gate alone when the source's half admits the address but the port is undeclared; and untouched for a source that is not a live box on this daemon's switch, which keeps the target-ingress-only behavior. Each connection says one debug line naming the source box, the target box and each side's verdict, and each refusal also says a warn line under the refusing box's label with the rule — the two lines the diagnostics bundle's daemon log tail is read for. Along the way: `is_zone_name` gets the unit test that pins its boundary (the apex and its names, never a name that merely carries the zone's words), and the DNS gate's test harness items the switch proof needs (the resolver address, the DNS frame builders, the box-end reader) are shared as `pub(crate)` rather than copied — the same sharing direction the switch's harness already gives the gate's tests. The harness's global capture reads at INFO, so the switch proof installs its own thread-local capture at DEBUG for the connect-time line.
|
Round 2 of 10 on a failed check suite, pushed as
Verify A box now resolves a sibling's zone name with no allowlist entry for it — the query rides the resolver carve-out, the reply passes through to the box, and the sibling's lease is admitted as reach — and a connection to it succeeds only when the target's ingress rules and the source's egress rules both allow it: decided at the target's relay on the SYN itself (the source's half looked up by lease in LIVE_GATES, with the DNS pin the source's own relay granted), each connection saying one debug line naming the source box, the target box and each side's verdict, and each refusal a warn line under the refusing box's label with the rule — all four combinations proved end to end against two live relays, plus the fabric's own traffic left to the target's ingress decision alone. Notes from the agent: The round opened with the whole workspace failing to compile — the cause of every red check in the directive: the snapshot's LIVE_GATES table in switch.rs had three errors (a HashMap::new() in a |
There was a problem hiding this comment.
/revise one narrowing before this PR can leave draft; everything else in the T31 contract is met (all four layers present, policy.rs needed nothing because register_dns_name already puts sibling names in the zone on main, the three named tests are real and on-requirement, the connect-time debug line carries source, target and both verdicts, and Kani re-proves the non-zone decision unchanged).
MEDIUM: the zone carve-out admits a zone-name answer at any non-infrastructure address, not only a plane lease. rebinding_admits (crates/sessions/src/core/egress.rs:728-730) skips the 100.64.0.0/10 plane check when box_zone is set, but nothing then requires the answer to be inside the plane: a *.min.internal answer of 10.1.2.3 or a public address passes, and the sessions test asserts exactly that (egress.rs:1426, the private-zone-answer case). Because allows_name (crates/minimald/src/net/dns_gate.rs:342-347) now auto-allows every *.min.internal question, the gate pins every A record in such a reply (dns_gate.rs:461-482) with no allow entry from the box. The answerer serves its zone for A and forwards other types upstream (NET-136 intercepts only AAAA/HTTPS/SVCB), so a zone question that reaches the upstream path and comes back carrying A records is pinned into the box's egress table. The design's carve-out is for box-zone names naming sibling leases, nothing wider.
Change:
- In
rebinding_admits, replace theif !box_zone && infrastructure.plane.contains(answer)branch withif box_zone != infrastructure.plane.contains(answer) { return Err(RebindingRefusal::Infrastructure); }so a zone answer is admitted only inside the plane and a non-zone answer only outside it. - Update the sessions test's private-zone-answer case to expect
Err(RebindingRefusal::Infrastructure), and add the positive case: a zone answer inside the plane is admitted. - Change the Kani oracle line (egress.rs:1739,
let plane = !box_zone && ...) tobox_zone != plane.contains(answer)so the proof keeps matching the code. - The three named test lines must still pass; run them.
Two LOW items to note in the PR body, no code change required: the target-side source check cannot refuse in production because the source relay's own egress leg already drops under the same rules (the test proves it by injecting on the target's switch side), and LIVE_GATES is process-global keyed by lease, so tests that register the same lease share it. Keep the commits already on the branch.
|
/revise one narrowing before this PR can leave draft; everything else in the T31 contract is met (all four layers present, policy.rs needed nothing because MEDIUM: the zone carve-out admits a zone-name answer at any non-infrastructure address, not only a plane lease. Change:
Two LOW items to note in the PR body, no code change required: the target-side source check cannot refuse in production because the source relay's own egress leg already drops under the same rules (the test proves it by injecting on the target's switch side), and |
The zone carve-out skipped the plane check outright, so a reply to a *.min.internal question could carry any non-infrastructure address -- RFC 1918 or a public host -- and, because the daemon-side gate auto-allows every zone question, pin it into the box's egress table with no allow entry from the box. The design's carve-out is for box- zone names naming sibling leases, which live in the plane; nothing wider. rebinding_admits now refuses the answer wherever the zone and the plane disagree: a zone answer is admitted inside the plane and nowhere else, an ordinary name's outside it and nowhere in it. The Kani oracle restates the same equality so the proof keeps matching the code, the sessions test asserts the refusal under every declaration shape and adds the positive case across the plane's span, and the dns gate's module doc names the narrowed semantics it composes with. Refs: #1766
|
Round 3 of 10 on a review requesting changes, pushed as
Verify A box still resolves a sibling's Notes from the agent: The review's MEDIUM is fixed in crates/sessions/src/core/egress.rs: rebinding_admits now returns RebindingRefusal::Infrastructure wherever the zone and the plane disagree (a zone answer only inside the plane, an ordinary name's only outside it), so the daemon-side gate — which auto-allows every *.min.internal question — can pin a zone reply's A records only where they are plane leases. The sessions test's private-zone-answer case now expects Err(RebindingRefusal::Infrastructure) under every declaration shape (open dimension, covering allow entry, deny-all declaration, plus a public answer), the positive case asserts admission across the plane's whole span, and the Kani oracle line is box_zone != plane.contains(answer) so the proof matches the code. Kani itself could not be run here (no cargo-kani on this box), so the oracle change is verified by inspection and the harness's equivalence claim rests with the ci-kani lane, which is advisory. The change is bit-identical for box_zone=false, so only the zone paths moved. dns_gate.rs changed only its module doc and one test doc comment, which still stated the pre-narrowing semantics. The two LOW items belong in the PR body, per the review, with no code change: (1) the target-side source check cannot refuse in production because the source relay's own egress leg already drops under the same rules — the test proves it by injecting on the target's switch side; (2) LIVE_GATES is process-global keyed by lease, so tests that register th…[truncated] |
There was a problem hiding this comment.
Round 3 (f8345b5) applies the plane-only carve-out exactly as asked, with the test and the Kani oracle following; the design check on NET-072/NET-073 passed. One defect the widened allows_name introduces, in the thread below, and one comment ask.
Recorded, no change needed: letting the box's own deny_subnets refuse a zone answer at resolution is stricter than the design (which exempts zone resolution from egress rules and decides at connect); net reach is identical.
`host.min.internal` is a zone name (NET-003), and inside an own-address box its reply carries the switch's NAT'd host alias — an address the infrastructure deny set names in its fixed range, because the alias is infrastructure by design. The widened `allows_name` from the box-zone carve-out therefore sent every host lookup through the rebinding intersection: the mandated answer was refused as infrastructure and the limiter wrote a false refusal line for each box that resolved the host. The row's reply now skips the pass entirely — it passes through to the box, pins nothing, warns nothing. The reach it grants was never the intersection's to give: reach over the name is local reach under the box's own egress rules, decided at connect by the frame verdict. A reply to the row's name carrying any other address is not the row and still meets the intersection like any subverted zone answer. The gate takes the subnet's host alias from the relay, and the unit-test fixture's deny-set alias is corrected to the default /16 subnet's real one (100.64.255.254, not 100.64.0.254 — no test depended on it). `box_zone_resolution_needs_no_allow_entry` gains the host-row case: the reply passes through byte-equal, the limiter emits no refusal line, and a connection to the alias is refused — nothing is admitted. Also say in `refuse_zone_connect`'s doc, per review, why the box-behind-another-daemon case is ingress-only: no such source can arrive on this switch, not because its egress goes unchecked — each daemon's gvproxy is its own L2 segment, and that box's host-address reach rides the host loopback under the host-side classifier.
|
Round 4 of 10 on a review requesting changes, pushed as
Verify Review threads the coder judged:
A box resolves a sibling's name with no allowlist entry, and a connection to it succeeds only when the target's ingress rules and the source's egress rules both allow it — and since this round the zone's own host row behaves the same from the box's side: resolving Notes from the agent: Round 4 (revise). Both threads judged valid and fixed in commit 9ce6a66. The MEDIUM fix is at the gate level, in minimald: the shared |
|
Approved: no findings 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. The base-branch-moved warning names |
|
Round 5 of 10 on the runtime's review findings: the coder changed nothing. No code change, on purpose: the finding was a verification gap, not a defect — the E0015/E0308/E0716 fixes it names were already in the tree, every proof it doubted passes, so there is nothing to commit. The LIVE_GATES caution is contained by design and now by evidence: register_live_gate is called only from spawn_relay, the connect proof's leases (100.64.0.10/.11) are registered by no other proof, no other proof writes a bare TCP SYN into a relay's switch side, and both proofs also pass inside the single-process libtest target. That libtest run ( |
There was a problem hiding this comment.
REQUEST_CHANGES — the KVM lane is red on every head of this PR, and the failure is a design conflict, not weather.
CI (Linux KVM) has failed on 0e0b44c, 319479a, 859677c, f8345b5 and 9ce6a66, each time at the landed NET-070 parity proof (scripts/session-e2e.sh, pair 5, "a caller whose egress rules deny the target", from #1730):
pair a caller whose egress rules deny the target
direct: GET http://e2e-par-own.min.internal:18087/ -> curl exit 0:
proxied: GET http://e2e-par-own.min.internal:18087/ via the proxy at the daemon's switch address -> HTTP 403 ()
##[error]the denied caller's direct attempt did not end in a connect timeout (curl exit 0, expected 28) — the caller's egress gate did not drop it
(run 36695398819, job 109833892861)
The caller is an own-address box whose only allow entry is --allow-subnets 100.64.255.253/32; the target's lease is undeclared. Before this PR its SYN was dropped (exit 28). With this PR the connection completes, because refuse_zone_connect lifts an UndeclaredSubnet drop whenever peer.dns.admits_flow(destination) holds, and this PR both exempts box-zone resolution from the allow-list and admits the zone answer into the pin table — so resolving a sibling's name now grants its lease. That reads NET-072 (resolution needs no allow entry) as "resolution grants reach", which contradicts NET-070, NET-073 ("enforce … the source's egress rules at connection time") and this task's own proof line ("a connection to it succeeds only when the target's ingress rules and the source's egress rules both allow it"). Only an explicit deny_subnets entry still refuses a sibling.
Design ruling (ARCH-EXPERT, revising the earlier PASS): the zone-answer pin lift is a FAIL; the landed NET-070 proof is the correct oracle. The design's pin machinery has one entrance, §5.3 l145 (names matched by egress_allow_dns); zone names never take it (l152, §7.1 l249: exempt from allow-list matching because local names need no entry). A name the allow-list does not match creates no admission window, so at connect the source half is decided by egress_allow_subnets/egress_deny_subnets alone (l249: "source egress per UC6's local-reach semantics"; l248 is the same shape for box→host). Lifting an UndeclaredSubnet drop because the sibling's name resolved is a fourth admission path the design does not have, and it defeats default-deny for every sibling on the host (every box resolves *.min.internal by NET-072).
How a box declares sibling reach: an egress_allow_subnets entry covering the sibling's plane address (the plane 100.64.0.0/10 or the node's block; leases are routing, not identity, §4.2 l66), refined by egress_deny_subnets; the target's default-deny ingress gives per-target precision. An egress_allow_dns entry naming a sibling is a no-op. A name-scoped sibling grant would be an architecture change (file against gominimal/arch citing §7.1 l249 and §5.3 l145/l152), not something this PR can add.
What stays PASS: the allow-list exemption for zone resolution (NET-072); zone answers admitted only inside the plane as a rebinding rule, provided no pin is created from them; the conjunction on the bare SYN at connect; host and gateway sources ingress-only. Fix scope: refuse_zone_connect (drop the admits_flow lift), the egress.rs carve-out (validate the answer, do not enter it in the pin table), and the unit test. The KVM lane must be green before merge.
|
/revise Round 6 was lost at the push (HTTP 403 on git-receive-pack after the work was complete), so nothing from it reached this branch; redo it against review 5365058842 on head 9ce6a66, whose threads are all still open. The one blocking item: remove the pin lift in |
…d-reach-sibling-boxes-by-name-under-bo
`rebinding_admits`'s doc said the plane carve-out is "the reason a box
reaches a sibling by name with no `allow_dns_hosts` entry" — which is
the reading the connect-time gate was built on and the review rejected:
the intersection only splits the answer set, and reach is the caller's
to decide. State that split in the contract itself, and fix the test
comment that said the same ("a zone name pins nothing but a sibling's
lease") to the shape the daemon now honours.
The box zone's carve-out is the resolution's alone. A zone answer is still validated by the rebinding intersection — each refusal is logged like any other — but it never enters the pin table: the design's admission windows come from `egress.allow_dns_hosts` matches alone (§5.3), and a zone answer that became a pin was a name-scoped grant of a sibling's lease. `refuse_zone_connect` drops its `admits_flow` lift with it, so the source half of a sibling connect is the source's `allow_subnets` / `deny_subnets` as declared and nothing beside them — the one decision the source's own egress leg and the hostname proxy's caller check both make of the same connection. That is the pair the connect proof now makes: a caller whose `allow_subnets` names the target's lease reaches it — its own leg forwards the SYN and the target's relay admits both halves — while a caller with no CIDR grant is refused even after resolving the zone name, at the target's relay on the SYN and by its own leg on the way out. The resolution proof asserts the negative the pin table owes: `admits_flow` on the answer's lease is false, where a declared name's answer keeps its window. The denied caller's direct connect is the NET-070 e2e pair's dropped SYN, so the KVM lane's red assertion (curl 28) now has a daemon that refuses it.
|
Round 7 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A box still resolves a sibling's zone name with no allowlist entry, but the answer pins nothing: a connection to the sibling now succeeds only when the source's own allow_subnets/deny_subnets admit it beside the target's ingress rules, so the denied caller's direct connect is a dropped SYN — the KVM lane's curl 28 — while the connect-time debug line still names both boxes and each side's verdict. Notes from the agent: The KVM lane cannot run here (no /dev/kvm, no built min/minvmd), so the NET-070 pair-5 fix is deferred to that lane (ci-linux-kvm / test-kvm): it follows from the daemon change — the pair's caller has --allow-subnets 100.64.255.253/32 and no allow_dns_hosts, so its zone resolution now creates no pin and its own egress leg drops the SYN to the target's lease (curl 28), while the proxied leg keeps the proxy's CIDR-only 403. Both halves are asserted at unit level in the two rewritten tests. Other commands run, all exit 0: cargo nextest run -p minimald --locked --no-tests=fail (496 passed, 8 skipped as env-gated; nextest flags one test LEAK — nsenter::tests::resolves_the_grandchild_not_the_forking_process, a module this round does not touch), cargo clippy -p sessions -p minimald --all-targets --locked -- -D warnings, scripts/clippy-strict.sh origin/main (clean, no hits to report). Design ruling implemented as directed, stated here for the re-read: a zone answer is validated by the rebinding intersection and never enters the pin table even when the box also declares the name in allow_dns_hosts, because reach to a sibling is CIDR-only on every surface (the source's own leg, the target's connect-time gate, the hostname proxy's caller check), so a pin for a sibling lease could only admit a frame another gate then drops. dns.rs and policy.rs needed no change this round; no file outside the task's layers was touched. |
The connect-time source refusal of refuse_zone_connect warned through the target relay's per-box PolicyWarnLimiter under the source's label, so it was not rate-limited against the source's own egress-leg warns for the same (box, rule): one refusal could say two lines in a minute, and the method doc's once-per-source-box-and-rule claim did not hold. Emit through the source's own limiter instead — the same one its egress leg rate-limits by — so one refusal is one R2.7 line whichever leg saw the frame, and the doc's claim is true. The connect-time half itself stays: it is the conjunction's backstop at the target, and its debug line is the one place both boxes' verdicts are named.
|
Round 8 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
At this branch's head a box resolves its sibling's zone name with no Notes from the agent: Round 8. Thread 4 was the round's work: the head (06fc697) had never been built or tested, so I built it cold and ran every test line — all three proofs passed at that head unmodified, and pass again at 94f9689; cargo fmt --check on minimald, cargo clippy -p minimald --all-targets (no warnings) and ./scripts/clippy-strict.sh (scope -p minimald -p sessions, clean) also ran, so the one gate the finding names is green at the new head. Threads 1–3 were already addressed at 06fc697; I verified each against the code (source_pass is exactly direct_connection_verdict == Admit with no pin lift; the proof is the two requested cases; a zone answer is validated, never pinned, and the negative is asserted beside the declared-name contrast) and changed nothing further for them. Thread 5's log-contract half held as stated — the connect-time source refusal warned through the target's per-box limiter, so it was not rate-limited against the source's own egress-leg warns and the method doc's once-per-source-box-and-rule claim did not hold across the two emits. Fixed in 94f9689 by emitting through the source's own limiter (the same one its egress leg rate-limits by), asserted in the proof: the leg's refusal of the same frame adds no second line. The connect-time half itself stays,…[truncated] |
There was a problem hiding this comment.
Round 8 at 94f9689 reviewed: the connect-time refusal now warns through the source's own limiter so the two legs dedupe to one line (R2.7); no verdict change. Round 7 fixed the blocking item at the root (zone answers validated, never pinned; source half is the declared rules alone), ARCH-EXPERT PASS on NET-072/NET-073 (§7.1 l249, §5.3 l145, UC6), KVM green on 06fc697 with the NET-070 pair-5 oracle, every thread resolved. Merge follows the checks on this head.
T31 — Resolve and reach sibling boxes by name under both boxes' rules
slice: S7
kind: task
covers: NET-072, NET-073
size: M
est: 200 code, 180 tests
executor: agent
difficulty: needs care
model: standard
diagnostics: the bundle's daemon log tail carries each box-to-box refusal with both boxes and the rule
observability: one debug log line per box-zone connection with the source box, the target box and each side's verdict
layers:
- core:
- crates/sessions/src/core/egress.rs: zone names need no allow entry and zone answers are carved out of the infrastructure deny set
test: cargo nextest run -p sessions box_zone_answers_carved_out_of_infrastructure_deny
- daemon:
- crates/minimald/src/net/dns_gate.rs: skips the allow-list check for the zone
- crates/minimald/src/net/dns.rs: exposes the zone suffix to the gate
- crates/minimald/src/net/switch.rs: checks the source's egress at connect beside the target's ingress gate
- crates/minimald/src/net/policy.rs: registers sibling names in the zone
test: cargo nextest run -p minimald box_zone_resolution_needs_no_allow_entry
test: cargo nextest run -p minimald box_zone_connection_enforced_at_connect
produces: none
consumes:
- crates/minimald/src/net/dns_gate.rs
proof: A box resolves a sibling's name with no allowlist entry, and a connection to it succeeds only when the target's ingress rules and the source's egress rules both allow it.
depends on:
- blocked by #1638
Out of time
The coder ran out of its 7200s before it finished. If it left work uncommitted, its last commit is the runtime's snapshot of that work as it stood — the commit message says so — and not a finished step: it may not build or pass its tests. So this PR is a draft.
Proof
A box resolves a sibling's name with no allowlist entry, and a connection to it succeeds only when the target's ingress rules and the source's egress rules both allow it.
Commit headers reworded by the runtime to fit commitlint. The header the coder wrote is the first paragraph of each of these commits' bodies:
feat(minimald): the coder's uncommitted work as it stood when its 7200s ran outTests
cargo nextest run -p sessions box_zone_answers_carved_out_of_infrastructure_denycargo nextest run -p minimald box_zone_resolution_needs_no_allow_entrycargo nextest run -p minimald box_zone_connection_enforced_at_connectVerify
min task run agent-verifyexited 101, so this PR is a draft.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/minimald/src/net/dns.rsCloses #1647