Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Kernel attack gaps

What

Claims the kernel pages state as built that no bench case attacks, or that only the model attacks. Each page’s status line says “partly tested” for these and names the gap. One line per gap: the page’s section, the claim, and what no case attacks.

ipc.md

  • R1 (flow): a call or send between user budgets with different labels is attacked only in the model.
  • R2 (fair waiting): the keying of groups by account, label set and (for account 0) budget is attacked only in the model, and on the kernel turns between groups only by ipc-fair-label-sets (two unlabelled groups beside a vault’s turn); redoubt-ipc fills one group’s cap.
  • What receive returns: a record made unwritable while its thread waits is attacked for an exit notice (process-attack’s late record), an interrupt and an abandoned-call notice (receive-bad-record); for a message it is not attacked.
  • How a call completes, R13 (one outcome per call): completion races between harts are not attacked.
  • R14 (unforgeable sender): every case delivers account 0 and no labels; a non-zero account or a label set reaching the receiver unchanged is attacked only in the model (MsgNoLabels, MsgAccountZero).

README.md

  • What the kernel keeps: that no driver, file system, naming or policy code sits in the kernel rests on the source map, not a case.
  • The no-cruft gate has no self-check: no planted forbidden name, allow(dead_code), unused feature or second PAGE_SIZE is shown to fail it.
  • The TCB’s line count is measured, not pinned by a case; only unsafe has a ceiling.
  • Nothing checks that every kernel/src file appears in the source map.
  • The unsafe ratchet cannot show that every on-target TCB source file is listed in a budget.

objects.md

  • What objects cost: an endpoint’s one page to its owner is attacked only in the model (R6EndpointsFree).
  • What objects cost: a device object’s one page to system is attacked by nothing.
  • What objects cost: the header page is pinned by no case.
  • mint: Dead from a message source whose call’s stamp was destroyed has no case and no mutation.
  • R9 (stamps): a handle minted from a call taking the call’s handle’s stamp (not the caller’s budget) is attacked only in the model (R9MsgStampIsSenderBudget).

budgets.md

  • R6 (charging): an endpoint’s page charge is attacked only in the model; the header page is pinned by no case.
  • R10 (destruction): timeouts before deadlines at an equal instant is attacked only in the model (ExpireBudgetsFirst).
  • Class is trust, not order: that the scheduler never reads class is argued from the code.
  • Deadlines: a process entering the kernel in a tight loop to put its deadline off is not attacked.
  • Root, system and users: no case checks the boot table (root’s 510 processes, the weights, INIT_WEIGHT).
  • R10 (destruction): destroying the budget a device object is charged to (the device destroyed, every handle closed) is not checked by a case.

timer.md

  • Time: that time_now counts from the kernel’s start is not checked (only monotonic, never early, linear with rdtime).
  • Expiry: the order at an equal instant (timeouts before deadlines; (pid, tid); budget id) is attacked only in the model (ExpireBudgetsFirst).
  • Budget deadlines: a destroyed child’s later deadline leaving the list is shown only by the kernel surviving past it.
  • Failure and restart: a boot with no Time tag (or 0) powering off is not attacked (R17 (fail closed)’s gap too).
  • The hart timer: a stale early hint costing one early interrupt and missing nothing is argued, not attacked.
  • A passed deadline comes first: a process entering the kernel in a tight loop to put its deadline off is not attacked (the same gap as budgets.md’s).

devices.md

  • Device objects: a DMA device past MAX_DMA_DEVICES (16) getting no object is not attacked: QEMU virt has eight virtio-mmio slots, and the bench hands QEMU no device tree of its own (the page a device object costs is measured by device-object-page).
  • Reset before reuse: that the reset precedes pooling inside the kernel is attacked only in the model.
  • Devices handed to the first program: the loader’s refusal of a device tree with no console, or a console with no interrupt, is not attacked (no case boots a crafted device tree).
  • R5 (interrupts): masking a fired source is attacked only in the model (QEMU’s 16550 raises per byte); completing the claim before masking, and billing interrupt time to the IRQ object’s owner, are argued on the page (QEMU’s PLIC accepts a completion for a masked source), not attacked.
  • R18 (device authority): the kernel’s refusal of a malformed Devs entry and of a Grnt boot argument is not attacked: the loader emits neither, no case hands the kernel a crafted argument block, and no device tree can produce a Grnt tag.
  • Failure and restart: at the destruction of a device object’s owner budget the source’s mask is argued on the page (device-owner-destroy attacks the waiters’ Dead and the handle sweep); a device handle closing with the budget that stamped it has no case short of the tree’s end, every device handle’s stamp being root.

processes.md

  • Processes and PIDs: that PIDs are drawn at random is not attacked.
  • Threads: thread_create refused with OutOfMemory, and the first thread returning from its entry (a fault), have no case.
  • Creating and starting: OutOfMemory from process_start has no case.
  • Exit notices: a notice dropped because its exit endpoint was destroyed has no case.
  • R21 (crash blame): blame after the blamed sender’s budget is destroyed has no case; a thread holding a parked call that receives a send and then faults (blames nobody) is covered only in parts.

memory.md

  • Backing and zeroing: that a frame freed with data comes back zero is attacked by smp-inflight-race’s witness, but no case can tell which frames it was handed; a frame free since boot zeroed at its first allocation cannot be told from one QEMU left zero.
  • Frames in flight, R81 (frames in flight): no case lands a stale store in a frame being zeroed (QEMU drops a hart’s TLB at its next satp write); the order is the trace’s.
  • Instruction fetch after mapping: no case can see a missing fence.i (QEMU keeps fetch coherent).
  • Lending at the page-table level: a lend within one process is not attacked across harts.
  • R11 (memory): the absence of any physical-address argument is argued from the call table.
  • R19 (kernel W^X): no case plants a writable kernel code page to show the boot check stops.

scheduling.md

  • One flat stride queue: round-robin among one budget’s threads is not attacked. sched-round-robin.
  • Preemption points: an interrupt’s wake not preempting, and another budget’s deadline preempting, are not attacked. sched-irq-wake, sched-deadline-preempt.
  • The current minimum and ties: clauses 1 and 4 are checked on the target only when a run happens to tie, and no case can make one: a waker ties a requeued budget, and two requeued budgets tie, only at passes equal to the tick, which charging makes a coincidence; the host tests and model attack them.
  • Charging: interrupt handling billed to the device object’s owner is not attacked. sched-irq-wake.
  • Responsiveness: budget_destroy call-to-return is recorded, not asserted. sched-latency (destroy_call_p99_us).
  • R12 (scheduling): the bound on a call’s kernel time is attacked for the memory calls (map-anon-search-bound, scan-bounds, worst-walk) and the endpoint, handle, thread, IPC and clock calls (call-bounds); not for lends and transfers, process_map, set_flags and the device calls.
  • R23 (no test channels): no case builds the production kernel and scans it for the trace. bench-no-trace, bench-trace-scan-catches, bench-test-only-refused.
  • Failure and restart: a picked thread dying before the switch needs another hart’s destruction to land between kmain’s pick and its switch, which no case can time; the queue cannot be filled (one slot per process). Neither is attacked by a case.

boot.md

  • Firmware: the bench never falling back to QEMU’s own firmware is not attacked. Closed: host:testbench::a_missing_firmware_image_fails_the_case_rather_than_falling_back, host:testbench::every_boot_names_the_checked_firmware_and_a_tree_only_when_edited.
  • The argument block: the kernel’s refusals of a block only the loader could write (a tag past the end, a second MREx, a Devs entry that names RAM or a controller, wraps or names interrupt 0, a Grnt tag) are not attacked: no device tree makes the loader write one (it filters RAM and interrupt 0 itself) and the kernel has no host tests; a loader test knob would be a loader change. The one malformed Devs entry a tree can produce, an interrupt past the PLIC’s sources, is attacked: boot-rejects-irq-past-plic. The page says so as a residual.
  • R16 (image confinement): an image cut short inside its segment data and a writable and executable segment are not attacked; the truncated-image case runs on rv64 only. Closed: loader-rejects-segment-data-cut, loader-rejects-wx-segment; loader-rejects-truncated-elf on both widths.
  • R17: a short or missing seed and a missing timebase are not attacked (every QEMU boot supplies both); nor an initrd under 64 bytes. Closed: boot-rejects-no-seed, boot-rejects-short-seed, boot-rejects-no-timebase (the tree QEMU built, edited), verified-boot-rejects-short-initrd. The kernel’s own refusal of a missing Seed tag stands behind the loader’s and is not reached; the page says so.
  • Verified boot, R15 (verified boot) and R17: the two signature cases run on rv64 only. Closed: both on both widths.
  • Devices handed to the first program: a DMA device past the sixteenth getting no object is not attacked (as devices.md’s): ATK3’s, with devices.md’s line.
  • Failure and restart: a reboot through system_reset (the chain rerun, the bundle verified again) is not attacked. Closed: reboot-verifies-bundle.

memory-layout.md

  • satp and the TLB: no case attacks a stale translation surviving an address-space switch or an unmap (one hart, global flush; argued from the code; attacked across harts in M2 (usable shell): several harts).
  • Placement areas: the message area (0x4000_0000, 4 MiB) and map_anon area bases are not attacked as addresses (not security claims; listed for completeness).

abi.md

  • The kernel keeps every register outside a0-a7 across an ecall: no case attacks it.
  • The order of checks after decoding: pinned by a case only for the first checks of budget_create, budget_usage (records before the handle: budget-syscall-attack), call (record before endpoint lookup: ipc-outcomes), receive (WrongObject), serve, process_start (count before record: process-attack). The rest of each row (stages 2 to 5) is not attacked.
  • The kernel’s order against the model’s: no trace replay (planned for M3 (agents, approvals and the attack suite)), so the rows that differ were found by reading only.
  • A valid call number with bit 32 set on rv64: not attacked (legacy-gone does it for 0..=46 only).

invariants.md

  • I7 (every flow obeys R1): a message between user budgets with different labels: no case (the same gap as ipc.md’s R1).
  • I9 (pages W^X, zeroed, lends unmapped): reuse of a freed frame (a case cannot choose which frame it gets; mem-attack says so): model only.
  • I11 (fair turns): turns among several groups on one endpoint: model only (the same as ipc.md’s R2).
  • I12 (ids never reused): budget and message ids never reused: invisible to a process, model only; endpoint, device and process-object ids: nothing attacks them, not even the model (it checks budget ids only).
  • I13 (every blocking call returns by its timeout): timeouts on a multi-hart boot: timeouts has no smp key (M2 (usable shell): several harts).
  • I16 (DMA pages reset before reuse): a live co-holder that still reaches a device reset at another holder’s death: model only (reset_at_one_death_does_not_cover_a_co_holder).
  • I1 (handles name live objects) and I10 (create-destroy leaves the parent unchanged): no mutation targets I1 alone; I10’s R10KeepCarvedLimits is caught first by the per-step R6 recount, so budget_lifecycle’s own check may be doing no unique work. Not a gap in the kernel, a note on the model.

model.md

  • R15 (verified boot), R16, R17, R19 and R23: not in the model at all.
  • steward_noninterference leaves out a server crash at an instant and one a vault’s call causes (service-slot timing, a residual of R37 (vault non-interference)).
  • Model replay on the real kernel: no case; every “attacked only in the model” on the kernel pages rests on it.
  • The budget test’s hand-copied model sequence: nothing checks it still matches the model.

Why it matters

A status line that says “built” promises a test that would fail if the claim were false. Each line here is a claim whose failure no bench case would see: it rests on the model, on reading the code, or on nothing. The model’s evidence about the kernel is only as good as its replay against the kernel, which does not exist yet.

Where

  • tests/: the bench cases, one .toml each, and their programs in tests/programs.
  • model/: the executable model, its properties and mutations.
  • The kernel pages in docs/kernel, whose status lines name each gap.

Done when

Each line has a case that attacks it, and the page’s status line names that case; or the page states the claim as argued from the code, outside any “built” status. The file is empty when every kernel section’s status line is built · tested.