Daniel Samson
547d0ec46b
device-authority.md is rewritten as an implementation design rather than a rival to device-manager.md. The what was already settled there in 2026-07: structure in the manager, authority in the kernel, and delegation as the step after hello. This is the how, plus the two decisions that paragraph leaves open. Decision 1: the manager claims, it is not granted. device-manager.md says "claims (or is granted)"; claiming wins because the manager runs before any driver exists and takes the seeded devices unopposed, leaving nothing unheld to race for. One new call, device_transfer(device_id, task_id), checks only that the caller holds the device — no names in the kernel, no attestation. The alternative put a binary path inside the kernel, and the kernel should hold only what cannot safely live in user space. The residual is stated rather than hidden: authority rests on the manager claiming first, which init.csv makes an operator-visible ordering rather than an attacker- controlled one, and the enforced version arrives with the spawn capability drivers.md already names as missing. Decision 2: the kernel stops holding inventory. It reads three things out of a descriptor — physical ranges, interrupt numbers, one PCI BDF — and stores the rest only so device_enumerate can hand it back. Devices with no resources leave the kernel entirely: a USB device conveys no mapping authority, so there is nothing to enforce. That is also the case which sidesteps containment, and therefore the reason a shared cap existed. Decision 3: no shared ceiling. The table becomes dynamic — it is built after heap.init, so nothing ever prevented it — and the two invented numbers go. A per-holder quota replaces them, because dynamic storage with no bound moves the ceiling to the kernel heap, which is shared and fatal rather than partial. A bound charged to whoever caused it is isolation. Two earlier drafts of this document are gone: one gave init the root grants, the other proposed extracting a firmware-framebuffer driver. Both were wrong and both are recorded as wrong in the run plan's settled list — the framebuffer is not a device, it is where pixels go until a real display driver announces itself. Run 2 is nine steps, ordered so the suite stays green throughout: build and prove the transfer mechanism, move the five claimants across one at a time, then the flag day, then the inventory, then the ceilings.
152 lines
8.1 KiB
Markdown
152 lines
8.1 KiB
Markdown
# Device authority: the implementation of delegation
|
|
|
|
*Implementation design, 2026-08-08. The **what** is settled in
|
|
[device-manager.md](../device-driver-development/device-manager.md) — "structure in the
|
|
manager, authority in the kernel", and delegation as the step after `hello`. This
|
|
document is the **how**, and the decisions that paragraph leaves open.*
|
|
|
|
Read first: [drivers.md](../device-driver-development/drivers.md) (the claim is the
|
|
capability), [driver-model.md](../device-driver-development/driver-model.md) (the three
|
|
invariants), [device-manager.md](../device-driver-development/device-manager.md) (the
|
|
tree, the matcher, the supervisor).
|
|
|
|
## The one thing not yet true
|
|
|
|
`device-manager.md` says assignment "stays argv for now", and names the next step:
|
|
|
|
> The step after `hello` exists is delegation: the manager claims (or is granted) the
|
|
> devices and passes the claim to the driver over IPC (the M13 capability-transfer
|
|
> mechanism), replacing first-come-first-served `device_claim` with policy.
|
|
|
|
Until that lands, the manager's matching is advisory. `device_claim` checks only that
|
|
the device exists and is unheld ([devices-broker.zig](../../system/kernel/devices-broker.zig)):
|
|
|
|
```zig
|
|
pub fn claim(id: u64, owner: u32) ClaimError!void {
|
|
if (id >= count) return error.NoSuchDevice;
|
|
if (claimed[@intCast(id)] != null) return error.AlreadyClaimed;
|
|
claimed[@intCast(id)] = owner;
|
|
}
|
|
```
|
|
|
|
A driver is spawned with its device id in `argv[1]` and claims it; any process could
|
|
pass any integer instead. Since a claim is a licence to map physical memory, that is the
|
|
gap this document closes.
|
|
|
|
## Decision 1: the manager claims, then transfers
|
|
|
|
`device-manager.md` leaves "claims (or is granted)" open. **Claims.**
|
|
|
|
The manager runs before any driver exists — `init` starts it from `init.csv`, and it is
|
|
what spawns drivers — so it takes the seeded devices unopposed and there is nothing
|
|
unheld left for anyone to race for. One new call moves ownership on:
|
|
|
|
```
|
|
device_transfer(device_id, task_id) -> 0/-errno
|
|
```
|
|
|
|
The kernel checks only that the caller currently holds the device. No names, no
|
|
attestation, no notion of "the device manager" — the rule is *you may give away what you
|
|
hold*, which is the capability discipline already in force.
|
|
|
|
The alternative was the kernel granting roots to a task it recognises by binary path
|
|
plus a PID-1 supervisor. It is more robust — it does not depend on the manager being
|
|
first — but it puts a binary name inside the kernel, and the goal is that the kernel
|
|
keeps only what cannot safely live in user space. A name is not that.
|
|
|
|
**The residual, stated plainly:** authority here rests on the manager claiming first.
|
|
That holds because `init.csv` decides what starts and in what order, so it is an
|
|
operator-visible ordering rather than an attacker-controlled one — but it is an
|
|
assumption, not an enforced invariant. The enforced version arrives with the spawn
|
|
capability [drivers.md](../device-driver-development/drivers.md) already names as
|
|
missing ("`system_spawn` is currently ungated … because there is no spawn capability
|
|
yet"). This design is compatible with it and does not block on it.
|
|
|
|
## Decision 2: the kernel stops holding inventory
|
|
|
|
The kernel reads exactly three things out of a descriptor: **physical ranges** (to check
|
|
a mapping falls inside one), **interrupt numbers**, and **one PCI BDF** (to key an IOMMU
|
|
domain). Vendor, device and subsystem ids, class triples, `_HID` strings, bus addresses
|
|
and names are stored only so `device_enumerate` can hand them back — which
|
|
`device-manager.md` already resolves: that call "fades to a manager-internal (then
|
|
deleted) seam", because the manager owns the tree as data.
|
|
|
|
So the kernel's table becomes: **parent, resources, holder, BDF.** That is what cannot
|
|
safely run in user space; the rest moves.
|
|
|
|
**Devices with no resources leave the kernel entirely.** A USB device is addressed
|
|
through its controller and carries `resource_count = 0`
|
|
([driver-model.md](../device-driver-development/driver-model.md): "that case is allowed
|
|
and is the common one"). It conveys no mapping authority, so there is nothing for the
|
|
kernel to enforce and no reason for it to know. It is inventory, and inventory is the
|
|
manager's — reported by `child_added`, which already carries everything needed.
|
|
|
|
That is also the case that made `maximum_children_per_parent` necessary: a zero-resource
|
|
child sidesteps containment, so a driver could loop `device_register` and fill the
|
|
shared table. Once such children are not kernel objects, every remaining entry is a real
|
|
contained subdivision of something the caller holds.
|
|
|
|
## Decision 3: no shared ceiling; a per-holder quota instead
|
|
|
|
`maximum_devices = 64` and `maximum_children_per_parent = 16` are numbers we invented,
|
|
and both are shared — one driver's enumeration starves every other driver, which is how
|
|
an AMD Ryzen booted with no USB and no storage.
|
|
|
|
- **The table becomes dynamic.** It is built after `heap.init` (`kernel.zig`: `pmm.init`
|
|
at 137, `heap.init` at 179, `devices_broker.init` at 202), so nothing prevents it. No
|
|
specification bounds how many devices a machine has, so nothing should bound ours.
|
|
- **`maximum_children_per_parent` is deleted**, because the authorisation it stood in
|
|
for now exists.
|
|
- **A per-holder quota replaces them.** Dynamic storage without a bound moves the
|
|
ceiling to the kernel heap, which is shared and fatal rather than partial — strictly
|
|
worse. The bound that is *not* worse is one charged to the task that caused it: a
|
|
driver that loops `device_register` exhausts its own allowance, is refused with an
|
|
attributable errno, and is restarted by its supervisor while every other driver
|
|
carries on. That is the microkernel property rather than a workaround for it, and it
|
|
is declared through [bounds.md](bounds.md) like any other.
|
|
|
|
## The shape of the change
|
|
|
|
| | Before | After |
|
|
|---|---|---|
|
|
| Manager gets its devices | claims them, unauthorised | claims them (first, unopposed) |
|
|
| Driver gets its device | `argv[1]` + `device_claim` | receives it in the `hello` reply |
|
|
| Kernel checks | is it free? | do you hold it? |
|
|
| Kernel stores | the full descriptor | parent, resources, holder, BDF |
|
|
| Zero-resource devices | kernel table entries | manager records only |
|
|
| Table size | `maximum_devices = 64` | dynamic, per-holder quota |
|
|
| Children per parent | `maximum_children_per_parent = 16` | deleted |
|
|
|
|
Bring-up order changes for the five claiming drivers: `hello` must precede the claim,
|
|
because the reply is where the device arrives. `pci-bus` today does the reverse — its
|
|
own comment reads "Claim the bridge, map the ECAM, hello the manager, then scan."
|
|
|
|
## What does not change
|
|
|
|
- The three invariants of [driver-model.md](../device-driver-development/driver-model.md):
|
|
a claim is exclusive, a descriptor is a licence to map physical memory, therefore
|
|
containment. This design strengthens the first and touches neither of the others.
|
|
- The display service's GOP path. The framebuffer is not a device — it is where pixels
|
|
go, handed over by the loader, and the compositor uses it as the boot floor until a
|
|
real display driver announces itself
|
|
([display-v2.md](../device-driver-development/display-v2.md)). The kernel wraps it in
|
|
a display-class descriptor so `mmio_map` can hand it over write-combining; that is
|
|
plumbing for a mapping, not a claim about what it is.
|
|
- Supervision, restart, pruning and re-report
|
|
([device-manager.md](../device-driver-development/device-manager.md),
|
|
[process-lifecycle.md](process-lifecycle.md)). Delegation slots into the existing
|
|
`hello` exchange and changes none of it.
|
|
- `device_register` idempotency, which is what lets a restarted bus rebuild the same
|
|
ids.
|
|
|
|
## How it is verified
|
|
|
|
The invariant is: **a process holds what it was handed and cannot name its way into
|
|
holding more.** The suite has no adversarial device case today — the audit's lesson was
|
|
that "the suite contains no attacker" — so this adds one: a process that was handed
|
|
nothing calls `device_claim` and `device_transfer` on a device another driver holds, and
|
|
on one nobody holds, and is refused each time with its own errno.
|
|
|
|
The Ryzen is the acceptance test for the ceiling half: it is the machine that found the
|
|
constants, and the one that proves them gone.
|