daniel/danos
1
0
Fork 0
Code Issues 4 Pull Requests Actions Packages Projects 1 Releases Wiki Activity

test: the attacker the device suite never had

Browse Source 
The audit's sharpest finding was structural, not a bug: a fully green suite
had hidden six real defects because it contains no attacker. Every device
case asserts that a driver handed its own hardware can drive it. None asked
what a process handed NOTHING can do.

device-authority-test is that process. It is spawned with no device and
asserts what it therefore cannot do: it cannot give away a device another
task holds, nor a free one, because the kernel's rule is that you may give
away what you hold and the device's state is irrelevant to a process holding
nothing. Asserted across every device the machine actually has, so it cannot
pass by accident of which one happened to be free at boot — six on QEMU,
none of them its.

A positive control runs first. device_enumerate works from this process, so
the refusals below it are decisions rather than a syscall path that is
simply broken here; without it, "everything failed" would read identically
to "the assertions are meaningless". A nonexistent device is refused as
NoSuchDevice rather than NotHeld, because a refusal that cannot name its own
rule is what cost a debugging session on the Ryzen.

What it deliberately does not assert, and says so in its header:
device_claim is still first-come-first-served at this point in the run. That
is the hole D6 closes, and the claim half of the invariant joins this
fixture then. Asserting it now would be writing a test that documents the
bug.

Verified to discriminate: removing the holder check flips "every transfer by
a non-holder is refused" while the positive control keeps passing.

Suite 117 -> 118.
This commit is contained in:
Daniel Samson
2026-08-08 17:23:17 +01:00
parent 3111c7c5e6
commit 33376f24ab
8 changed files with 174 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/bounds-track-plan.md
+1 -1
View File
@@ -40,7 +40,7 @@ that cannot safely run in user space.**
| Step | What | State |
|---|---|---|
| D1 | `device_transfer(device_id, task_id)` — the holder gives a device away | **done** — syscall 54; a move, not a copy |
| D2 | Adversarial case: a process handed nothing is refused, on a held device and a free one | not started |
| D2 | Adversarial case: a process handed nothing is refused, on a held device and a free one | **done** — `device-authority-test`; the claim half joins it at D6 |
| D3 | The manager claims the seeded devices at boot, before any driver is spawned | not started |
| D4 | `usb-xhci-bus` receives its controller in the `hello` reply instead of claiming argv[1] | not started |
| D5 | The other four claimants converted: `pci-bus`, `ps2-bus`, `virtio-gpu`, `acpi` | not started |