Devices and DMA

A driver reaches hardware only through a device object: an MMIO range (which may carry a DMA flag), an interrupt line, or the Reset right. The kernel makes one for each device the loader describes at boot and never makes another. Holding a handle to one is the whole authority: to map the registers, to receive the interrupt, to allocate memory the device may write, or to power off. Memory given to a device is never reused until the device has been reset, and a device that does not confirm its reset keeps that memory, and loses its object, until reboot.

Purpose

Devices are where a capability system is easiest to get around. A process that can program a bus master can make it read or write any physical address; one that can reach the interrupt controller can silence everyone’s interrupts; one that can name RAM by address can read any page. So the kernel keeps device authority in objects like every other authority, keeps the interrupt controllers and RAM out of reach altogether, and makes sure a dead driver’s device cannot keep writing into pages that have passed to someone else.

Interface

Device objects

Status: built · partly tested: the refusal of a DMA device past the sixteenth is not attacked by a case (QEMU virt has eight virtio-mmio slots, and the bench hands QEMU no device tree of its own: Residual risks) · tested: bench:device, bench:irq-attack, bench:dma-rules, bench:device-object-page

A device object takes one of three forms (kernel/src/device.rs):

The loader reads the machine’s device tree and describes each device in the argument block’s Devs tag, and the interrupt controllers in its Ctrl tag (boot). The kernel turns each Devs entry into an object while it builds the budget tree, and refuses to boot on a malformed one (R18). No call creates a device object, so the set is fixed by the machine.

A DMA-flagged device also gets a slot in the kernel’s reset registry, keyed by its base: at most MAX_DMA_DEVICES (16) of them. A DMA device past that gets no object at all, because a device the kernel could not reset must not be handed out.

Each device object costs DEVICE_PAGES (1) page, charged to the budget that owns it, as an endpoint is (objects). At boot that owner is system, and that is all system holds: its usage is one page per device object, and one page comes back when a quarantine destroys one (device-object-page). There is no device_destroy: a device object dies when its owner budget is destroyed (R10 (destruction)), or when its device is quarantined (Quarantine). Handles to device objects carry badge 0 and can be copied and closed like any other handle; closing one leaves the object in place. The full error rows of the device calls are in the ABI reference.

map_device

map_device(h(MMIO)) -> addr, len maps the whole range readable and writable, not executable, at an address the kernel chooses (R11 (memory)), and returns the address and the length in bytes. The length is what the driver may touch; which device the handle names is device_info’s answer, and which handles a driver gets is its launcher’s choice. Errors, in order: BadHandle, WrongObject (an IRQ, the Reset right or any other object), OutOfMemory (page tables).

The device’s pages are not RAM and cost nothing; the page tables that map them are charged to the caller’s budget. Each call makes a new mapping, so two calls give two addresses. The kernel keeps no record of who mapped a device: the handle, not a page owner, is the authority, and a mapping outlives its handle. Closing or revoking the handle stops new mappings, not the ones already made; those end when the process unmaps them or ends.

Mapping a DMA-flagged device adds it to the caller’s reset set: the devices the caller’s end must reset before its DMA pages are reused (Reset before reuse), because a process with the registers mapped could have programmed the device with any address it knows.

device_info

device_info(h(device)) -> kind, a, b, flags says which device a handle names, in the form of the Devs entry the object was made from (boot). For MMIO it gives the physical base, the size in bytes and the DMA flag. For an IRQ it gives the interrupt number. For the Reset right it gives only the kind. Errors, in order: BadHandle, then WrongObject for anything that is not a device object. It maps nothing and changes nothing, and its kernel time is a constant.

It is how init matches the manifest’s devices to the handles the kernel gave it (which process gets which device). It shows a holder where the device’s registers are, which a holder that maps them could find out anyway. The address is not RAM and grants nothing, and no call takes a physical address (R11 (memory)). The kernel says which device a handle names; the launcher still decides which handles a driver gets.

The result travels as the Devs entry does: the kind in a1 (1 MMIO, 2 IRQ, 3 Reset), a and b in two registers each, the flags in a6, and a field the kind does not use 0 (ABI). redoubt-sys decodes it as DeviceInfo and refuses any other shape. The kernel’s time is one handle lookup and one read of the object’s frame, whatever the device. The executable model checks every answer it gives against the Devs entry of the device the caller’s handle names, after every step (device_info_answer in model/src/invariants.rs).

dma_alloc

dma_alloc(h(MMIO), npages) -> addr, phys returns npages physically contiguous, zeroed pages, mapped readable and writable at an address the kernel chooses, and their physical address. It is the one call that returns a physical address, and only through a device the loader flagged as a bus master. Errors, in order: BadHandle, WrongObject (not MMIO), InvalidArgument (no pages), NotPermitted (no DMA flag), OutOfMemory (the device’s MAX_RUNS (32) runs all in use, the caller’s budget, no free run of npages in the DMA pool, or the page tables).

Runs come from the DMA pool: DMA_POOL_PAGES (1024) contiguous pages, 4 MiB on both widths, which the kernel takes from the top of RAM at boot and keeps outside every budget, root’s limit included. A run is the first free stretch of npages in the pool, found by a search linear in the pool’s 1024 pages, a constant, never in RAM (R12 (scheduling)). The pool holds one device’s MAX_RUNS runs at 32 pages each; the largest run a driver asks for today is 9 pages. A request longer than the pool’s longest free stretch is OutOfMemory, whatever the caller’s budget holds. A held run is still charged to the caller’s budget, though the pool, not the budget tree, supplies its frames: while runs are held, up to DMA_POOL_PAGES frames of the budget tree go unbought, which is conservative and never short.

Each allocation is a run, recorded against the device it came through. Its pages are charged to the caller’s budget (R6 (charging)), but the ownership table records them as the kernel’s, not the process’s, so no path that frees or moves a process’s own pages can reach them. While the process lives its runs stay put:

• a lend, a transfer or a process_map of a DMA page is InvalidArgument;
• set_flags works on them as on any page, EXECUTE included, which R11 forbids (Residual risks);
• unmap drops only the mapping: the pages stay held, charged and out of the pool.

A run’s device joins the caller’s reset set, as a mapped DMA device does. The pages leave the process only at its end.

Reset before reuse

A DMA device may still hold the physical address of a run after the process that programmed it has died. So no DMA page goes back to the pool until every device that could hold its address has been reset: I16 (DMA pages reset before reuse).

• Trigger: the end of a process, however it ends (exit, fault, kill, its budget’s destruction), after its own pages are released. Not the close of a device’s last handle, because handles copy and a mapping outlives its handle.
• The reset set is every device one of the process’s runs came through, and every DMA device it ever mapped. A confirmed reset at one process’s end does not remove the device from a live co-holder’s set: the co-holder can still program it, so its own end resets it again.
• The reset: for each device in the set, the kernel writes 0 to the virtio-mmio status register through a register window of its own (the device’s first register page, mapped for the kernel alone), then reads it until it reads 0. It waits at most RESET_US (1000 µs) per device on the timebase, and at most RESET_READS (100 000) reads should the timebase not advance, without preemption. With at most MAX_DMA_DEVICES (16) devices in a reset set, one process’s end can spend up to 16 ms here. The kernel does nothing else to the device: it never services it on the driver’s behalf.
• Pooled only if every device in the set confirmed in that same step: then each run’s pages go back to the pool and their charge back to the budget that paid for them. Otherwise nothing is pooled (see Quarantine).

A device confirms only if it answered as virtio-mmio at boot (magic virt, version 1 or 2, read once when its slot is made) and has not been quarantined. Any other device never confirms.

stateDiagram-v2
    [*] --> Mapped: dma_alloc (zeroed, charged,<br/>device joins the reset set)
    Mapped --> Held: unmap (mapping gone,<br/>still charged)
    Mapped --> Ended: the process ends
    Held --> Ended: the process ends
    Ended --> Resetting: status 0 written to every<br/>device in the reset set
    Resetting --> Pooled: every device reads 0<br/>within 1 ms
    Resetting --> Quarantined: any device does not,<br/>is not virtio, or is quarantined
    Pooled --> [*]: pages free,<br/>charge returned
    Quarantined --> Quarantined: payer destroyed<br/>(charge moves to its parent)
    Quarantined --> [*]: reboot

Figure: the life of a DMA run, from dma_alloc to the pool or to quarantine.

Quarantine

When a device in the reset set does not confirm, every run the ending process held is quarantined, the runs through devices that did confirm included: their pages are never pooled, and nothing maps them again. Every device that did not confirm is quarantined too, and the kernel prints DMA: device <base> did not confirm its reset; quarantined until reboot.

• A quarantined device never counts as reset. A later process end whose reset set holds it quarantines all of that process’s runs, even if the device would reset by then.
• Its object is destroyed at that same process end, as R10 destroys one: every handle naming it closes, in every table, and a copy in a message not yet received arrives as 0. Its page goes back to its owner. Its base stays flagged in the registry until reboot, and no device object names it again. The device’s interrupt object is a separate object and is not destroyed. A live co-holder keeps any mapping it already made (see Residual risks).
• Charging: a quarantined run stays charged to the budget that paid for it, the dead driver’s. When that budget is destroyed, alone or in a subtree, the destroyed subtree’s carve first returns to the budget above it, and only then does the charge move there, so that budget never exceeds its limit (I5 (usage within limits)). With no budget above it, the charge ends with the tree.

system_reset

system_reset(h(Reset), kind) powers the machine off (kind 1), reboots it (kind 2), or powers it off reporting a system failure (kind 3), through the firmware’s system reset call; only kind 3 gives the firmware a reason, SystemFailure. init refuses a boot with kind 3, as the loader and the kernel refuse one (R17 (fail closed)). On success it does not return. Errors: InvalidArgument (an unknown kind, refused as the call is decoded), BadHandle, WrongObject (not the Reset right). The kernel lets go of its memory lock before it calls the firmware, because that call never returns.

The console’s one writer

The console’s UART has two writers. The kernel prints its lines through the firmware’s debug console, which writes the same UART, and the process that holds the console’s MMIO device writes its registers: init until consoled starts, then consoled, or in a kernel case the first program. On several harts the two would interleave byte by byte, so a kill line ([!] Terminating process with PID n) could land inside a program’s line and break both.

console_hold(h(MMIO), hold) keeps each writer’s lines whole. The holder takes the hold (hold

1. before it writes and gives it back (2) after. While it holds it, a kernel line waits, whole, in a queue of 4 KiB (about 107 kill lines, a containment-sized destruction’s), and the lines that waited go out when the hold is given back, before the call returns, so they come before the holder’s next write.

• A line left unfinished between writes. A holder’s line can span its writes: a prompt waiting for its answer, a \r sent before the text. Between them nobody holds, so a kernel line goes out at once, inside that line. The holder says so: a give-back with hold 3 says its line is unfinished, and the kernel then ends that line (\r\n) before the next line of its own that finds nobody holding, or before the lines that waited and go out at that give-back, once; that holder’s next take, and only its, returns 1 if it did, and the holder starts its line again (consoled). A give-back with 2 says the line is finished. Nothing else changes: the kernel never waits, a held line waits whole, and the bound below stands.
• The kernel never waits for user mode. A line with nobody holding goes out at once. A line that does not fit the queue goes out at once too, after everything queued: a holder that keeps the hold, or writes for long, then sees a kernel line inside its own write. That is the bound: a holder delays the kernel’s lines by one queue’s worth at most, and never loses or stops one. A holder’s write is meant to be short: consoled holds it a chunk of 256 bytes at a time (consoled).
• Who may hold it. Only through a handle to the console’s MMIO device: the Devs entry the loader marks as the console, the one the device tree’s /chosen/stdout-path names (boot). A second marked entry stops the boot, and with none every hold is WrongObject. Any other device or object is WrongObject. One process holds it at a time: another’s take is Busy, and writes as before. Taking it again, or giving back a hold the caller does not have, changes nothing. A writer that never takes it writes as before.
• A holder that dies holding it was cut off inside a write. The kernel gives the hold back for it as the process ends, ends that line (\r\n), then prints the lines that waited and the kill’s own. The hold is the process’s: a thread that exits holding it leaves it to the process’s other threads, and the last thread’s exit ends the process. A process that dies between writes with its line unfinished is treated the same: the kernel ends that line before the kill’s own, and nothing is owed to its PID after, so a later process given that PID is told nothing.
• When the machine stops (system_reset), the hold ends and the lines that waited go out first. A panic’s text goes out after them and never waits.

Errors, in order: decoding (hold not 1, 2 or 3 is InvalidArgument), BadHandle, WrongObject, Busy. With no kernel console (a build without printing) the hold has nothing to make wait. The rules and the queue are redoubt-conhold, host-tested; the queue sits beside the kernel’s console under the lock its prints already take, one hart at a time (kernel/src/debug/console.rs). The executable model has the call, with the first MMIO device as the console (the loader’s order), and checks that the holder is a live process after every step; the lines themselves are not modelled.

Devices handed to the first program

Status: built · partly tested: the loader’s refusal of a device tree that names no console, or a console with no interrupt, is not attacked by a case (the bench hands QEMU no device tree of its own: Residual risks) · tested: bench:device, bench:irq-attack

The kernel gives every device object to init, the one program the loader starts, to place (below), in the handle order boot gives. The objects are charged to system, and the handles are stamped with root, so they are revoked only with the whole tree (stamps). A program finds its DMA devices by asking: dma_alloc is NotPermitted without the flag and WrongObject on an IRQ or the Reset right.

Which process gets which device

The loader loads only the kernel and init, and init holds every device object. The boot manifest’s devices entry names each device object by its register base and interrupt, and says whether it may do DMA; each server’s entry names the devices it gets (init). init places each driver’s handles in its startup block, by name, so no driver depends on a handle’s index. The Reset right stays with init. In a confined deployment init refuses a manifest that lets two label sets share a device.

• The device tree and the manifest decide together. The loader’s reading of the device tree decides what becomes a device object and which carry the DMA flag, because the kernel must know both at boot to give each DMA device a reset slot. The manifest decides who gets each object. It names each device by its register base and, if it has one, its interrupt number. init asks device_info about every device handle it holds and matches the answers to the manifest. It refuses the boot if the manifest names a base or an interrupt no handle has, names one twice, or says a device may do DMA when the kernel’s object says it may not, or the other way round. A device object the manifest does not name stays with init and is never placed.
• Drivers find their devices by name. init installs a device’s register region under the name the server’s entry gives it, and its interrupt under that name with -irq added (consoled looks up uart and uart-irq, blkd disk and disk-irq, netd net and net-irq). The names are init’s: it matched them to the kernel’s objects with device_info, and a driver relies on the name, never on a handle’s index.
• init keeps a copy of every device handle it places, so that it can place the handle again when it restarts a driver. It never maps a device after it starts consoled, and a copy it never maps never puts it in a reset set, so being a co-holder costs nothing at a driver’s end (reset before reuse).
• A driver whose device was quarantined is not restarted; init reboots the machine. The device’s object is gone, and only a hardware reset can make a device whose reset was never confirmed safe to hand out again. This is the same fail-closed reboot as a server that cannot stay up (init).

Authority

• A device handle is the device. An MMIO handle is the right to map its registers, an IRQ handle the right to receive its interrupt, the Reset handle the right to stop the machine. Device handles carry badge 0 and no rights bits.
• A DMA-flagged MMIO handle is kernel-level trust. It lets its holder call dma_alloc and point a bus master at physical addresses. Without an IOMMU the device can then reach any RAM, so a holder of one is inside the TCB while it lives.
• Handles copy. A device handle passes in a message or a startup block like any other. Two holders can both map one device; an interrupt goes to whichever holder’s thread is waiting in receive. A driver that must be alone is alone only because whoever holds the handle gave it to it and to nobody else. Whoever hands out a device handle hands out the device.
• Revocation closes the handle (its stamp’s budget destroyed, or the object destroyed with its owner or by quarantine). It does not reach a mapping already made (see Residual risks).
• Nothing else reaches a device. No call takes a physical address; map_anon and map_fixed give fresh zeroed RAM wherever they map (R18).

Security properties

R5 (interrupts)

When an interrupt fires, the kernel masks its source and sets the IRQ object’s fired flag. receive on the IRQ handle unmasks the source when it begins, then returns an interrupt record as soon as fired is set, clearing it (IPC). There is no acknowledge call. So a source stays masked from the moment it fires until its driver next receives, and a driver that is busy, stuck or dead cannot be stormed by its own device. A level-triggered source still asserted when the driver receives fires again at once, and that receive returns straight away.

• The kernel completes the controller’s claim first, then masks the source, in the same kernel section. Nothing can be delivered in between: the hart takes no interrupt in supervisor mode, and another hart that traps for the source claims it only once it holds the kernel lock, by which time the source is masked and its claim finds nothing.
• An interrupt no IRQ object owns is completed and masked, and stays masked.
• Every IRQ object starts masked, so a source nobody receives on cannot storm the kernel.
• An interrupt that fires with no thread waiting keeps fired set; the next receive returns at once. One fire answers one waiting thread. Threads waiting on one interrupt are woken in the order they began to wait.
• The kernel’s time handling an interrupt is billed to the budget that owns the IRQ object (scheduling), not to whichever budget it interrupted.

An interrupt raised while its object is masked stays pending in the controller, and the unmask at the next receive, the first after a handle is handed over included, delivers it. Masking writes the source’s priority 0, which the PLIC (the RISC-V platform interrupt controller) never delivers on any hart’s context; unmasking writes it back to 1. Every unmask, the re-arm after a claim included, is that receive’s. Why a priority and not the enable bits is on boot.

sequenceDiagram
    participant T as Driver thread
    participant K as Kernel
    participant P as PLIC
    participant D as Device
    T->>K: receive(IRQ handle, timeout)
    K->>P: unmask the source
    Note over K: fired not set: the thread blocks
    D->>P: raise the line
    P->>K: external interrupt, claim
    K->>P: complete the claim
    K->>P: mask the source
    Note over K: fired set, then cleared<br/>by answering the waiting thread
    K->>T: record: kind = interrupt
    Note over T,D: the driver services the device,<br/>the source stays masked
    T->>K: receive(IRQ handle, timeout)
    K->>P: unmask the source
    Note over P,D: a line still asserted<br/>fires again at once

Figure: one interrupt, from the driver’s receive to the next.

R18 (device authority)

Status: built · partly tested: the kernel’s refusal of a malformed Devs entry (one overlapping RAM or an interrupt controller among them) and of a Grnt boot argument is not attacked by a case (the loader emits neither, and the bench hands the kernel no argument block of its own: Residual risks) · tested: bench:irq-attack, bench:legacy-gone, bench:device-info-attack

Device objects are the only device authority. A process reaches an MMIO range, an interrupt or the Reset right only through a handle to its device object; a process that holds none gets BadHandle from every device call, and the holder keeps its interrupt. No call names a physical address, so neither a device’s registers nor RAM can be reached by address (R11). No call number outside the call table does anything: each is InvalidArgument, so no number claims an interrupt or maps a physical address. The bundle carries no list of device claims: the loader reads no entry it does not load (boot), and the kernel refuses a Grnt boot argument.

Two ranges never become device objects, because either would give away everything else: an interrupt controller (a holder of the PLIC could mask and raise every source; one of the CLINT, the core-local timer block, could forge timer interrupts) and RAM. The loader leaves both out of the device list, but that is a reading of a device tree the kernel does not trust, so the kernel checks every Devs entry itself. It refuses to boot on an MMIO entry that overlaps RAM or a Ctrl range, wraps the address space, is empty or is not whole pages, and on an IRQ entry for interrupt 0 (the hart timer, a hart resource and not a device) or for one at or above MAX_IRQS (1024: the PLIC numbers its sources 1 to 1023, and the kernel’s IRQ index has a slot for each). The kernel maps the PLIC for itself alone.

Failure and restart

• A driver ends, however it ends: its device mappings go with its address space, its handles close, and its DMA runs are reset and pooled, or quarantined. The device objects survive, so another holder can hand the handles to a restarted driver, which finds the device reset. A PID the driver held passes on with none of its mappings or handles (R20 (PID reuse)).
• A driver dies mid-interrupt: the source stays masked until the next receive by any holder of the IRQ handle.
• A device fails its reset: it is quarantined, its object destroyed and its handles closed everywhere; it is gone until reboot (Quarantine).
• A device object’s owner budget is destroyed: each device object it owns is destroyed. Threads waiting in receive on an IRQ object get Dead, its source is masked, every handle naming the object closes, and its page goes back (R10). Nothing makes a device object again, so the device is unreachable until reboot.
• The budget that stamped a device handle is destroyed: that handle closes; the object and other holders’ handles stay.
• No argument to any device call can make the kernel panic (I14 (no call panics the kernel)).

Residual risks

• A DMA driver is TCB without an IOMMU. Its device can read and write any physical address it is given, not only its runs. The DMA flag is the loader’s reading of the device tree (compatible names virtio); a bus master the loader does not flag is still a bus master, and whoever maps it can program it. Reset-before-reuse closes one hole, a dead driver’s device writing into pages that have passed on; it does not confine a live driver. The answer is hardware confinement (FPGA platform).
• Only virtio-mmio devices are reset. A DMA device that does not answer as virtio-mmio never confirms, so every process end that reaches it quarantines, even one whose pages that device never held, and such a platform gets no driver restart. The boot read that classifies each DMA device assumes the read has no side effect, true of the virtio nodes the loader flags.
• A reset stops the device for every holder. Any holder that mapped a DMA device, or allocated through it, resets it when it ends, under every other driver of that device.
• A co-holder keeps its mapping of a quarantined device, and of any device whose handle was revoked: the kernel does not unmap device ranges. It can go on programming a quarantined device until it ends, when its own runs are quarantined in turn.
• One early process holds all device authority: init holds every device object, the Reset right and every DMA device, and nothing narrows that until it places them (below).
• A device tree that hides a controller from the loader’s controller search as well as from its device list defeats the kernel’s Ctrl check: the kernel’s own list of controllers comes from the same tree (boot).
• Quarantine costs memory for good, in exactly the hostile case, a device that ignores its reset: its runs stay charged to the dead driver’s budget, then its parent, and out of the DMA pool, until reboot. A quarantined run through a device still in service also keeps one of that device’s MAX_RUNS places.
• The reset poll is not preemptible: up to 1 ms per device in the reset set, 16 ms at most for one process end, on top of the rest of its teardown (scheduling).
• The order inside the kernel is argued, not attacked. dma-reset-reuse reads the device’s status after dma_alloc has handed a frame to a new holder, so it shows the reset came before the new holder’s use. That the reset strictly precedes the pooling rests on the kernel’s own assertion and the model’s I16 check.
• Two parts of R5 are not attacked on QEMU. Its 16550 console raises the controller once per byte, not from a held level, so a kernel that never masked a fired source passes uart-irq; the mask is attacked in the model. The order, the claim completed before the source is masked, is argued: both writes are made in one kernel section, on a hart that takes no interrupt in supervisor mode, under the kernel lock that another hart’s claim would need, so nothing is delivered between them; and because the mask is a priority write and the enable bits stay, the PLIC does not ignore a completion for a masked source, so even the reverse order would lose nothing on this controller, and QEMU’s PLIC, which accepts either, cannot tell the two apart for a case. The billing, the interrupt’s kernel time charged to the IRQ object’s owner (system at boot, whoever holds the handle), is attacked by bench:sched-irq-wake: the trace records each charge inside a device interrupt, and its oracle requires every claimed interrupt to charge system and nothing but the return to the budget interrupted (scheduling). Masking bounds that time to one interrupt per receive, at the driver’s pace.
• Crafted boot inputs are not attacked. Every case boots QEMU’s own device tree and the loader’s own argument block. So the loader’s refusal of a tree that names no console or a console without an interrupt, a seventeenth DMA device (QEMU virt has eight virtio-mmio slots), and the kernel’s refusal of a Devs entry that overlaps RAM or a controller and of a Grnt tag are code no case reaches: the loader filters the first and emits neither of the last two. A device tree the bench could hand QEMU would reach every one but Grnt, which no tree can produce; that lever is not built.
• The mask at an owner’s destruction is argued. destroy_device fails the waiters, masks the source and then sweeps the handles, the one path quarantine takes too (dma-reset-quarantine); device-owner-destroy sees the Dead and the sweep. A source left unmasked would, at the device’s next interrupt, be completed and masked by the handler for an interrupt no object owns, whose line prints only under debug-print, and the checked build’s count of claims prints at system_reset, which the destruction takes the Reset right away from: nothing a case can see tells a masked source from an unowned one.
• A device handle’s stamp is root. Boot stamps every device handle so, a copy keeps its stamp and mint takes endpoints only (R9 (stamps)), so the one destruction that closes a device handle by its stamp rather than by its object is the whole tree’s.

Why

• Device objects, not claim lists. A per-process list of ranges and interrupts in the signed bundle would be a second kind of authority, checked by process identity and not revocable by budgets. A device object is an object like any other: held as a handle, passed by init, charged to a budget and revoked with it.
• The kernel keeps the controllers and RAM out itself, because the loader’s exclusion is a heuristic over an untrusted device tree, and one missed controller would hand its holder every interrupt.
• Mask on fire, unmask on receive, no acknowledge. The driver’s own receive is the acknowledgement, so one fire costs the kernel one interrupt until the driver asks for the next, and a driver that stops asking stops its device’s interrupts, nobody else’s.
• Reset at the end of a process, not at the last handle’s close, because handles copy and a mapping outlives its handle: the only moment the kernel knows a process can no longer program a device is when that process is gone.
• Reset before reuse, and quarantine when it fails. A dead network driver’s freed pages hold its descriptor tables and rings, and a virtio device re-reads them on every packet. Whoever next owns those pages could post descriptors pointing anywhere: every received frame becomes an arbitrary physical write of network bytes, every transmit an arbitrary read sent out. A driver may reset its own device on a controlled exit (netd does), but one that faults or is killed cannot, so the kernel’s reset is the one that holds. A device that will not confirm is exactly the hostile one, so its pages are given up rather than risked.
• A quarantined device never counts as reset, or a co-holder’s end would pool pages the device may still write.
• DMA pages stay put so that the process whose end triggers the reset is the only one that ever held them.
• The charge stays with the payer, then its parent after the carve returns, so quarantine never takes a budget over its limit and stays with the tree that paid for it.
• map_device returns the length so a driver needs to know nothing about where its device is; which device it holds comes from the manifest, by name.