kernel: claim refuses delegated hardware — and E2 had already closed the hole

The rule as planned: a device that was given to someone may be handed on,
never taken. Implemented, and honest about what it is worth.

Writing the test showed the plan had the wrong step doing the work. A
delegated device is HELD, so an attempt to take it is refused as
AlreadyClaimed before the giver is ever consulted; and once a borrower's
death returns the device to its lender — or clears both when the lender is
gone — there is no state where a device is unheld and still on loan. The
window a stranger could have used stops existing at E2. This check is
unreachable.

It stays anyway: one comparison, failing closed, guarding any future path
that frees a device without clearing its giver, which is exactly the hole
this run closed. The comment says it is unreachable rather than implying a
protection it does not provide.

The attacker fixture does not gain the assertion that was deferred to this
step, and its header records why: there is no refusal for it to observe, and
on a bare boot with no device manager nothing is delegated at all, so the
assertion had nothing to bite on. It failed loudly on its first run rather
than passing quietly, which is the only reason this was noticed.

It also leaves the loader's framebuffer alone without naming it: nobody
delegates the framebuffer, so it has no giver, so the display service claims
it exactly as before.

Suite 118/118.
This commit is contained in:
Daniel Samson
2026-08-08 22:31:04 +01:00
parent 1a1d92cba9
commit ba195fa0a2
4 changed files with 38 additions and 10 deletions
@@ -25,12 +25,13 @@
//! is what cost a debugging session on the Ryzen, so the distinction is
//! part of the contract and is tested as such.
//!
//! **What this fixture cannot yet claim.** `device_claim` is still
//! first-come-first-served at this point in the run — that is the hole D6
//! closes. So the claim half of the invariant ("a process holds what it was
//! handed and cannot name its way into holding more") is deliberately NOT
//! asserted here; it is added to this fixture at D6, when it becomes true.
//! Asserting it now would mean writing a test that documents the bug.
//! **Why there is no "cannot take a delegated device" assertion here.** The
//! hole this fixture was written for is closed, but not by a refusal it could
//! observe. A device that was given to someone is *held*, so an attempt to
//! take it is refused as `AlreadyClaimed` — the same answer as before. What
//! changed is what happens when the holder dies: the device returns to
//! whoever lent it instead of becoming free, so the window in which a
//! stranger could take it no longer exists. There is no moment to catch.
const std = @import("std");
const device = @import("driver");