From ca1126537d91286e647608be35c66524e05a6c21 Mon Sep 17 00:00:00 2001 From: Daniel Samson <12231216+daniel-samson@users.noreply.github.com> Date: Sat, 8 Aug 2026 22:01:49 +0100 Subject: [PATCH] =?UTF-8?q?docs:=20Run=203=20=E2=80=94=20close=20the=20cla?= =?UTF-8?q?iming=20hole,=20six=20steps,=20no=20open=20questions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One field settles both outstanding questions. The kernel records who gave each device. device_claim then refuses anything that has a giver, and on death a device reverts to its giver rather than to nobody. The framebuffer needs no exemption: nobody delegates it, so it has no giver, so the display service claims it exactly as today. The rule never mentions display. And restart stops racing. Today a dying driver releases its claim to nobody and the manager re-claims first-come, so every restart reopens the hole this run closes; a loan that reverts to its lender removes the window entirely. The zero-resource inventory question is dropped from the plan rather than carried as a blocker. It is real but nothing depends on it. --- docs/bounds-track-plan.md | 53 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/docs/bounds-track-plan.md b/docs/bounds-track-plan.md index c8a7a73..8044f10 100644 --- a/docs/bounds-track-plan.md +++ b/docs/bounds-track-plan.md @@ -95,6 +95,59 @@ They land together, with the manager claiming only for drivers in an explicit anything in D4 — recorded rather than dismissed, because D4 moved the `hello` earlier and so did shift boot timing. Watch it across the remaining steps. +--- + +## Run 3 — close the claiming hole + +*Every driver now receives its hardware. What remains is that `device_claim` still +works for anyone, so a device nobody holds can still be taken. Six steps, no open +questions.* + +### The rule this run implements + +The kernel records, per device, **who gave it**. From that one field everything follows: + +- `device_transfer` and the spawn-fused grant set the giver. +- **`device_claim` refuses a device that has a giver.** A device that was given to + someone is delegated hardware and must be handed on, never taken. +- **On death a device reverts to its giver**, if that task is still alive; otherwise its + claim clears. A grant is a loan, not a gift. + +Two things fall out rather than being special-cased: + +- **The framebuffer is untouched.** Nobody delegates it, so it has no giver, so the + display service can still claim it exactly as today. No exemption in the kernel, no + mention of display anywhere in the rule. +- **Restart needs no race.** A dying driver's device returns to the manager, which + re-delegates it on respawn. Today the kernel releases it to nobody and the manager + re-claims first-come, so every restart reopens the hole this run closes. + +| Step | What | +|---|---| +| E1 | Record a giver per device; `device_transfer` and the spawn grant set it | +| E2 | On task death a device reverts to its giver if alive, else its claim clears | +| E3 | `device_claim` refuses a device that has a giver | +| E4 | The manager claims every resource-bearing device at boot, so nothing is left takeable | +| E5 | The attacker fixture gains the claim half it has been waiting for since D2 | +| E6 | Delete the delegated-set scaffolding — every driver is delegated now | + +Ordering: E1 alone changes no behaviour. E2 must precede E3, or a restart cannot +re-acquire. E4 must precede E5, or the attacker will find takeable devices and the +assertion will be wrong about why. E6 is cleanup. + +### Not in this run, and not blocking it + +**Zero-resource devices stay in the kernel.** Moving them out needs an answer to who +mints their ids, given that the id is the `device_token` on the usb-transfer wire and +the kernel's idempotency is what keeps it stable across a bus restart. Nothing depends +on it: both invented ceilings are already gone and this run does not need it. Recorded +as future work. + +**Not every driver hellos.** Delivery no longer needs it, so it stands or falls on its +own merits — uniform liveness and one class of driver. Also future work. + +--- + ### Question 9 — answered: a singleton gets every device that matched it The 8042 is one controller described by two ACPI nodes, so it cannot be split across