Repository navigation
T30 — Pin allowed names to the addresses they resolved to, refuse denied ranges, and answer AAAA, HTTPS and SVCB empty - #1730
Conversation
NET-067's core: the pure decision of which addresses a name resolved to may ever be admitted for a box, subtracting the box's own deny_subnets and the infrastructure deny set (design §5.3) — link-local and the metadata services in it, loopback space, the 100.64.0.0/10 plane, the gateway's own two addresses (the answerer's and the helper's), and RFC 1918 unless the box's allow_subnets covers the answer. Kept beside the frame verdict in `core::egress` as a pure function over owned addresses and CIDRs, separate from resolver I/O, so the new `kani_rebinding_intersection_admits_no_denied_address` harness can exhaust it at an unwind bound of 4: every comparison is u32 mask arithmetic (no [u8; 4] memcmp loops), with each CIDR set carried as None, empty, or two symbolic rules — at most 4 per set. The set-shaped wrapper (`rebinding_intersection`) splits one name's answers into the admitted addresses and the refusals to log; `kani.sh` now expects the eighth sessions harness.
NET-066, NET-067 and NET-136 enforced where every one of a box's frames already passes: the session relay. A new `net::dns_gate::DnsGate`, built per box into the `SessionGate` at attach and shared by both relay legs, holds the admission table and the three decisions that read it: - Pinning: a DNS reply from the switch's own resolver answering a query for a name the box's `egress.allow_dns_hosts` declared is split by the pure rebinding intersection (the sessions core landed beside this), and each surviving answer is admitted for a five-minute window. On the egress leg an admitted address is the one thing that lifts an undeclared-destination drop — denied ranges and protocol rules keep governing, so a pin cannot smuggle a refused range through. - Refusal: an answer landing in the box's `deny_subnets` or the infrastructure deny set never enters the table, and each says so through the session's rate limiter with the name and the answer (`warn_dns_refusal`, one line per box per rule per minute). - NODATA: AAAA, HTTPS (65) and SVCB (64) queries toward the switch's resolver are answered empty by the relay itself, under the query's own id, and never written on to the switch. The reply itself always passes through to the box; resolution is honest, it is the connection to a refused address that is not admitted. Synthesizing the reply frame needs honest length bookkeeping at the relay, so the switch gains `udp_datagram` (bounds-checked UDP payload extraction), `udp_reply_frame`/`ipv4_checksum` (a reply the box's kernel accepts), and `write_tap_frame` (the ingress leg's write loop, now shared with the NODATA answers). The relay harness items in the switch tests become `pub(crate)` so the gate's tests drive the same legs, and the own-IP attach doc names the DNS dimension it carries.
…d-names-to-the-addresses-they-resolved
|
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 |
|
Reviewed: 1 finding, none blocking at Address the comments on the diff. Clobber: none: |
The ingress leg parsed every inbound frame as a UDP datagram before the gate could say whether the frame was one of its own, and the egress leg parsed every frame twice — once for the conntrack window and once for the NODATA interception. Both now cost nothing on a frame that is not IPv4+UDP, which is most of a relay's traffic: the ingress leg reads the EtherType and the IPv4 protocol byte before it parses anything, and the egress leg shares one parse between the conntrack and the DNS gate, with the datagram's length arithmetic split out so the payload needs no second pass. The pre-check is a narrowing, never a reclassification — every frame it rejects is one udp_datagram could not have read — and that is what the new test asserts.
|
Round 1 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
A box that allows github.com reaches exactly the addresses github.com resolved to for the admission window and nothing else, an allowed name that resolves into a denied range is refused with the name and the answer in the rate-limited log line, and AAAA, HTTPS and SVCB lookups come back NODATA from the relay — all four proofs still pass at this branch after this round's change, which now spends the DNS gate's frame parse only on IPv4+UDP frames instead of on every frame the relay carries. Notes from the agent: Revise round 1 of PR #1730: the directive carried one review finding (LOW perf, switch.rs) and one thread, and this round addresses only that. The fix is behavior-preserving and confined to switch.rs, a named layer file: the ingress leg (relay_switch_to_tap) now reads the EtherType and the IPv4 protocol byte (is_ipv4_udp) before parsing, so a peer's TCP/ARP/IPv6 frames cost three comparisons instead of a full udp_datagram parse; the egress leg (relay_tap_to_switch) now parses once and shares the result between the conntrack window and the NODATA interception, with the datagram's length arithmetic split out of udp_datagram into udp_payload so the payload needs no second pass. A new test, udp_precheck_narrows_without_losing_datagrams, asserts the pre-check only ever narrows (every frame it rejects is one udp_datagram could not have read). No other file needed a change; nothing was touched outside the layers. Deferred (lane: kani): cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address was not run on this box — the harness exists (crates/sessions/src/core/egress.rs, one of the 8 sessions harnesses scripts/kani.sh expects) from the earlier round, and this round did not touch it, so the lane still owes its evidence run. |
|
/revise Babysitter review against T30's plan block (covers NET-066, NET-067, NET-136; four test lines exit 0, gate exit 0, K 8000 ani lane green). The design's window (deployment-and-egress-gateway §5.3) is what NET-066 points at, and the gate departs from it in three places. Fix 1; decide 2 and 3 and say so in the module doc; the rest are notes.
Verified: both relay legs are hooked, "nothing else" is enforced at the relay (drop unless admitted), one table per |
Round 2 of the review on the DNS gate. The blocking finding first: a pin expired under a live connection. The relay's egress leg asked admits_destination per frame, which checks the window and nothing else, so a git clone or a keep-alive to an allowed name longer than five minutes stalled silently once the pin aged out. The gate now carries a flow table beside the admission table: the first frame a pin admits establishes its flow (protocol, both ports, destination), and an established flow keeps its admitted destination past window expiry until a FIN or RST ends it — design §5.3's conntrack-aware retention — while a new connection to the same address after the window is refused until the box re-resolves. The egress leg asks the new admits_flow with the L4 packet it already parsed on the pin's path. The window itself stays fixed at 300 s, now stated in the module doc as a deliberate deviation from §5.3's TTL-bounded window rather than an unexplained one: a TTL-bounded window hands the duration of the box's grant to a value its policy does not control and a rebinding-controlled zone can set to the cap, and §5.3's floor alone would double the reach every answer holds here. What the floor covers is covered instead by retention for established flows and by re-resolution for new ones — the box's libc holds no DNS cache, so every getaddrinfo rides the relay again. The admission table is also no longer unbounded: §5.3 caps admitted addresses at 32 per name per family, and the gate enforces it, refusing answers past the cap with a debug line naming the name and address. The size-triggered sweep stays as the per-box backstop. The review's notes are named in the module doc now: the forward NODATA of NET-136 carries no SOA deliberately (the gate is authoritative for no forward zone, and the box's stack holds no negative cache to warm — the box-zone answerer's SOA is NET-124's and serves a different resolver), reply matching reads the first question for the name and nothing else (the relay's source check is the whole defence, the pre-NET-084 hairpin inherited), and DNS over TCP is not carried, so a TC=1 retry fails — a resolution failure recorded, not a rebinding vector. The refused-range test also says which half proves the intersection at the relay and which half the frame verdict's own denied-subnet rule decides. Tests: established_flow_keeps_its_pin_past_the_window drives a relay whose window is shrunk to a second — the flow's frames pass after expiry, a new flow to the same address is refused, the flow's end releases the address, and a re-resolution re-admits it — and admitted_addresses_are_capped_per_name proves the cap refuses the 33rd address of a name while a second name still admits beside it.
The rate limiter behind warn_dns_refusal keyed on (session, rule) alone, so a box refused on two names inside the minute heard about the first only — the spec's sub-requirement logs the name and the answer per refusal, and the log test replayed one reply twice and never a second name. The key now carries the refused name beside the rule, so each refused name spends its own once-per-minute line while every other warning keeps its old budget. The test asserts it: a second refused name inside the interval is heard, and the line says which name and answer it is.
The rebinding harness bounds each deny set at two CIDRs where the tier text allows four, and the doc let the text be read as the proof's. The bullet now says the bound honestly: two per set, pinned for the same reason two_protocols pins two protocols — a third adds no new failure shape while it multiplies CBMC's search — and a set-shaped hole that only opens at three or more rules is outside this proof's bound, which the doc states rather than leaves to be inferred.
|
Round 2 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A box whose egress declares a name now keeps what it resolved for as long as it is using it: an established flow to a pinned address still passes the relay after the admission window expires (until FIN/RST ends it), a new connection to that same address is refused until the box re-resolves, the admission table is capped at 32 addresses per name per family, a second refused name inside the rate-limit minute is logged with its own name and answer, and the gate's module doc states the fixed 300s window as a deliberate deviation from design §5.3 (with reasons) plus every loose end the review named (no SOA on the forward NODATA, loose reply matching, DNS over TCP not carried). Notes from the agent: Deferred (lane: kani, not runnable on this box): cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address — the harness name is real (crates/sessions/src/core/egress.rs:1324) and the round's only change to that file is prose inside its cfg(kani)-gated doc comment, so it cannot be compile-verified here; the kani lane still owes that run. Review findings: #1 fixed (flow table + admits_flow on the egress leg, with the relay-level test asked for; the window is shrunk to 1s through a #[cfg(test)] hook threaded spawn_test_relay_with -> SessionGate::shrink_admission_window -> DnsGate::shrink_window because the relay uses real Instant::now()). #2 decided, not changed: the window stays fixed at 300s and the module doc now states it as a deliberate deviation from §5.3's TTL-bounded window (the TTL hands the grant's duration to a value the box's policy does not control; the 600s floor alone would double the reach; the floor's job is covered by retention for established flows and by re-resolution for new ones). #3 fixed: MAX_ADDRESSES_PER_NAME = 32 per name per family, over-cap answers refused with a debug line, the size sweep kept as the per-box backstop. #4 and #5 (loose reply matching; DNS over TCP not carried) named in the module doc's 'Known loo…[truncated] |
|
/revise Round 2 covers the three points: retention past the window, a documented deviation on the fixed window with a rebinding rationale, and the per-name cap. Two minimal-review threads remain open on 897e330 and the second is a real gap:
Resolve both threads when addressed. |
…d-names-to-the-addresses-they-resolved
The retention's staleness bound was documented as FLOW_IDLE_CAP but enforced only by the sweep that runs once the flow table crosses 4096 entries, and that sweep is the only place the cap was read. Below that size — every ordinary box — an established flow kept its pinned destination for the whole box uptime, and a UDP flow could never be released at all: parse_ipv4_l4 zeroes the flags byte for every transport that is not TCP, so a FIN or RST is a close signal a UDP flow cannot carry and the flow's only possible release was idleness. Read the cap at the lookup of every frame that would ride a flow, the way the same file's UdpConntrack::allows_ingress reads its TTL, so an idle flow is reclaimed at the frame that would have ridden it however small the table is. The sweep stays, as the bound's memory half; the docs of both constants now say which half is which, and admits_flow's contract names the lookup as where the release happens. Two proofs, one per transport the finding called untested: a UDP flow ridden past the window is still admitted and the same flow idle past the cap is dropped at the relay, re-resolution opening it again; and an idle TCP flow that never sent a FIN behaves the same. Each also drives the gate directly against its own clock, where a ridden flow holds up to the cap and an idle one is released at its edge. The NODATA thread on the same file is judged and left as documented: the gate is authoritative for no forward zone, and the box-zone SOA it could borrow names a zone that does not cover the qname, so it is not a record the reply can carry.
The review thread on the NODATA reply's empty authority section asked the one question the module doc left implicit: whether the record the box-zone answerer synthesizes for its negatives could be borrowed for parity. State the answer where the omission is documented, with the facts it rests on rather than the conclusion alone — the reply is non-authoritative, hickory's response_from_request clearing the AA bit, and RFC 2308's negative answer carries the SOA of the zone holding the asked name, so the answerer's min.internal SOA on a github.com answer names a zone that does not cover the record. For the one client that reads an authority section, a caching resolver, that is a discarded record at best and a broken reply at worst, so carrying it would trade the honest empty answer that lets getaddrinfo degrade to IPv4 for a protocol violation.
|
Round 3 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A box that allows only github.com reaches the addresses github.com resolved to for the admission window and nothing else, an established flow keeps its pin past the window only while it is ridden — an idle one, UDP included, is released at the idle cap, which the relay now reads at every lookup the way the conntrack reads its TTL — an allowed name that resolves into a denied range is refused with the name and the answer in the log, and AAAA, HTTPS and SVCB lookups come back empty. Notes from the agent: Revise round 3: both open threads judged, one fixed in code, one resolved by the finding's own second remedy. Nothing outside the task's layers was touched this round; the branch's changed set is still the seven files the layers name, and this round adds only the two daemon files above. Inside switch.rs, IPPROTO_TCP was made pub(crate) for the DNS gate's tests, mirroring the existing pub(crate) note on IPPROTO_UDP in the same file. Deferred: |
|
/revise One open minimal-review thread on 29147b0, and it is right: |
|
/revise Re-posting: the round this note opened at 05:11Z never got a container (capacity refusal, job cd808c43) and no job exists for it now, so the task status is stuck on "round 4". Same directive: One open minimal-review thread on 29147b0, and it is right: |
…d-names-to-the-addresses-they-resolved
The egress relay leg recorded a conntrack window for every admitted outbound UDP datagram before the AAAA/HTTPS/SVCB interception ran, so a query the relay answered itself — one that never reached the resolver — still opened a window keyed (resolver, 53, box_src_port). Nothing was sent upstream, so no reply is coming through that window: its only possible consumer was an unsolicited inbound datagram from the resolver's address to the query's source port, which the ingress gate would then pass as solicited for the TTL. Record the window after the interception, so only a datagram this leg actually forwards opens one. The normal A-query path is unchanged and an undeclared datagram still never reaches the record, being dropped earlier in the leg. The NODATA test asserts both halves: an intercepted query leaves a datagram from the resolver to its own source port unsolicited — dropped, with only the sentinel behind it reaching the box — and the forwarded A query's reply still comes back.
|
Round 4 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A box that allows github.com reaches the addresses github.com resolved to for the admission window and nothing else, an allowed name that resolves into a denied range is refused with the name and the answer in the log, and AAAA, HTTPS and SVCB lookups come back empty from the relay — which this round also proves leave no inbound hole: an intercepted lookup opens no UDP conntrack window, so a datagram from the resolver to the query's own source port stays unsolicited and the ingress gate drops it, while the A query the relay does forward still opens the window its reply returns through. Notes from the agent: Revise round 4: one open thread, judged valid and fixed. |
…d-names-to-the-addresses-they-resolved # Conflicts: # crates/minimald/src/net/gvproxy_network.rs # crates/minimald/src/net/switch.rs # crates/sessions/src/core/egress.rs
Main added the diff-scoped strict clippy gate (`just clippy-strict`), and once this branch had merged main in, it reported 26 diagnostics on the lines this branch adds — all inside the DNS gate's three files. Fix the ones whose input is an untrusted frame: `is_ipv4_udp` and `ipv4_checksum` now read their fields the way `udp_payload` does, and `udp_reply_frame` states the parsed-datagram invariant its MAC slices were silently relying on. The two relay loops keep their `..n` slices and name the invariant that bounds them with `#[expect(clippy::indexing_slicing, reason = "...")]`: `n` is the count the loop's own read returned for that buffer. The test sites follow: the four `is_ok()` assertions unwrap, the eight forwarded-query reads now check the `io::Result` they were discarding — the inner read had been unchecked, so a failed read passed for a forwarded query — and one `as u8` disappears by making the range `u8`. `just clippy-strict`: clean.
|
Round 5 of 10 on a conflict with the base branch, pushed as Resolved conflicts in:
Verify On this branch a box whose egress policy allows github.com reaches exactly the addresses that name resolved to for the admission window (a flow the pin established keeps its destination past the window until it goes idle, and nothing else — every other destination is still dropped); an allowed name that resolves into a denied range has that answer refused at resolution time and the refusal is logged rate-limited with the name and the answer; and the box's own AAAA, HTTPS and SVCB lookups toward the switch's resolver come back NODATA without ever reaching the switch. All three still hold with main's lease check (NET-084) now in the same relay legs. Notes from the agent: Round 5 was a conflict round: the three paths in conflicts.txt were resolved and the merge completed as 9465c79 before anything else. The resolution combines this branch's DNS gate with main's new lease check (NET-084, T40): the egress leg rejects a foreign source before the verdict, the DNS pin stays the one drop the rejection-then-verdict path lifts, and both parents' doc comments were merged rather than one picked. The merge forced four adaptations, all inside the layers: main's arp_frame now takes the ARP sender address (its lease check reads it), so dns_gate.rs's eight sentinel calls pass LEASE; EgressRules::from_policy grew a lease argument, so the dns_gate test helper and the egress accessor test pass one; main's spawn_relay_for gained the configure hook the DNS-gate proofs shrink their window through; and main's lease() accessor was kept beside this branch's allow_subnets()/deny_subnets(). Second commit, out of the merge but in the layers: main also added the diff-scoped strict clippy gate (just clippy-strict, part of just ci), and once main was merged in it reported 26 diagnostics on this branch's own lines — fixed by bounds-checking is_ipv4_udp/ipv4_checksum/udp_reply_frame the way their sibling udp_payload already does, naming the relay loops' read-count invariant with #[expec…[truncated] |
warn_dns_refusal keys the rate limit by rule and name while the frame drops key on the rule alone, so the two paths hold separate buckets inside the one limiter they share. The module doc and the limiter field doc both claimed the budget was shared; they now say the bucket is deliberately separate and why, matching what policy.rs documents.
| let mut held = admitted | ||
| .values() | ||
| .filter(|admission| &*admission.name == name) | ||
| .count(); | ||
| let mut admitted_now = Vec::new(); | ||
| let mut over_cap = Vec::new(); | ||
| for address in addresses { | ||
| if let Some(existing) = admitted.get_mut(address) { | ||
| // The name answered again: refresh the window it holds for, | ||
| // under whichever owner first admitted the address. | ||
| existing.expires = expires; | ||
| admitted_now.push(*address); | ||
| continue; | ||
| } | ||
| if held >= MAX_ADDRESSES_PER_NAME { | ||
| over_cap.push(Ipv4Addr::from(*address)); | ||
| continue; | ||
| } | ||
| held += 1; | ||
| admitted.insert( | ||
| *address, | ||
| Admission { | ||
| name: Arc::from(name), | ||
| expires, | ||
| }, | ||
| ); | ||
| admitted_now.push(*address); | ||
| } | ||
| if admitted.len() > ADMISSION_SWEEP_AT { | ||
| admitted.retain(|_, admission| now < admission.expires); |
There was a problem hiding this comment.
MEDIUM · correctness · confidence 0.62 · in DnsGate::admit
The per-name admission cap is never released for a box whose table stays under ADMISSION_SWEEP_AT (4096), so the cap fills up with stale, expired admissions and a name whose resolved address set changes becomes permanently unreachable. held (line 499-502) counts every admitted entry owned by the name with no expires filter, and the only prune of the admitted table is admitted.retain inside if admitted.len() > ADMISSION_SWEEP_AT (lines 527-528). For a typical box with one or two allowed names the table never crosses 4096, so expired admissions are never swept; once a name has resolved to MAX_ADDRESSES_PER_NAME (32) distinct addresses across its lifetime, every later resolution to a different disjoint set is refused as over-cap (the held >= MAX_ADDRESSES_PER_NAME branch at 513), even though the old addresses' windows have long expired. The module doc says the cap bounds addresses 'at once', which this does not: a stale entry admits nothing but still consumes the cap, so an allowed name that rotates its address set (a CDN, a host that moves providers) becomes reachable only while its first 32 ever-resolved addresses happen to be re-answered. Re-resolution to the same addresses is unaffected (the get_mut refresh path). The fix is to count only unexpired entries in held (or prune the name's expired entries as part of admit), independent of the 4096 sweep threshold.
What the reviewer checked
dns_gate.rs:499
let mut held = admitted.values().filter(|admission| &*admission.name == name).count();/ :527if admitted.len() > ADMISSION_SWEEP_AT { admitted.retain(|_, admission| now < admission.expires); }— the sweep is the only release, gated at 4096.
Hand this to an agent
Act on a code-review finding.
File: crates/minimald/src/net/dns_gate.rs
Lines: 499-528
Category: correctness
Severity: medium (reviewer confidence 0.62)
Finding:
The per-name admission cap is never released for a box whose table stays under `ADMISSION_SWEEP_AT` (4096), so the cap fills up with stale, expired admissions and a name whose resolved address set changes becomes permanently unreachable. `held` (line 499-502) counts every `admitted` entry owned by the name with no `expires` filter, and the only prune of the `admitted` table is `admitted.retain` inside `if admitted.len() > ADMISSION_SWEEP_AT` (lines 527-528). For a typical box with one or two allowed names the table never crosses 4096, so expired admissions are never swept; once a name has resolved to `MAX_ADDRESSES_PER_NAME` (32) distinct addresses across its lifetime, every later resolution to a *different* disjoint set is refused as over-cap (the `held >= MAX_ADDRESSES_PER_NAME` branch at 513), even though the old addresses' windows have long expired. The module doc says the cap bounds addresses 'at once', which this does not: a stale entry admits nothing but still consumes the cap, so an allowed name that rotates its address set (a CDN, a host that moves providers) becomes reachable only while its first 32 ever-resolved addresses happen to be re-answered. Re-resolution to the *same* addresses is unaffected (the `get_mut` refresh path). The fix is to count only unexpired entries in `held` (or prune the name's expired entries as part of `admit`), independent of the 4096 sweep threshold.
First verify this against the code yourself. It is model output and
may be wrong. If it is wrong, or the tradeoff was deliberate, say so
and change nothing.
👍 useful · 👎 noise — react to tell the reviewer. Replying works too, and says more.
There was a problem hiding this comment.
Addressed in 8c33619c6cf9: Fixed in 8c33619: admit releases a name's expired admissions before counting its cap, so a rotated answer set is admitted instead of refused as over-cap by long-expired entries; the 4096 sweep stays the table-wide bound. New test expired_admissions_release_the_per_name_cap covers the rotation case and fails on the unfixed code.
|
Round 6 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
At this branch head a box that allows github.com reaches the addresses github.com resolved to for its admission window and nothing else, an allowed name that resolves into a denied range is refused with the name and the answer in the log (rate-limited per name per rule per minute, a bucket deliberately separate from the frame drops' per-rule one, as the dns_gate docs now say), and AAAA, HTTPS and SVCB lookups come back empty. Notes from the agent: Revise round 6, one review finding, no behaviour change: the module doc and the limiter field doc in dns_gate.rs claimed the DNS refusal shares the frame drops' rate-limit budget; they now say the limiter instance and log are shared while the bucket is deliberately keyed by name as well as rule, which is what policy.rs already documents. Also verified: cargo fmt --check clean, and cargo doc --no-deps -p minimald resolves both new PolicyWarnLimiter::warn_dns_refusal links with no dns_gate warnings (the crate's pre-existing doc warnings are untouched). Deferred (lane: kani, not runnable on this box): cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address — the harness exists (crates/sessions/src/core/egress.rs) and scripts/kani.sh already expects sessions 8 for it from an earlier round; run nothing here. |
|
/revise Round 6 fixed the doc claim (that thread is addressed; resolve it). The MEDIUM thread on
CI is green on |
…d-names-to-the-addresses-they-resolved # Conflicts: # crates/minimald/src/net/switch.rs
…d-names-to-the-addresses-they-resolved
|
Round 7 of 10 on a conflict with the base branch, pushed as Resolved conflicts in:
Verify A box that allows github.com reaches the addresses github.com resolved to for the admission window and nothing else; an allowed name that resolves into a denied range is refused with the name and the answer in a rate-limited warn line; and AAAA, HTTPS and SVCB lookups the box sends to its resolver come back empty (NODATA) from the relay — all of it intact at the branch head after main's proxy-parity refactor was merged in, with the four named tests green. Notes from the agent: Round 7 was a conflict round: the directive carried only the merge instruction, no review threads. The conflict was in SessionGate::for_session — this branch had inlined the egress compilation, the infrastructure deny set and the DNS-gate construction there, while main's T34 (#1737) had refactored the same function to call two new helpers, declared_ingress_ports and compiled_egress. Resolved by keeping main's helper-based shape for the ingress halves and the egress field, and building the DNS gate on top: the gate now takes its rules from compiled_egress — the same one compilation the relay's frame verdict and the hostname proxy's caller check read — so a name's admission and a frame's verdict cannot disagree about what the box declared. No behaviour change; the four named tests and the whole minimald suite (475) pass. Files the runner may see in the merge commit beyond that one are main's own (dns.rs, proxy.rs, server.rs, session.rs) — they came in with the merge and are not this task's work. Deferred, not run: cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address (lane: kani) — this box has no Kani; the harness is in place at crates/sessions/src/core/egress.rs (#[kani::proof], unwind 4, per-address oracle plus a two-answer set wrapper over the allow, deny and both halves of the infrastructure set) and scripts/kani.sh's sessions expectation is already 8 to count it. |
|
/revise Round 7 was the conflict merge, so the MEDIUM thread on
CI is green on |
…d-names-to-the-addresses-they-resolved
DnsGate::admit counted every entry the name owned, expired or not, toward MAX_ADDRESSES_PER_NAME, and the only prune was the table-wide sweep behind ADMISSION_SWEEP_AT (4096). A box with one or two allowed names never crosses that threshold, so once a name had resolved to 32 distinct addresses across its lifetime every later disjoint answer was refused as over-cap although the old windows had long expired: a stale admission admitted nothing but still spent the cap, and a name whose address set rotates (a CDN, a host that moves providers) became reachable only while its first 32 ever-resolved addresses happened to be re-answered. admit now releases the name's expired entries before counting, so the cap bounds what a name holds at once, as its module doc claims. The 4096 sweep stays the table's bound, and now only reclaims the entries of names that stopped resolving.
|
Round 8 of 10 on a /revise note, pushed as
Verify Review threads the coder judged:
A box that allows github.com reaches the addresses github.com resolved to for the admission window and nothing else — now including a name whose resolved address set rotates after the window, whose fresh answers are admitted instead of refused as over-cap — an allowed name that resolves into a denied range is refused with the name and the answer in the log, and AAAA, HTTPS and SVCB lookups come back empty. Notes from the agent: Revise round 8 of 10, one thread open, and it held verbatim at the branch head: the head has moved past the directive's stated 1503f11 to 009c63c (a merge of origin/main), and DnsGate::admit still counted every entry the name owned, expired or not, with the 4096 sweep 10BC8 as the only prune. Fixed in 8c33619. I took the directive's second shape — admit now releases the name's expired entries before counting, rather than only filtering the count — because it also keeps the 'at most MAX_ADDRESSES_PER_NAME at once' bound exact (a filtered count would let one reply that both refreshed expired entries and added new ones overshoot the cap) and keeps the table proportionate to the box's declared names, which is what the constant's doc already claimed. ADMISSION_SWEEP_AT is unchanged and remains the table-wide bound; the two constants' docs and admit's doc were reworded to match. Mutation-checked the new test: with the retain line removed it fails on 'an expired admission spends no cap, so the rotated set is admitted', so it is load-bearing, not a tautology. Nothing outside the task's layers was touched. Not run on this box: the deferred kani line 'cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address' (lane: kani) — the harness from round 1 is still at crates/sessions/src/core/egress.rs:1624 and this round changed no code it covers; and the full-crate suite beyond the module scopes named above, which is why the runner's own re-run of the four test lines is the record for those. |
`just fix` is the innermost loop, and the gate failed there. Three agent rounds on the NET walk then rewrote lines their task never named to clear it (#1737 round 3, #1730 round 5, #1727 round 4), two of them in conflict rounds whose only directive was the merge. A command that fails in the edit loop outranks a sentence in AGENTS.md telling you to leave the hit alone, so the sentence this branch added needs the recipe to agree with it. CLIPPY_STRICT_REPORT_ONLY=1 prints the diagnostics and exits 0. `fix` sets it; `clippy-strict` and `ci` do not, so "before opening a PR" stays the round that owns the judgement. Only hits are demoted — a build or tooling failure still exits non-zero, which is what the cargo check above the filter is for.
…l ref The base was `git merge-base main HEAD`, and a branch that merges `origin/main` leaves the local ref where it was — agent sandboxes and worktrees never check main out at all. The merge-base against a ref that stale predates the main commits the branch merged in, so every line of those commits reads as a line this branch changed, and the gate reports diagnostics on other people's code under a heading saying they are yours. Three agent rounds fixing lines their task never named is what that looks like from the outside (#1737, #1730, #1727). Measured on this branch: a local `main` ten commits behind turned a change touching no Rust at all into 14 changed Rust files across `minimald`, `sessions` and `switch`. With `origin/main` it is nought, and the gate says "no Rust changes" as it should. The remote ref is the safe one by construction: it cannot be behind anything the branch merged, because merging it required fetching it, and a fetch only moves it forward. Stale means the base is older than the newest main, never older than this branch's first commit. The local ref stays as the fallback for a clone without a remote.
…d take it out of just fix (#1749) * docs(agents): say the strict clippy gate is local and bounded by the directive Three agent rounds since #1724 landed rewrote lines beyond their task to satisfy `just clippy-strict`, two of them in conflict rounds whose only directive was the merge, and two coders wrote that the PR lanes would have gone red otherwise. They would not: the gate is local, no CI lane runs it. Say so where AGENTS.md names the gate, and say what a revise or conflict round does with its hits: report them in `notes`, not fix them. * chore(lint): report the strict gate in just fix, enforce it in just ci `just fix` is the innermost loop, and the gate failed there. Three agent rounds on the NET walk then rewrote lines their task never named to clear it (#1737 round 3, #1730 round 5, #1727 round 4), two of them in conflict rounds whose only directive was the merge. A command that fails in the edit loop outranks a sentence in AGENTS.md telling you to leave the hit alone, so the sentence this branch added needs the recipe to agree with it. CLIPPY_STRICT_REPORT_ONLY=1 prints the diagnostics and exits 0. `fix` sets it; `clippy-strict` and `ci` do not, so "before opening a PR" stays the round that owns the judgement. Only hits are demoted — a build or tooling failure still exits non-zero, which is what the cargo check above the filter is for. * fix(lint): demote only the filter's hits, and never inherit report-only Two false-success paths in the report-only mode added a commit ago, both of them the thing this gate exists to avoid: exiting 0 without having checked. The filter's exit was read as "hits" whatever it was, so no python3 on PATH or a crash inside it made `just fix` pass having reported nothing. It now exits a distinct 2 for hits and only that is demoted; 1 from an unhandled exception, 127 from a missing interpreter, and the cargo failure above the filter all still leave non-zero. CLIPPY_STRICT_REPORT_ONLY was read from the ambient environment, so one export in a shell profile would have turned the gate off in `just clippy-strict` and therefore in `just ci`, silently. The enforcing recipe clears it. * fix(lint): take the strict gate's base from origin/main, not the local ref The base was `git merge-base main HEAD`, and a branch that merges `origin/main` leaves the local ref where it was — agent sandboxes and worktrees never check main out at all. The merge-base against a ref that stale predates the main commits the branch merged in, so every line of those commits reads as a line this branch changed, and the gate reports diagnostics on other people's code under a heading saying they are yours. Three agent rounds fixing lines their task never named is what that looks like from the outside (#1737, #1730, #1727). Measured on this branch: a local `main` ten commits behind turned a change touching no Rust at all into 14 changed Rust files across `minimald`, `sessions` and `switch`. With `origin/main` it is nought, and the gate says "no Rust changes" as it should. The remote ref is the safe one by construction: it cannot be behind anything the branch merged, because merging it required fetching it, and a fetch only moves it forward. Stale means the base is older than the newest main, never older than this branch's first commit. The local ref stays as the fallback for a clone without a remote. * fix(lint): report-only never fails, whatever stopped the gate `just fix` is the autofix loop: safe to run any number of times and never stopping on the strict gate. Report-only demoted hits but still exited 101 on a build failure and 127 with no python3, so the loop failed on the gate it was told only to report. Under report-only every failure is now printed with its exit code and demoted; enforcing (`just ci`) keeps every one fatal, so a gate that did not run still cannot pass there. Driven through cargo and python3 shims: hit 2/0, cargo 101/0, no python3 127/0 (enforcing/report-only), and report-only twice gives the same output. * chore(lint): take the strict gate out of just fix `just fix` is the edit loop, and everything it prints is something to fix, so a strict hit printed beside fmt and clippy --fix reads as work whatever a doc sentence says. Report-only kept the hits in that loop and only removed the failure. Remove the gate from the recipe instead: it runs in `just clippy-strict` and `just ci`, the round that owns the judgement, and nowhere else. With no caller, the report-only mode and the recipe that cleared it go too; the script's exit codes are 0 clean, 2 hits, anything else a failure to run, none read as clean. AGENTS.md's tight-loop bullet says the loop prints only what to fix.
T30 — Pin allowed names to the addresses they resolved to, refuse denied ranges, and answer AAAA, HTTPS and SVCB empty
slice: S7
kind: task
covers: NET-066, NET-067, NET-136
size: L
est: 480 code, 300 tests
executor: agent
difficulty: unknown ground
model: strongest
diagnostics: the bundle's daemon log tail carries each admission with the name, the addresses and the window, and each refused answer with the name and the answer
observability: one debug log line per admission; one rate-limited warn line per answer refused as a denied range with the name and the answer
layers:
- core:
- crates/sessions/src/core/egress.rs: the pure rebinding intersection with the infrastructure deny set, with its Kani harness
- scripts/kani.sh: expects one more sessions harness
test (deferred: kani): cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address
- daemon:
- crates/minimald/src/net/dns_gate.rs (new): parses and builds DNS messages at the relay, keeps the per-box admission table with its window, and synthesizes NODATA for AAAA, HTTPS and SVCB
- crates/minimald/src/net/mod.rs: declares the gate module
- crates/minimald/src/net/switch.rs: hooks both relay directions into the gate and shares its admission table
- crates/minimald/src/net/policy.rs: the refusal log goes through the limiter
- crates/minimald/src/net/gvproxy_network.rs: passes allow_dns_hosts and deny_subnets into the attach
test: cargo nextest run -p minimald dns_pinned_admission_window
test: cargo nextest run -p minimald denied_range_resolution_refused
test: cargo nextest run -p minimald denied_range_resolution_logged
test: cargo nextest run -p minimald aaaa_https_and_svcb_queries_are_nodata
produces:
- crates/minimald/src/net/dns_gate.rs
consumes:
- crates/sessions/src/core/egress.rs
proof: A box that allows github.com reaches the addresses github.com resolved to for the admission window and nothing else, an allowed name that resolves into a denied range is refused with the name and the answer in the log, and AAAA, HTTPS and SVCB lookups come back empty.
depends on:
- blocked by #1629
- assumes OQ1 (the spec's interim holds: a native non-deny-all host-address box resolves through the host's resolver, a name rule admits nothing on that host, and the per-box enforcement recorded there covers addresses, never names)
Proof
A box whose policy allows github.com now reaches exactly the addresses github.com resolved to — admitted for a five-minute window at its relay, with every other destination still dropped — an allowed name that resolves into a denied range (the box's deny_subnets or the infrastructure deny set) is refused at resolution time with one rate-limited warn line carrying the name and the answer, and the box's AAAA, HTTPS and SVCB lookups toward its resolver come back NODATA, answered empty by the relay itself.
Notes from the agent: Deferred, never run on this box (no Kani/CBMC inst 8000 alled): the core layer's
test (deferred: kani): cargo nextest run -p sessions kani_rebinding_intersection_admits_no_denied_address. The harness is written (crates/sessions/src/core/egress.rs, kani_proofs, unwind 4) and scripts/kani.sh now expects sessions 8; the ci-kani lane owes the run. Two semantic calls made where the source docs were ambiguous, both documented in dns_gate.rs's module docs: (1) an undeclaredegress.allow_dns_hosts(None) pins NOTHING — only a Some entry can admit — because the schema doc in crates/sessions/src/lib.rs calls None "allow-all hosts", and reading it that way would turn every deny-all-subnets box into a resolve-anything box, lifting a declared deny with an undeclared dimension; if the allow-all reading is ever the intended one it needs its own task, since lib.rs is outside this task's layers. (2) For the RFC 1918 exemption an undeclared allow_subnets (None) counts as covering (is_none_or), consistent with allow-all meaning the address dimension governs; Some([]) covers nothing. gvproxy_network.rs is doc-only: the attach already passed the whole policy into SessionGate::for_session, so allow_dns_hosts/deny_subnets were already riding it — the note names them, no behavior change. The gate watches only replies from the switch gateway (the resolver NET-079's carve-out is keyed to), matches the question name (CNAME chains work; a forged record owner …[truncated]Tests
cargo nextest run -p minimald dns_pinned_admission_windowcargo nextest run -p minimald denied_range_resolution_refusedcargo nextest run -p minimald denied_range_resolution_loggedcargo nextest run -p minimald aaaa_https_and_svcb_queries_are_nodataVerify
min task run agent-verifypassed ([tasks.verify]).Base
The base branch moved while the coder worked; it was merged in before the tests ran.
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 sessions kani_rebinding_intersection_admits_no_denied_addressCloses #1638