Repository navigation
Beta gap closure: bounded WORM audit, net driver hardening, ARM lint and nTWE - #3
Merged
Merged
Conversation
The mobile WORM chain grew without limit and several denials were serial-only. It is still one hash-chained, append-only log, but each event class now has a fixed quota (total capacity 456 entries including summary slots). Overflow is coalesced into counted summary entries that are also printed on the serial log, state-changing entries keep reserved headroom, and verify() also checks the per-class counts against the quotas. Repeated identical reconciler incidents are recorded once, and a clean reconcile pass is recorded once and then only counted. Now audited with authorized=false, within their quotas: MARSHAL Refuse and HardStop blocks, capability denials for all eSIM, MVNO and data syscalls, and the MVNO gate_enable refusal. RIL and IPC capability denials, a malformed SYS_DATA_SESSION_CLOSE argument, an unknown reset mode and the no-period SYS_DATA_PERIOD poll stay serial-only. Residual gaps are listed in the ADR: first-N retention per class, the applied class can still be exhausted by a capability holder, quotas are global rather than per caller, and the chain is still volatile and unsigned.
… F6) F5 (ARM, high): validate_rx_completion had no lower bound on the device-written length and RxToken::consume subtracted the virtio-net header length unchecked, so a length below 12 underflowed into a huge slice length (undefined behaviour in a release build). The validator now rejects len < 12 and consume saturates, the same fix the x86 driver received in 51c606f. F6 (ARM): the driver accepted any device QueueNumMax except 0 while posting 8 RX and 4 TX descriptors regardless. It now picks the largest power of two up to min(QueueNumMax, 256) and fails through the existing QueueSetupFailed path only if that is below the posted descriptor count. Not memory-unsafe (all ring accesses stay in the three-page region), but a protocol violation that stalls RX with a non-spec device. F1 (both): receive() consumed a used-ring RX entry before validating it and before checking TX capacity, and never re-posted the buffer on an early return, so bad completions or a TX-full burst permanently lost RX buffers. TX capacity is now checked first (one pure service_rx entry point), a bad length with a valid id re-posts its buffer, and an out-of-range id is counted and skipped. At most 16 used entries are examined per call. F4 (both, partial): a per-buffer posted bitmask means a second avail entry is never written and a used entry for a buffer the driver holds is counted and dropped (DropNotOwned). Limit: a forged completion that arrives after a legitimate re-post is indistinguishable from an honest one and can still duplicate an avail entry; closing that needs a used-index snapshot at re-post time. The policy lives in a pure rx_policy.rs, byte-identical in both crates, with host tests including an 8-buffer pool model, a proptest over ids 0..8 and call-sequence tests that pin the TX-first order. Safety comments are added to the previously undocumented ARM unsafe sites. rustfmt-only changes in net-driver-host/src/main.rs.
grid-sandbox-host, net-driver-host, blk-driver-host and net-driver-host-arm are not workspace members, so the root fmt and clippy steps never reached them, and the undocumented_unsafe_blocks lint three of them carry was only ever checked locally. Add one fmt + clippy -D warnings step per crate to the host job. grid-sandbox-host has no library target, so it is checked with --bins only. net-driver-host-arm does not carry the lint yet, so it is enforced for three of the four crates.
Reflect the bounded WORM chain and denial auditing (ADR 0009) across STATUS, BETA_CRITERIA, the Beta release notes draft, ADRs 0001 and 0006 and the ADR index: Refuse/HardStop and capability denials are now audited within quotas, the chain is size-bounded, and the stated serial-only remainders are updated. Correct the net driver statements for the RX length, queue-size and buffer-loss fixes, and add CHANGELOG entries for the audit chain, the net driver fixes and the new CI lint step.
…x0 operand
Every previously undocumented unsafe site in syscall.rs, virtio_net.rs and
main.rs now has a // SAFETY: comment stating its invariants, and the crate
carries #![warn(clippy::undocumented_unsafe_blocks)] like the other three
ring-3 host crates, so the host-crate CI lint step now covers all four.
Virtqueue::new's safety docs also state the 8-byte alignment the code needs.
Bug fix: the two svc #0 blocks in _start declared x0 as in(..) although the
kernel overwrites x0 with its return value. They are now
inout("x0") .. => _. Unobservable before (nothing read x0 afterwards and the
kernel does not return from these calls) but the old declaration let the
compiler assume x0 was preserved. A kernel-arm QEMU boot with the TCP
workaround still reaches result=0 (Pass) through the edited
SYS_NET_PROOF_DONE block; the SYS_MARSHAL_PROOF_DONE block got the same
change and is exercised by the proxy-backed CI steps.
Correction to 1ea0537: its message says a used-index snapshot at re-post time
would close the forged-completion hole in the RX ownership guard. It would
not. A snapshot could only reject an entry the device wrote before the
re-post, and a hostile device writes it after, which is indistinguishable from
an honest completion; everything the driver can observe is device-written.
The real defences are an IOMMU or treating the device as trusted.
Binding is a prerequisite of enabling: mvno::gate_enable returns NotBound for an unbound profile. esim.enable is fail-open because enabling may be needed to bootstrap connectivity to MARSHAL, so failing bind closed would stop an offline-provisioned device from ever binding and therefore from ever enabling, defeating that exemption. The three remaining fail-open actions (enable, bind, suspend) now each have a recorded reason and revisit conditions in ADR 0008; ADR 0003, BETA_CRITERIA and STATUS no longer call them open decisions.
SCTLR_EL1.nTWE was never configured, so on a core where it resets to 0 an EL0 wfe (the idle loops at the end of the EL0 payloads and the panic handler of net-driver-host-arm) trapped to EL1 with EC 0x01 instead of idling. mmu.rs install() now sets nTWE together with the MMU bit through a pure helper, hw_contract::sctlr_with_mmu_and_el0_wfe, still a read-modify-write that only ORs bits in. nTWI is left alone because no EL0 code runs wfi. QEMU's cortex-a53 resets SCTLR_EL1 to 0xc50838, which already has nTWE set (measured), so this is a no-op there and is covered by the helper's unit tests only. net_process::setup took the boot-info mode and the MARSHAL request bytes independently, so mode 1 without request bytes would have faulted at EL0 on the first access to the unmapped request pages. It now calls hw_contract::check_net_mode first, before anything is allocated or mapped, and rejects mode 1 without bytes, mode 0 with bytes and unknown modes through the existing Err path (no panic: kernel-arm is panic=abort). Both current callers agree by construction and are unaffected. A kernel-arm boot (secure and non-secure, TCP workaround) still reaches net TCP proof result=0 (Pass) with no EL1 EXCEPTION line.
Removing the try_post refusal in post_rx_buffer was caught only by the two cfg-gated double_post unit tests (one per build profile), because the proptest model checked is_posted itself before calling it. The new post_rx_buffer_refusal_path proptest calls the real function unconditionally over posted, unposted, out-of-range and usize::MAX indices and checks that the write callback runs exactly once per not-posted-to-posted transition and that the mask matches an independent model. In debug an illegal call trips the debug_assert (caught with catch_unwind); in release it is a silent skip. A mutant that makes try_post always succeed and one that ignores its result both fail the new test in debug and in release. Test code only; the two rx_policy.rs files stay byte-identical.
… test Adds the Unreleased entries for the three changes above, including the measured fact that QEMU already resets SCTLR_EL1.nTWE to 1.
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
2 participants
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.
Summary
Continues the Beta gap closure after #2. Nine commits, all on
kernel-armand the ring-3 net drivers plus their docs and CI. No change to any trust boundary or to which actions MARSHAL gates.verify()also checks the books).Refuse/HardStopblocks, capability denials (eSIM, MVNO, data) and the MVNO enable-gate refusal are now WORM-audited withauthorized=false. Reconciler incidents are deduplicated and clean passes are coalesced.net-driver-host,net-driver-host-arm).kernel-arm: setsSCTLR_EL1.nTWE(EL0wfeno longer traps on cores where it resets to 0) and rejects a boot-info mode that disagrees with the MARSHAL request bytes before anything is mapped.net-driver-host-arm: 12 undocumentedunsafesites documented,undocumented_unsafe_blocksenabled, and thex0operand of twosvc #0blocks fixed (in->inout ... => _).-D warningsfor the four ring-3 host crates, which are not workspace members and were never linted in CI.mvno.bind_profilerecorded as fail-open on purpose (binding is a prerequisite of enabling), updated STATUS/BETA_CRITERIA/CHANGELOG.What this does not claim
1ea0537) says a used-index snapshot would close this; that is wrong, and6bfe6efcorrects it. Everything the driver can observe is written by the device.nTWEchange is a no-op on QEMU (cortex-a53 resetsSCTLR_EL1to0xc50838, bit 18 already set; measured). It is covered by the helper's unit tests only, not by any boot.appliedclass can still be exhausted by a capability holder; the chain is still volatile and unsigned.SYS_DATA_SESSION_CLOSEargument, an unknown reset mode, the no-periodSYS_DATA_PERIODpoll.Verification and what CI will show for the first time
Done locally: unit/property tests (kernel-arm 154, net-driver-host 30, net-driver-host-arm 29), mutation checks for each new guard, fmt and the exact clippy lines, x86 QEMU net tests (ICMP, DHCP, TCP via a guestfwd workaround), and kernel-arm boots (secure and non-secure) reaching
net TCP proof PASS. Several independent verification passes were run.Never run before this PR, because the workflow only triggers on PRs and pushes to
main:Refuse/HardStopaudit assertions in the proxy-backed boots (Refuseruns against a Python stand-in listener; onlyHardStopruns against the realcitadel_proxy);SYS_MARSHAL_PROOF_DONEblock touched by thex0fix.If any of those fail, the fix is likely an assertion count or a lint line, not a logic change.
Not in this PR
docs/BETA_MOBILE_PROGRESS.mdanddocs/THREAT_MODEL.mdare local-only and are not part of the history.