The kernel

The Redoubt kernel is a small RISC-V microkernel in Rust. It keeps five things: memory, threads, IPC, interrupt delivery and the timer. Everything else (drivers, file systems, the network, policy) is an unprivileged server that reaches the kernel only through handles and the 26 system calls. The kernel runs in S-mode under RustSBI firmware, one binary for rv64 (Sv39) and rv32 (Sv32). This page says what the kernel keeps, names its objects, measures the trusted computing base, and maps each source file to the page that documents it.

Purpose

The kernel is the part of Redoubt every other guarantee rests on, so it has to be small enough to read in full (TENETS). A reader who wants to audit it needs three things first: what the kernel is responsible for and what it refuses to hold, the objects it hands out and how they refer to each other, and where the code for each rule lives. The pages below this one each take one mechanism; this page is the map.

What the kernel keeps

Status: built · partly tested: that no driver, file system or policy sits in the kernel is read from the source map, not attacked by a case · tested: bench:no-cruft, bench:legacy-gone

Budgets pay for all five: every object, page, process and share of the CPU is charged to one, and destroying one revokes everything under it (budgets, R10 (destruction)). The budget calls are budget_create, budget_destroy, budget_reap (destroy one child, keep the budget) and budget_usage. Two calls sit outside the five jobs. random returns 64 bits from the kernel’s ChaCha8 generator, keyed from the loader’s Seed argument; the kernel also draws PIDs from it. system_reset powers the machine off or reboots it through the firmware, and only a holder of the Reset device object can call it.

The kernel holds nothing else:

• No drivers. Its own console is the SBI debug console. Every real device (UART, virtio block, virtio net) belongs to a userspace server that holds its device object. The console’s UART is shared: its holder takes the console’s hold around each write, and the kernel’s lines wait, whole, for it (the console’s one writer).
• No names. The kernel knows handles, never paths, file names or server names. A process reaches only what its own handle table holds.
• No program loading. The loader places the kernel and init at boot. After that a launcher builds a process with process_map and process_start, and a loader stub inside the new process reads its ELF image (boot, processes).
• No policy. The kernel enforces R1 (flow) on label sets and the budget limits. Who gets which label, lease or capability is decided by init and the steward.

There is one call table. A number in a0 outside it is InvalidArgument, whatever the other registers hold (ABI). The kernel never calls into user code and never switches straight from one process to another. User mode is entered two ways (resuming a thread, or returning from a call) and left one way (a trap), so every instruction a process runs is counted against the budget the scheduler picked (R12 (scheduling)). The kernel runs on every hart, with interrupts off while it runs, under one FIFO lock that a hart takes at its trap from user mode and gives up at its return or idle. Each kernel global (the memory manager, the process table, the timer, the generator) sits in a KernelCell of its own (kernel/src/cell.rs): a run-time-checked borrow under that lock, so a nested borrow is a panic, not two live references. A checked build asserts that the hart reaching it holds the lock; a release build does not check, and rests on the trap paths taking it.

bench:no-cruft reads the sources and fails on a name from a list of call-interface identifiers Redoubt does not have, on a silenced dead-code warning (allow(dead_code) or allow(unused)) in the kernel, the loader, paging, redoubt-layout or the test programs, on a Cargo feature no cfg(feature) reads, and on a second literal definition of PAGE_SIZE or USER_AREA_END. Every exemption is an entry in the case with its reason, and an exemption that covers nothing fails the case (test bench). bench:legacy-gone makes the calls such an interface would take, from user mode, and checks that each is refused and that nothing it asked for happened: no mapping, no callback run, no switch.

The objects at a glance

A process holds handles: indices into a handle table that only the kernel writes. A handle names an object, a badge (a 64-bit number the minting server chose; 0 for the receive right) and a stamp (the budget whose destruction closes the handle everywhere, R9 (stamps)). Index 0 is never a handle. There are four kinds of object:

Each object lives in a RAM frame of its own. Every lookup compares the id in the frame with the id in the handle, and a mismatch stops the kernel rather than naming a reused frame (I1 (handles name live objects)). Threads, handle-table pages and open calls are not objects: no handle names them. A thread is named by its process and its TID (1 to 255). Details, costs and mint are in objects.

flowchart LR
    H["handle<br/>(object, badge, stamp)"]
    P["process<br/>address space, handle table,<br/>exit slot"]
    T["thread<br/>TID 1 to 255"]
    E["endpoint"]
    D["device object<br/>MMIO, IRQ or Reset"]
    B["budget"]
    P -- "holds, in its table" --> H
    H -- names --> B
    H -- names --> E
    H -- names --> D
    H -- names --> P
    H -- "stamp: closed when destroyed" --> B
    T -- "belongs to" --> P
    T -- "blocked sender:<br/>a queued message" --> E
    P -- "runs in, pays for<br/>threads and memory" --> B
    P -- "object page charged<br/>to the creator's" --> B
    P -- "exit endpoint" --> E
    E -- "owner (R1, charged)" --> B
    D -- "owner (charged)" --> B
    B -- "parent, carved from" --> B

Figure: the kernel’s objects and what each refers to. An arrow points from the one that holds the reference to the one it names.

Containment

Status: built · tested: bench:kernel-containment

One boot, bench:kernel-containment, shows that the kernel’s primitives alone contain hostile code before init, the steward or any server is built on them. Hostile code in a lease is preempted, then ended at its deadline or revoked by hand while its messages and lends are in flight, and its victims stay responsive the whole time. The boot is evidence for the kernel only. Sessions have their own cases (M1 (sessions over SSH, kept apart)), and the steward’s leases, approvals and the network theirs (M3 (agents, approvals and the attack suite)).

What runs. The loader starts one program. It holds root, system, users, the console and the Reset right. It builds the budget tree at the weights init gives (init) and starts copies of itself in the tree, as the latency workload does (responsiveness):

• in system: the workload’s driver stand-in and steward stand-in, and a victim server that takes the hostile agents’ calls and holds them open;
• in users: a bystander session, and a sessions budget the steward stand-in holds. The steward stand-in carves each lease from that budget and starts a hostile agent in it, as the steward will.

Each hostile agent runs in a lease the size of the workload’s leases, with room added for a full handle table and one sub-agent. It does all of these at once:

• some of its threads spin and never enter the kernel, and one enters the kernel in a tight loop;
• some threads call the victim server with lends, which the server takes and holds open, and others are blocked in send to it. All of them go through handles minted into the lease’s revocation scope;
• a sub-agent runs in a budget the agent carves from its lease. That budget has a later deadline of its own, and the sub-agent’s process churns threads and processes;
• the agent fills the rest of its lease with endpoints and its handle table up to MAX_HANDLES, so the destruction walks as much as a lease of its size can make it walk.

The bystander also holds a message queued at the victim server that carries a handle stamped with a live lease. The hostile leases come in pairs, one of each kind. One ends at its deadline while the other lives, so two hostile leases are live at every deadline’s end. The steward stand-in then ends the other with budget_destroy after a timeout, which is its decision; that lease is the only one live at its end. Each pair is replaced when both have ended, until nine of each kind have ended.

Verdicts. None of them comes from a hostile agent:

The program’s lines are trusted (rule F) because it owns the console and holds the reset. Its children hold no device and have no path to the console, so no line on it can come from a hostile agent. Each victim reports through a handle the program badged for it, and the program never counts a hostile agent’s report as a verdict.

The run. The boot runs on rv64 and rv32, at the bench’s hart count, one and two in the gate, in a checked build with the tracing kernel (R23 (no test channels)). Its trace ring is 256 MiB (sched-trace-large, at 576 MiB of RAM), not the usual 64: at the 1 ms slice the run writes about ten records a slice, some four million at one hart and seven million at two, and a trace that drops one fails the gate. It uses the latency workload’s virtual time and one pinned seed. Sweeps of 16 seeds on both widths, at one hart and at two, set which seed the gate runs, and this page records them. The targets are the ones in responsiveness, and the gate adds none. If the gate misses one of them, that is a finding against the kernel, not a reason to set a new target.

The sweep at one hart (with the 192 MiB ring then) ran all 16 seeds on both widths, and every run passed. The table gives each run’s net p99 of the deadline notice, R10’s p99 and a lease’s end (the decision wake’s net p99 plus R10’s), in µs, against targets of 40000, 30000 and 125000:

The deadline notice is the target closest to its limit, at 65% in the worst run, and every seed lands within 1.5 ms of the others. An earlier version of the gate showed a second group about 10 ms higher on some seeds. The steward stand-in then polled for its notices in 200 ms waits, and when one ran out just before a deadline, the stand-in was runnable rather than waiting when the notice came, so another party ran a slice first. It now waits in one receive bounded by the deadline. At one hart seed 13 is the worst on both widths for the deadline notice (26197 µs on rv32, 25794 µs on rv64) and a lease’s end, and on rv32 for R10; rv64’s worst R10 is seed 16, at 22385 µs.

At two harts every target is met on all 16 seeds on both widths; the deadline notice’s p99 is 4 to 7 ms above its one-hart value, and R10’s 1 to 1.5 ms. The bystander’s share of the charges (its one thread is owed a hart, 500 of 1000) fell in two modes by the hart it landed on: the one that waited longer for the lock and took the audits, or the other, 445 or 543 to 546 on rv32. With a wait behind another hart’s audit billed to no one it reads 464 on rv64 and 442 on rv32 on the default seed, so at two harts the share is still reported, not judged (@1; scheduling). In µs, against the same targets, before that change:

The case file pins one seed for both widths and both hart counts: the gate runs seed 4, the worst at two harts or within a millisecond of it on both widths: the deadline notice on rv64 (31641 µs; rv32’s worst is seed 3, 3 µs above), R10 on both (23221 and 23908 µs) and a lease’s end on rv32 (28252 µs; rv64’s is seed 9, 27090 µs). At one hart it is 25939 µs on rv32 and 25258 µs on rv64 for the deadline notice, within 0.6 ms of seed 13.

The gate replaces none of the focused cases. budget-deadline, redoubt-revoke, uaf-lent-page, endpoint-destroy-open-calls and sched-latency each attack one clause alone, and each fails with a narrower message. The gate shows that all of those clauses hold together, under load, against one party that tries them all at once.

The TCB and its size

Status: built · partly tested: the inclusive line counts in the table are snapshots, not pinned by a case · tested: bench:unsafe-budget, bench:docs, bench:size-budget, host:testbench::actual_source_counts_still_enforce_the_budget, host:testbench::every_configured_root_must_contain_rust_source

The trusted computing base (TCB) is the code whose failure can break Redoubt’s guarantees: the firmware interface, the loader and the kernel, with the libraries they link, plus any server that programs DMA without hardware to confine it (devices). Lines are every line of the .rs files under the path, comments and in-file tests included, as the ratchet walks them.

Without the firmware, the TCB Redoubt writes is 28,921 lines. The kernel’s unsafe is split three ways in the ratchet:

Trap entry and context restore are global_asm! in arch/riscv/asm.rs, which the ratchet lists but which holds no unsafe keyword. redoubt-sys’s three are the ecall itself, the unsafe trait Transport whose contract the runtime’s unsafe rests on, and Ecall’s implementation of it. redoubt-layout, redoubt-stride and redoubt-signing say #![forbid(unsafe_code)], so their budgets can only stay at 0.

The unsafe counts on this page are kept true by the docs checker: every count in a `unsafe` (pinned) column must equal the ceilings in tests/unsafe-budget.toml, summed over the budgets under a row’s paths or read by a row’s budget name, so a change to a ceiling fails bench:docs until this page follows it (docs checker).

bench:unsafe-budget does not boot. It counts every use of the word unsafe outside a // comment in each budget’s paths, and fails if a count is over its ceiling, or if any use lacks a justification: a // SAFETY: comment within 6 lines above a block, or a # Safety doc section within 16 lines above an unsafe fn, impl, extern or trait. Every ceiling in the TCB equals its count and allows 0 undocumented uses, so one more unsafe anywhere in it fails the case. A budget whose path holds no Rust source fails too, so a moved directory is not silently uncounted (test bench).

Source map

Status: built · partly tested: the map is checked by reading the source, not by a case

Every file in kernel/src, and each library the kernel links, is documented on one page (or two, where a file serves two mechanisms).

Residual risks

• RustSBI is TCB and outside the ratchet. The firmware runs in M-mode below the kernel. It is vendored at a pinned commit and built with only QEMU virt’s drivers, but its unsafe is not counted, and QEMU loads it outside the signed bundle, so verified boot does not cover it (boot).
• Third-party crates in the TCB are outside the ratchet. The kernel links riscv, sbi-rt, plic and rand_chacha; paging links bitflags; the loader links fdt-rs, elf, tar-no-std, crc, sbi-rt and an Ed25519 verifier. They are pinned by Cargo.lock and are TCB like the rest (TENETS), but no case counts their unsafe.
• The ratchet counts words, not soundness. It checks that a SAFETY: comment is near each unsafe, not that the comment is true, and it counts only the paths its budgets list: a TCB file no budget names is not counted, and the case cannot notice (test bench).
• The table’s inclusive line counts are snapshots. The size budget has separate ceilings for shipped code lines, excluding comments and tests, and fails if a trusted crate grows past its ceiling (the size budget).
• Several harts, one lock. Every hart runs user code, one process’s threads on several harts at once, under one kernel lock (bench:smp-boot, bench:smp-shootdown); completion races between harts are not attacked by a case (IPC). Finer locking is M2 (usable shell)’s later step (several harts).
• The containment gate is one workload. Containment runs hostile leases of one size, against stand-ins for the steward and a driver, at one hart and two and under one pinned seed. It shows that the kernel’s primitives hold together for that workload. It does not bound every workload, and it says nothing about the real steward. The steward reruns the responsiveness measures with its real servers (M3 (agents, approvals and the attack suite)).
• The kernel trusts the loader’s handoff. It reads the argument block through a pointer the loader passed and trusts the memory map in it. It checks the device list itself (no device may overlap RAM or an interrupt controller), and it checks its own mappings are W^X before the first process runs (R19 (kernel W^X)). The loader is TCB for the rest (boot).
• Test builds carry more. The kernel source has features only some bench cases turn on: sched-trace, walk-trace, lock-trace, hold-trace, block-trace, dma-reset-deaf, sum-probe, panic-in-print and smp, and sched-inject-tie-fault for a recorded negative run. A production build leaves them off (R23 (no test channels)); a kernel built with them is not the kernel this page measures.

Why

• Five jobs, because each needs privilege. Page tables, trap entry and the context switch, the stamp on a message’s sender, the one interrupt controller and the one hardware timer can only be done safely by code no process controls. A driver, a file system or a policy can run unprivileged, so it does: a bug there reaches only what its server’s handles reach.
• One call table, no compatibility layer. Two call interfaces are two sets of argument checks to audit and two ways into every object. Redoubt carries one, and bench:no-cruft keeps the tree from growing a second, or dead code, or a feature nothing reads. For the same reason each shared constant has one literal definition.
• No callbacks, no direct switch. A kernel that calls into user code, or hands the CPU from one process straight to another, runs code on a budget the scheduler never picked, and a callback that never returns holds the CPU for ever. With two ways in and one way out, every instruction is charged and every slice ends.
• Count unsafe, not just lines. unsafe is where Rust’s checks stop and a reader’s must start. A ceiling that only goes down, with a written reason beside each use, keeps that part small and said out loud.
• Objects in frames of their own. Each object is one page charged to a budget, so there is no kernel table whose size one budget could exhaust for another, and destroying a budget can free everything it paid for.