danos/docs/os-development/device-authority.md

Device authority: the implementation of delegation

Implementation design, 2026-08-08. The what is settled in 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 (the claim is the capability), driver-model.md (the three invariants), 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):

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 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: "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 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: 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). 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, 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.