Repository navigation
T40 — Reject relay frames whose source is not the box's lease - #1738
Merged
norrietaylor merged 6 commits intoSep 26, 2026
Merged
norrietaylor merged 6 commits into
norrietaylor merged 6 commits into
Conversation
NET-084 lands in the pure verdict: a frame whose source address is not the box's lease is rejected before any family or rule is consulted. The frame summary now carries the source the frame speaks from — an IPv4 frame's header source, or an ARP frame's sender protocol address, so a foreign address cannot be announced by address resolution either — and EgressRules carry the lease beside the resolver, compiled per box at attach when the address is known. An ARP frame too short to carry its sender address has no readable source and is truncated rather than admitted; frames with no readable source at all were already dropped by their family, so None never admits. The check is one function, foreign_source(summary, lease), that the verdict composes first and the relay calls directly on the frames it forwards ungated. The frame-verdict Kani harness now runs symbolically over the source and the lease as well — the property is over every frame and every lease — with the declared half restated as lease && (carve-out || rules), so a verdict that drops the lease check, checks it after the carve-out, or admits on a missing source fails here.
Every egress relay — a box's gated one and the daemon's own — now carries the switch lease it was attached with and rejects any frame whose source is not it (NET-084) before the gate verdict runs: an IPv4 frame's IPv4 source address, an ARP frame's sender protocol address. A rejected frame is dropped without answering and opens no conntrack window, and the rejection says so once per lease per minute, naming the session, the lease and the foreign source.
…ay-frames-whose-source-is-not-the-box
Contributor
|
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 |
Contributor
Author
|
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: |
An ARP frame claiming a protocol type other than IPv4 — or an unexpected hlen or plen — summarized with no readable source, passed the NET-084 lease check on that ground, and was admitted as the declared ARP family: a foreign address could be announced by address resolution by dressing the ARP up as another protocol. The sender protocol address slot is now the frame's source whatever the frame claims to speak, so the slot is lease-checked and a foreign announcement is rejected — and named — the same way as any other, at the gated relay and the daemon's own alike.
…ay-frames-whose-source-is-not-the-box
Contributor
Author
|
Round 1 of 10 on the runtime's review findings, pushed as
Verify Review threads the coder judged:
A frame a box sends with any source other than its own lease never leaves the relay, and the log names the lease and the foreign source — now whatever the frame claims about its own source, an ARP dressed up with a protocol type other than IPv4 included: its sender protocol address slot is lease-checked like a 8000 n IPv4 ARP's, and the rejection line carries the session, the lease and the source it carried. Notes from the agent: Revise round 1: judged the one thread valid and fixed it by strengthening summarize rather than scoping the docs. An ARP claiming a non-IPv4 ptype (or an unexpected hlen/plen) used to summarize as Arp with src None, pass foreign_source on that ground, and be admitted — at the verdict for a gated relay and, unchecked, by the daemon's own gateless relay. The sender protocol address slot is now the frame's source whatever protocol the frame claims for it, so any foreign announcement is rejected as ForeignSource (named: session, lease, source) at the relay level too. That shape was chosen over marking a non-Ethernet/IPv4 ARP Truncated because a Truncated drop carries no source to log and would still have been forwarded by the gateless daemon relay. Deferred test line, not run: cargo nextest run -p sessions kani_frame_verdict_admits_nothing_undeclared (lane: kani); the harness already exists from round 1, pins IPv4 frames, and is untouched by this change — nothing new to write for it. No change needed in gvproxy_network.rs, guest.rs, or tests/netns_root_integration.rs: the lease plumbing and attach signatures are unchanged, the fix is entirely in how the summary reads the source. Also corrected a stale offset in a neighbouring test comment (sender address sits 14 bytes into the ARP payload, not 18). Extra checks run: cargo clippy -p sessions --all-targets and cargo clippy -p minimald --all-targets, both clean; cargo fmt --check clean. |
norrietaylor
approved these changes
Sep 26, 2026
norrietaylor
deleted the
agent/1641-reject-relay-frames-whose-source-is-not-the-box
branch
September 26, 2026 08:19
minimal-foundry Bot
added a commit
that referenced
this pull request
Sep 26, 2026
#1738 threaded the box's lease into `EgressRules::from_policy` and `EgressRules::new`, and the merge that brought it in left this branch's two deny-all proofs calling the two-argument shape, so neither crate's test target compiled. Pass the lease the frames each proof builds carry — the source `ipv4_frame` writes in one, a labelled constant in the other — so the verdicts still turn on the egress dimension alone.
norrietaylor
pushed a commit
that referenced
this pull request
Sep 28, 2026
…he opt-out, and task runs under the same rules (#1727) * feat(sessions): resolve an own-address box's effective egress by phase The deny-all egress default (NET-074..NET-077) needs one place that says what an absent egress section resolves to. Add the build-time rollout phase (this build ships it in force), the EffectiveEgress answer (deny-all, allow-all, or the declaration verbatim), and the resolver that decides between them: deny-all only for an own-address box, once in force, without the daemon opt-out; the shipped allow-all of 03-spec R2.1 everywhere else. A declared section survives every phase untouched. EgressPolicy::deny_all() materializes the deny-all arm as the section whose compiled rules admit nothing, so the gate compiles the default through the same path a declaration takes. * feat(rpc): serve a session's effective policy over its own RPC GetEffectiveSessionPolicy answers the same lookup GetSessionPolicy does, with the egress half resolved to what the gate enforces: deny-all for an own-address box with no egress section once the default is in force (NET-074/NET-075), the shipped allow-all behind the daemon's opt-out (NET-077), or the declaration verbatim. A separate response rather than a field on SessionPolicy, so the strict declaration a client reads back stays exactly what the box was launched with. * feat(minimald): default an own-address box's egress to deny-all The daemon now enforces what the rollout decides: the session launcher passes the box's effective policy to the gate, so an own-address box created with no egress section reaches nothing once the deny-all default is in force (NET-074), while the record keeps the declaration untouched for the strict GetSessionPolicy reply. A --egress-deny-all-opt-out flag (NET-077) threads from the server config through the sessions manager into each session actor, and the task path reads it through a new handle accessor so a task runs under its session's effective egress instead of none. Every session start logs one line naming the rollout phase, the opt-out state, and the effective egress (NET-076's companion diagnostic), so a diagnostics bundle's log tail can explain the box's posture without the daemon's flags. serve_get_effective_ session_policy serves the new rpc-layer response, and the harness gains an opted-out TestServer for the opt-out's tests. * feat(min): print the effective egress default and its announcement * fix(minimald): answer a declared exposure under the deny-all default The deny-all egress NET-074 brings in force drops the box's own replies to connections its ingress gate admitted, so a published port could never complete under the new default: the proxy proof's own-address half timed out at NET-001 (curl exit 28) on the VM lanes. Track admitted inbound flows the way the egress leg already tracks outbound UDP: the ingress leg records the reverse tuple of every packet it admits to a port the box declared, and the egress leg consults that window before a drop stands. A peer that reached a declared port can be answered; the box still cannot initiate anything - the window is keyed to the remote's port on the box's declared one, so a new connection from the box never matches it, and talking at an undeclared port opens nothing. The pure verdict in sessions::core::egress is untouched; the window lives in the relay, like the UDP one. * test(e2e): declare the host alias the own-address proxy box reaches With the deny-all default in force a bare own-address box resolves host.min.internal and reaches nothing, so the proxy proof's NET-003 and NET-004 steps - which are about name routing, not the egress default - must run against a box that declared the address they dial. The box now asks for the switch's host alias the way a box that wants the host would, while its published port keeps needing no egress at all: NET-001 stays the bare-egress assertion it always was. * style(minimald): wrap the reply-window test's timeout chain to width * revert(minimald): drop the relay's inbound reply window Reverts d2e599d and ae0e28e. The window existed so a declared exposure kept answering once the deny-all default bound a bare own-address box; the default ships announced instead (NET-076), and a published port answering under deny-all belongs to the slice that puts the default in force, not to this one. Removing the whole window also removes its flow key, which carried no transport protocol: a window a TCP peer opened on a declared port admitted the box's UDP datagrams to that same peer tuple, traffic that was no reply to any flow. * revert(test): drop the e2e box's host-alias allow-subnets Reverts 377c85c. The declaration existed to keep the proxy proof's NET-003/NET-004 steps reachable once the deny-all default bound the bare box; with the default shipped as announced the bare box reaches the host alias as it does on main, so the case stays the bare-egress assertion it was cut as. * refactor(minimald): thread t 8000 he rollout phase into the resolvers The daemon resolved the egress default through an implicit phase: effective_egress_section and effective_session_policy read nothing but their arguments, so the phase the build ships lived in every caller. Give the resolution seam an explicit sessions::EgressDefaultPhase parameter. Production callers (the session gate, task_network, the GetEffectiveSessionPolicy handler) pass sessions::EGRESS_DEFAULT_PHASE; the unit tests that prove the in-force posture the requirements name pass EgressDefaultPhase::InForce explicitly, and the session starts log-line assertions follow the constant, so a future cutover flips one constant and every reader follows. * feat(sessions): ship the deny-all egress default as announced NET-074/075 name the in-force posture; NET-076 the one before it. The release that turns the default in force is a plan fact, and no plan has named one yet, so ship EGRESS_DEFAULT_PHASE = Announced: an own-address box that declares no egress section keeps the shipped allow-all, min session activate prints the coming change, and the opt-out flag is how a deployment keeps the prior default when the cutover lands. The in-force behaviour stays proven beside it: the unit tests pass the phase explicitly, and policy_shows_deny_all_default renders the in-force resolution through format_policy while the wire reply follows the shipped constant. deny_all_announcement_printed proves the shipped path through the real binary: the notice on a bare own-address activate, nothing on a host-address one, and no notice under InForce. When a release turns the default in force, the constant is the whole cutover - every reader of it (the session gate, the session-start line, min session policy, the activate notice) follows. * fix(minimal): keep the deny-all notice off an opted-out daemon The coming-change notice at activate (NET-076) was decided entirely client-side: the phase is a build-time constant the client shares, so it printed for any own-address activate with no declared egress while the default is announced — with no term for the daemon's opt-out (NET-077), the one rollout fact only the daemon knows. On a daemon started with `--egress-deny-all-opt-out` it still advised starting the daemon with `--egress-deny-all-opt-out`: the exact action that daemon had already taken. Carry the fact on the reply the activation path already holds — `CreateSessionResponse::deny_all_opt_out` — and scope the notice to daemons that have not set the flag. A daemon that predates the field replies with `None`, and a daemon that predates it cannot have the flag, so the client prints exactly as it did. Crates: minimald-rpc carries the field, minimald fills it, minimal reads it. Tests: the daemon test pins both replies over the real wire (`create_reply_reports_the_deny_all_opt_out`), the rpc tests pin the field's wire behaviour against pre-field replies, and the CLI announcement test gains the opted-out half — an activate against an opted-out daemon still succeeds and announces nothing. * test(sessions,minimald): pass the box lease to the deny-all proofs #1738 threaded the box's lease into `EgressRules::from_policy` and `EgressRules::new`, and the merge that brought it in left this branch's two deny-all proofs calling the two-argument shape, so neither crate's test target compiled. Pass the lease the frames each proof builds carry — the source `ipv4_frame` writes in one, a labelled constant in the other — so the verdicts still turn on the egress dimension alone. * fix(minimald): attach a task gate only where its egress has rules A task PTask is a second client beside its session's on the same switch, and the gate built from a policy with no ingress declaration blocks inbound as well as outbound — `allowed` and `udp_allowed` come up empty, so unsolicited TCP and UDP are denied. Passing `Some(SessionPolicy::new(egress, None))` for every own-address task run therefore changed a task's inbound under the announced phase too, where the effective egress is allow-all and nothing else about the box moves: behaviour an announcement is not allowed to change. Resolve the task's effective egress as before, but attach a gate only where it has rules to enforce — the deny-all section the in-force default resolves an absent declaration to, or the box's own declaration. An absent section, what the announced phase and the opt-out both leave in place, passes `None`, exactly as every task did before the deny-all default. `task_network` now takes the rollout phase by name — the pattern `effective_egress_section` already set — so the new `a_task_gate_follows_the_egress_default` can prove both postures: under Announced with no opt-out a bare own-address task run gets no gate, under InForce it gets the deny-all gate. The existing mode test now derives its gate expectation from the shipped phase, so a cutover keeps it honest. * chore(lint): satisfy the strict gate on this branch's new lines The diff-scoped strict gate landed with #1724 and holds the lines a branch changes to a stricter lint set than the workspace's. Ten hits were on lines this branch itself had added, in files the task's layers name. Give the `unwrap`s named `expect`s, and carry `#[expect]` with a reason where the new code keeps its neighbours' idiom on purpose: a discarded oneshot send is the asker already being gone, and a closed oneshot carries no cause beyond the actor being gone. * test(minimald): prove a declared section gates a task in every phase The announcement defers the *default* for a box that declared no egress section; a box that declared one is enforced on its session's own PTask in every phase, so the task path inherits that declaration's gate even while the shipped build is only announcing the change. The gate follows the rule the in-force case already accepts: a task PTask holds no ingress of its own, so its gate default-blocks unsolicited inbound. `a_task_gate_follows_the_egress_default` gains that case: a record carrying a declared section resolves to the declaration verbatim under both phases (not the deny-all section, and not nothing), and the network it gets under the shipped phase carries a policy. * docs(minimald): say the harness runs the deny-all default as announced `new_opted_out_in`'s doc claimed every other harness server runs the default this build ships "in force", but the build ships it as announced (NET-076), so a bare box on any of them still allows all. Say that, and where the in-force posture is proven instead: passed by name to `effective_egress_section`, not asked of a harness server. --------- Co-authored-by: minimal-foundry[bot] <327719912+minimal-foundry[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
T40 — Reject relay frames whose source is not the box's lease
slice: S9
kind: task
covers: NET-084
size: M
est: 200 code, 120 tests
executor: agent
difficulty: needs care
model: standard
diagnostics: the bundle's daemon log tail carries each rejected frame with the session, the lease and the source it carried
observability: one rate-limited warn log line per rejected foreign-source frame with the session, the lease and the source
layers:
- core:
- crates/sessions/src/core/egress.rs: the frame summary carries the lease and the verdict rejects any other source
test (deferred: kani): cargo nextest run -p sessions kani_frame_verdict_admits_nothing_undeclared
- daemon:
- crates/minimald/src/net/switch.rs: the relay takes the lease and rejects foreign IP and ARP sender addresses
- crates/minimald/src/net/gvproxy_network.rs: passes the lease into the relay
- crates/minimald/src/guest.rs: the daemon's own relay passes its own address as the lease
- crates/minimald/tests/netns_root_integration.rs: the attach call follows the new signature
test: cargo nextest run -p minimald relay_rejects_non_lease_source
produces: none
consumes:
- crates/sessions/src/core/egress.rs
proof: A frame a box sends with any source other than its own lease never leaves the relay, and the log names the lease and the foreign source.
depends on:
- blocked by #1629
Proof
A frame a box sends with any source other than its own lease never leaves the relay: the egress leg of every relay (gated per-session and the daemon's own) checks the frame's source against the lease it was attached with and drops the mismatch before the policy verdict, so no conntrack window opens, and the rejection is logged once per lease per minute naming the session, the lease and the foreign source (IPv4 source address, or ARP sender protocol address).
Notes from the agent: Deferred test, lane kani: test (deferred: kani): cargo nextest run -p sessions kani_frame_verdict_admits_nothing_undeclared — the harness exists (crates/sessions/src/core/egress.rs) and was updated to quantify over a symbolic frame source AND lease, not run here; scripts/kani.sh's expect sessions 7 count is unchanged. The harness now carries ~64 more symbolic bits, so the CI kani lane may take longer to solve it. Two commits: 7d7c2e7 (core: summarize reads the frame's source — IPv4 header or ARP SPA, with a too-short-for-SPA ARP frame truncated fail-closed — EgressRules carry the lease, and verdict runs foreign_source() first) and 38e399e + 0363bb5 (daemon: attach_to_switch/attach_to_switch_vsock take the lease, relay_tap_to_switch pre-checks foreign_source before the gate so rejected frames open no UDP conntrack window and log one dedicated rate-limited ForeignSourceReject line instead of the generic R2.7 warn; gvproxy_network passes the allocated lease, guest.rs's root egress passes the daemon's own address, the netns test follows the new signature). Clippy clean for both crates. MAC addresses were deliberately not checked: the lease is an IP lease and the layer note names IP and ARP sender addresses only; a foreign source with the lease's MAC is still rejected because the IP/SPA is what is compared.
Tests
cargo nextest run -p minimald relay_rejects_non_lease_sourceVerify
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_frame_verdict_admits_nothing_undeclaredCloses #1641 8000