The security register

This is where an audit of Redoubt starts. Every security property the book claims is one row below: what it is, the rule that states it, the code that enforces it, the tests that attack it, whether it is built, and what it leaves open. Nothing else is claimed. The rules are defined on the pages that own them; this register is derived from those pages, and the docs checker holds it to them (the test bench). The guarantees the rules add up to, and the walls they rest on, are on the tenets.

How to audit

Start from a guarantee on the tenets: capability closure, label non-interference, human control. Each names the rules it rests on.
Find the rule’s row. The Rule column links the section that defines it; read that section whole. It states the rule, says why, and opens with its status line. For example, R1 (flow) is the kernel’s half of label non-interference, and I7 (every flow obeys R1) is the model’s check of it after every step.
Read the enforcing code. The Enforced in column names the files where the rule is kept. The kernel’s files are small enough to read in full; each cites the rules it keeps.
Read the tests that attack it. A bench: test is tests/<name>.toml: most are a boot under QEMU whose verdict comes from a party the attacker cannot impersonate (rule F), and the rest run a host check and judge its exit status (wire-host-tests, for one, runs host tests; the kinds); a host: test is a Rust test in that crate; a mutation: is the rule deliberately broken in the model, which its checks must catch (the model); a fuzz: test is a fuzz target.
Read what is left open. “Built, partly tested” means the section’s status line names what no test attacks yet; the Residual risks column names what the rule does not stop, and links the page’s full list.

Status reads the same as on the pages (reading this book): built (every claim attacked by the tests listed), built, partly tested (the gap is on the page), or planned for a named milestone, with nothing built yet. Built means the code exists and its named tests pass. A host test or a build case is not a boot: a server whose rows are built from host tests is not thereby running in the integrated system, and running there is its own planned section on its page.

The walls

The rows fall into groups, one per wall of the prison. From outside in: the boot chain that decides what runs, the kernel that separates processes, the servers that separate principals, and the network that is the way out. Four walls are not the OS’s own: they are named, with what rests on them, below.

flowchart TB
    subgraph HOST["host: virtio emulation"]
      BOOT["Boot<br/>verified bundle, confined images, init's checks"]
      subgraph K["Kernel"]
        KI["IPC and objects"]
        KM["memory"]
        KB["budgets, scheduling and time"]
        KP["processes and devices"]
        KV["invariants (the model)"]
      end
      subgraph SV["Servers"]
        SL["the serving library and wire formats"]
        SS["the steward"]
        SK["keys, files and devices"]
        SP["packages and services"]
      end
      NET["Network<br/>netd, ipd, resolver, gatewayd, sshd"]
    end
    HUMAN(["the approval human"])
    OUT(["allowed egress"])
    BOOT --> K
    K --> SV
    SV --> NET
    NET --> OUT
    SS -.-> HUMAN

Figure: the register’s row groups as walls, outermost first. Solid lines are built, dashed lines planned. Side channels cross every box and are listed below.

The register

Property	Rule	Enforced in	Tested by	Status	Residual risks
Kernel: IPC and objects
Information flows between two `user` budgets only if their label sets are equal; `system` budgets check labels themselves	R1 (flow)	`kernel/src/message.rs`, `kernel/src/budget.rs`, `kernel/src/process.rs`	bench:process-attack, bench:process-review, mutation:R1SkipLabelCheck, mutation:R1ChecksReceiverNotOwner, mutation:R1ExitNoticeIgnoresLabels, mutation:R1UsageIgnoresLabels	built, partly tested	System-class servers are trusted to check labels (more)
Blocked senders are served in turns per (account, label set), so one principal cannot crowd out another at an endpoint	R2 (fair waiting)	`kernel/src/endpoint.rs`, `kernel/src/message.rs`	bench:redoubt-ipc, bench:ipc-fair-label-sets, bench:walfsd-flood-turn, bench:vault-flood-turn, bench:blkd-fairness, host:redoubt-model::steward_noninterference, host:redoubt-model::one_cursor_scenario, mutation:R2FifoAcrossAccounts, mutation:R2NoWaitCap, mutation:R2KeyByAccountOnly, mutation:R2KeyByStampLabels, mutation:R2SystemCallersShareGroup, mutation:R2OneCursor	built, partly tested	Turns between groups are attacked on the kernel only as one label set’s order beside a vault’s turn and a served group going behind one already waiting (more)
A lend is the caller’s own writable RAM, unmapped from it while lent, and an abandoned call’s lend stays with the server until it replies	R3 (lends and abandoned calls)	`kernel/src/message.rs`, `kernel/src/arch/riscv/mem.rs`	bench:redoubt-revoke, bench:timeouts, bench:ipc-outcomes, bench:uaf-lent-page, bench:process-lifecycle, bench:endpoint-destroy-open-calls, mutation:R3UnmapAbandonedLend, mutation:R3ChargeStaysWithCaller, mutation:AbandonNoticeMissing, mutation:AbandonNoticeRepeated, mutation:BadRecordConsumesNotice, mutation:EndpointDestroyNoticeKept	built	A server pays for the calls it holds (more)
A message is delivered only if the receiver’s budget can pay for everything it brings	R4 (delivery)	`kernel/src/message.rs`, `kernel/src/handle.rs`	bench:redoubt-ipc, bench:redoubt-dead, bench:redoubt-tight, mutation:R4IgnoreMaxTransfer, mutation:R4OverdrawOnDelivery, mutation:IpcDropPartial	built	`Refused` and `Busy` are signals (more)
An open call costs the receiver a page and counts against its limit of open calls	R4a (open calls)	`kernel/src/message.rs`, `kernel/src/budget.rs`	bench:redoubt-ipc, bench:net-pinned-ssh, mutation:R4aOpenCallsPerThread, mutation:R4aFullTakesNothing	built	A server pays for the calls it holds (more)
A server that dies holding calls gives each caller `Dead` and its lend back intact	R4b (a server dies)	`kernel/src/message.rs`, `kernel/src/process.rs`	bench:redoubt-dead, bench:process-lifecycle, bench:ending-pumps-once, bench:destroy-keeps-notices, bench:destroy-keeps-notices-creator, mutation:R4bDeadServerFakesReply	built	A server pays for the calls it holds until it replies or dies; delivery reads the endpoint’s own lists, never every thread (more)
Every call ends in exactly one outcome, and caller and server agree on it	R13 (one outcome per call)	`kernel/src/message.rs`, `libs/sys/src/ret.rs`	bench:ipc-outcomes, bench:elixir-oracles, mutation:IpcWrongLend, mutation:IpcFalseDelivery, mutation:IpcSkipOutputCheck, mutation:IpcLeakRollback	built, partly tested	Completion races between harts are argued, not attacked (more)
The badge, account and labels a receiver sees are the kernel’s, never the sender’s claim	R14 (unforgeable sender)	`kernel/src/message.rs`	bench:redoubt-ipc, bench:bench-attack-forgery, bench:pid-reuse-authority, mutation:MsgNoLabels, mutation:MsgAccountZero	built, partly tested	A non-zero account or a label set reaching the receiver unchanged is attacked only in the model (more)
Every handle carries a stamp, and destroying that budget or one above it revokes the handle everywhere	R9 (stamps)	`kernel/src/handle.rs`, `kernel/src/budget.rs`	bench:process-attack, bench:redoubt-revoke, bench:budget-deadline, mutation:R9ReceivedHandleRestamped, mutation:R9MintStampsCaller, mutation:R9MsgStampIsSenderBudget, mutation:R10KeepForeignHandles	built, partly tested	Revocation is by budget only; a budget handle cannot be narrowed (more)
Kernel: memory
No RAM page is writable and executable, every page is zeroed, the zeroes cannot be discarded from user mode, no physical address leaks, DMA pages are held until reset, and `map_fixed` never replaces	R11 (memory)	`kernel/src/mem.rs`, `kernel/src/arch/riscv/mem.rs`, `kernel/src/arch/riscv/asm.rs`	bench:wx, bench:write-only-attack, bench:map-fixed-attack, bench:device, bench:mem-attack, bench:process-attack, bench:return-lent-unmapped, bench:dma-rules, bench:dma-reset-reuse, bench:device-exec-refused, bench:cbo-user-fault, bench:smp-inflight-race, mutation:R11NoZeroing, mutation:R11SetFlagsAllowsWx, mutation:R11SetFlagsAllowsWriteOnly, mutation:R11LendStaysMapped, mutation:R11MapFixedSkipsOverlap, mutation:R11ExecOnDeviceMemory, mutation:R11ProcessMapSkipsFlags	built, partly tested	No case ties a reused page it read to the frame another process filled (more)
A freed frame is no process’s and not free until it is zeroed, by the hart that freed it or by an allocation, one hart at a time, after every hart that could store to it has flushed; every free frame is zero	R81 (frames in flight)	`kernel/src/reclaim.rs`, `kernel/src/mem.rs`, `kernel/src/arch/riscv/irq.rs`	bench:smp-inflight-race, mutation:R81InFlightAllocatable, mutation:R81CommitUnzeroed	built, partly tested	QEMU drops stale translations at a hart’s next `satp` write, so the order that keeps a stale store out is checked from the trace (more)
The kernel’s own mappings are never writable and executable	R19 (kernel W^X)	`loader/src/paging.rs`, `kernel/src/arch/riscv/mem.rs`, `libs/paging/src/lib.rs`	bench:kernel-wx	built, partly tested	The physmap maps every user frame writable for the kernel (more)
A range call costs what the page tables need and the budget can pay, never what the length asks	R22 (range cost)	`kernel/src/mem.rs`, `kernel/src/arch/riscv/mem.rs`	bench:map-fixed-attack, bench:map-anon-search-bound, host:redoubt-model::huge_len_is_refused_promptly	built	`map_anon`’s search is bounded by its area, not by what is mapped: about 9.6 ms at worst (more)
The kernel keeps `sstatus.SUM` and `sstatus.MXR` clear	R24 (SUM and MXR clear)	`kernel/src/arch/riscv/asm.rs`, `kernel/src/arch/riscv/mod.rs`	bench:sum-clear	built, partly tested	No probe covers `MXR` (more)
Kernel: budgets, scheduling and time
Every kernel object is charged to one budget, and a charge over the limit fails before anything changes	R6 (charging)	`kernel/src/budget.rs`	bench:budget, bench:budget-mem-churn, bench:budget-table-attack, bench:map-fixed-tables, bench:page-table-reclaim, bench:pages-exhaustion, bench:redoubt-tight, bench:process-attack, bench:pid-pinning-attack, bench:thread-limit, mutation:R6ChargeAncestors, mutation:R6OwnPageChargedToItself, mutation:R6EndpointsFree, mutation:R6PageTablesFree, mutation:R6EmptyTableKept, mutation:R6OpenCallsFree, mutation:R6ProcessObjectFree, mutation:R6ProcessObjectChargedToBudget, mutation:R6LendChargedOnce, mutation:R6RootPageUncounted, mutation:R6PidUncountedAtEnd	built, partly tested	An endpoint’s page charge is attacked only in the model (more)
A child’s limits come out of its parent’s free limits and never add up to more	R7 (carving)	`kernel/src/budget.rs`	bench:budget-carve-attack, bench:budget, bench:process-attack, bench:pid-pinning-attack, host:redoubt-model::budget_lifecycles, mutation:R7NoCarveCheck, mutation:R7CarveToZeroFree, mutation:ProcessInWeightlessBudget	built	A lost budget stays carved until its parent goes (more)
A budget’s account is inherited and cannot be changed by the budget’s holder	R8 (accounts)	`kernel/src/budget.rs`	bench:process-attack, mutation:R8AccountFromArgument	built	Usage reads are signals (more)
Destroying a budget destroys everything below it, in a fixed order, and returns its resources to its parent; a reap does so for one child and keeps the budget	R10 (destruction)	`kernel/src/budget.rs`, `kernel/src/time.rs`	bench:budget, bench:budget-destroy-attack, bench:budget-destroy-kills, bench:budget-destroy-growth, bench:budget-deadline, bench:deadline-flood-billed, bench:redoubt-revoke, bench:process-attack, bench:pid-pinning-attack, bench:endpoint-destroy-open-calls, bench:endpoint-destroy-full, bench:handle-chain-attack, bench:handle-chain-fault, bench:process-chain-fault, bench:sched-destroy-billing, bench:dma-reset-quarantine, bench:dma-destroy-quarantine, bench:budget-reap, host:redoubt-model::budget_lifecycles, host:redoubt-model::quarantine_charge_moves_to_a_parent_at_its_limit, host:redoubt-model::a_reap_destroys_one_child_and_keeps_the_budget, host:redoubt-model::a_destruction_delivers_at_its_end, mutation:R10KeepForeignHandles, mutation:R10KeepCarvedLimits, mutation:R10SpareDescendantProcesses, mutation:R10ExitNoticesOutlivePayer, mutation:R10RevokedMessageDelivered, mutation:R10RevokedCallAnswered, mutation:R10SweptHandlesDropped, mutation:R10CreatorDeathSparesProcess, mutation:R10HeldPidsDropped, mutation:R10ReapDestroysParent, mutation:R10ReapKeepsCarve, mutation:R10ReapSkipsGrandchildren, mutation:R10DeliveredMidDestruction, mutation:ExpireBudgetsFirst, mutation:BudgetDeadlineIgnored	built, partly tested	Destruction is uninterruptible kernel time; a process entering the kernel in a tight loop to put its deadline off is not attacked (the timer’s part, more)
A budget’s CPU follows its free weight, in one queue with no priority	R12 (scheduling)	`kernel/src/sched.rs`, `libs/stride/src/lib.rs`	bench:sched-share, bench:steward-latency, bench:steward-latency-n4, bench:steward-latency-n16, bench:sched-share-release, bench:sched-capped, bench:sched-capped-mttcg, bench:sched-capped-holds-floor, bench:sched-sleep-gaming, bench:sched-idle-gap, bench:sched-exit-churn, bench:sched-budget-churn, bench:sched-budget-churn-shell, bench:sched-carve-inflation, bench:sched-debt-lift, bench:sched-lift-delay, bench:sched-timer-flood, bench:sched-server-busy, bench:sched-large-weight, bench:sched-large-weight-release, bench:deadline-flood-billed, bench:deadline-flood-billed-traced, bench:deadline-flood-billed-traced-mttcg, bench:sched-exit-churn-mttcg, bench:deadline-placement, bench:sched-carve-return, bench:map-anon-search-bound, bench:scan-bounds, bench:call-bounds, bench:worst-walk, host:redoubt-stride::the_crate_and_the_model_agree, host:redoubt-stride::a_broken_model_disagrees, host:redoubt-stride::a_slice_end_reads_no_more_states_for_a_longer_queue, host:redoubt-stride::a_rank_out_of_step_with_its_frame_trips_the_audit, host:redoubt-model::scheduler_fairness, host:redoubt-model::scheduler_contracts_hold, mutation:R12PriorityById, mutation:R12IgnoreWeight, mutation:R12WakeBanksCredit, mutation:R12TieQueuedFirst, mutation:R12RequeueAhead, mutation:R12RequeueLifo, mutation:R12PreemptOnWake, mutation:R12TimeoutWakePreempts, mutation:R12NoFloorWhenIdle, mutation:R12ShortRunsFree, mutation:R12DropRemainder, mutation:R12ExitRunsFree, mutation:R12DestroyDropsDebt, mutation:R12CreateAtFloorOnly, mutation:R12LiftByMax, mutation:R12StrideWeightIsLimit, mutation:R12UnnormalizedLift, mutation:R12LiftCountsEntryWait, mutation:R12FoldAtNewWeight, mutation:R12NoMinimumCharge, mutation:R12DeadlineWorkUnbilled, mutation:R12RescaleOnlyOnReturn, mutation:R12SliceCountsExitWork, mutation:R12TimerWorkUnbilled, mutation:R12SwitchBilledToPrevious, mutation:R12CappedHoldsFloor, mutation:R12CapOnce, mutation:R12AllCappedHoldsFloor, mutation:R12UncapBanksCredit, mutation:R12UncapForfeitsWait, mutation:R12EmptyHoldsFloor, mutation:R12RequeueWaitsForCap, mutation:R12BlockLeavesAsRequeued, mutation:R12OneRunnerPerBudget, mutation:R12SpreadChargesOnce	built, partly tested	Server work is paid by the server’s weight; wakeup is prompt but not bounded, and the steward decision-wake target is missed on rv64 (the timer’s part, more)
On several harts, a hart waits for kernel entry behind at most `MAX_HARTS` - 1 kernel sections: the kernel lock is FIFO, so no budget’s harts can starve another’s of the kernel	R78 (fair kernel entry)	`kernel/src/cell.rs`	bench:smp-boot, bench:smp-lock-wait, bench:sched-lock-contention, bench:sched-lock-contention-4, bench:sched-lock-contention-4-mttcg, bench:irq-boot-hart-only, host:testbench::lock_waits_take_the_lock_in_ticket_order	built	The bound is by hart count, not time; a long kernel section delays every waiting hart by its length, and at two harts a wake behind R12’s costliest call waits about two of its sections (more)
The production kernel carries no test-only diagnostic channel	R23 (no test channels)	`kernel/src/sched.rs`, `kernel/Cargo.toml`	bench:bench-no-trace, bench:bench-trace-scan-catches, bench:bench-test-only-refused	built	Test builds carry more (more)
Kernel: processes and devices
A reused PID inherits nothing of the process that had it	R20 (PID reuse)	`kernel/src/process.rs`	bench:pid-reuse-authority, bench:process-attack, bench:process-lifecycle, host:redoubt-model::pid_reuse_only_after_notice_receipt	built	PIDs are one global pool held by untaken notices (more)
A crash blames the sender of the current call, or nobody	R21 (crash blame)	`kernel/src/process.rs`, `kernel/src/message.rs`	bench:process, bench:process-attack, mutation:BlameNobody, mutation:BlameNewestCall, mutation:ExitWithOpenCallsNotFaulted, mutation:CurrentNeverSet, mutation:ReceiveKeepsCurrent, mutation:ServeIgnored, mutation:ExitEndpointBadged	built, partly tested	Delayed corruption can misattribute blame; a crash with no current call blames nobody (more)
An interrupt is masked and flagged, and reaches only the holder of its IRQ object	R5 (interrupts)	`kernel/src/device.rs`, `kernel/src/arch/riscv/irq.rs`, `kernel/src/arch/riscv/intc_plic.rs`	bench:uart-irq, bench:sched-irq-wake, bench:irq-first-receive, bench:receive-bad-record, mutation:R5NoMaskOnFire, mutation:R5NoUnmaskOnReceive, mutation:R5BadRecordConsumesInterrupt	built, partly tested	Two parts are not attacked on QEMU: the mask is attacked in the model, the completion order argued; the billing is attacked by bench:sched-irq-wake (owner `system`, whoever holds the handle) (more)
A process reaches a device only through a device object it was given	R18 (device authority)	`kernel/src/device.rs`, `loader/src/main.rs`, `kernel/src/main.rs`	bench:irq-attack, bench:legacy-gone, bench:device-info-attack	built, partly tested	A DMA driver is trusted without an IOMMU; one early process holds all device authority; a co-holder keeps its mapping of a quarantined or revoked device; a device tree that hides a controller defeats the `Ctrl` check (more)
Kernel: invariants
Handles name live objects: a process names objects only through its own handle table	I1 (handles name live objects)	`kernel/src/handle.rs`	bench:budget-forge-attack, bench:budget-destroy-attack, bench:process, host:redoubt-model::exited_object_handles_and_queued_copies_live_until_notice_receipt, host:redoubt-model::kernel_sequences	built	A stale handle stops the machine (more)
Revocation is complete: no handle below a destroyed budget can be used anywhere	I2 (revocation is complete)	`kernel/src/budget.rs`, `kernel/src/handle.rs`, `kernel/src/message.rs`	bench:budget-destroy-attack, bench:handle-chain-attack, bench:handle-chain-fault, bench:process-chain-fault, bench:redoubt-revoke, bench:budget-deadline, bench:process-attack, mutation:R10KeepForeignHandles, host:redoubt-rt::badges_are_never_reused_and_ids_are_never_zero	built	Revocation is by budget only (more)
Minted badges are non-zero, and a mint never widens its source’s stamp	I3 (minted badges are non-zero and narrow)	`kernel/src/message.rs`	bench:redoubt-ipc-attack, bench:redoubt-revoke, bench:redoubt-ipc, host:redoubt-sys::malformed_calls_are_refused, mutation:R9MintStampsCaller	built	The model checks its own abstraction (more)
Only badge-0 handles receive	I4 (only badge-0 handles receive)	`kernel/src/message.rs`	bench:redoubt-ipc-attack, bench:redoubt-ipc, bench:process-attack, mutation:ReceiveWithBadgedHandle, mutation:ExitEndpointBadged	built	The model checks its own abstraction (more)
Every budget’s usage is within its limits	I5 (usage within limits)	`kernel/src/budget.rs`, `kernel/src/dma.rs`	bench:budget, bench:budget-carve-attack, bench:redoubt-tight, host:redoubt-model::quarantine_charge_moves_to_a_parent_at_its_limit, mutation:R4OverdrawOnDelivery, mutation:R7NoCarveCheck	built	Quarantined DMA pages stay charged (more)
A budget’s labels never change, and a child carries all its parent’s	I6 (labels only grow downward)	`kernel/src/budget.rs`	bench:budget, bench:process-attack, mutation:LabelsAddedByParentClass	built	Adding a label needs a `system`-class caller (more)
Every flow the kernel carries obeys the flow rule	I7	`kernel/src/message.rs`, `kernel/src/budget.rs`	bench:process-attack, bench:process-review, mutation:R1SkipLabelCheck, mutation:R1ChecksReceiverNotOwner, mutation:R1ExitNoticeIgnoresLabels, mutation:R1UsageIgnoresLabels, mutation:R1UsageExemptBySystemTarget, mutation:R1ExitExemptBySystemExiting	built, partly tested	System-class servers are trusted to keep it (more)
A child budget inherits its parent’s class and account	I8 (class and account inherited)	`kernel/src/budget.rs`	bench:process-attack, mutation:ClassNotInherited, mutation:R8AccountFromArgument	built	The model checks its own abstraction (more)
User pages are W^X, zeroed before reuse, and unmapped from the lender while lent	I9 (pages W^X, zeroed, lends unmapped)	`kernel/src/mem.rs`, `kernel/src/arch/riscv/mem.rs`	bench:wx, bench:write-only-attack, bench:mem-attack, bench:map-fixed-attack, bench:return-lent-unmapped, bench:lender-touches-lent, bench:uaf-lent-page, bench:device-exec-refused, bench:smp-inflight-race, mutation:R11NoZeroing, mutation:R11SetFlagsAllowsWx, mutation:R11SetFlagsAllowsWriteOnly, mutation:R11LendStaysMapped, mutation:R11ExecOnDeviceMemory	built, partly tested	No case ties a reused page it read to the frame another process filled (more)
Creating then destroying a budget leaves its parent unchanged, once notices are taken	I10 (create-destroy leaves the parent unchanged)	`kernel/src/budget.rs`, `kernel/src/process.rs`	bench:budget, bench:budget-deadline, bench:process-lifecycle, bench:process-attack, host:redoubt-model::budget_lifecycles, mutation:R10KeepCarvedLimits	built	The invariant waits for the exit notices (more)
Each group of blocked senders gets a turn within k receives	I11 (fair turns)	`kernel/src/endpoint.rs`, `kernel/src/message.rs`	host:redoubt-model::flood, host:redoubt-model::kernel_sequences, bench:ipc-fair-label-sets, mutation:R2FifoAcrossAccounts, mutation:R2OneCursor	built, partly tested	Turns between groups are attacked on the kernel only as one label set’s order beside a vault’s turn and a served group going behind one already waiting (more)
Object ids are never reused	I12 (ids never reused)	`kernel/src/budget.rs`	bench:redoubt-ipc, bench:redoubt-ipc-attack, mutation:MsgIdsGlobal	built, partly tested	Id reuse is attacked only in the model (more)
Every blocking call returns by its timeout	I13 (every blocking call returns by its timeout)	`kernel/src/time.rs`, `kernel/src/message.rs`	bench:timeouts, bench:timeouts-tcg, bench:sched-latency, bench:sched-wake-no-preempt, host:redoubt-model::kernel_sequences, mutation:TimeoutIgnoredWhileOthersRun	built, partly tested	The invariant bounds the commit, not the run; the timer’s own cases for it are on the timer (more)
No sequence of calls, with any arguments, panics the kernel	I14 (no call panics the kernel)	`kernel/src/redoubt.rs`	bench:budget-syscall-attack, bench:syscall-attack, bench:redoubt-tight, bench:pages-exhaustion, host:redoubt-sys::malformed_calls_are_refused, fuzz:redoubt-sys/decode, host:redoubt-model::kernel_sequences	built	A kernel bookkeeping bug is a stop (more)
Every abandoned call is reported exactly once and stays open until replied to	I15 (abandoned calls reported once)	`kernel/src/message.rs`	bench:redoubt-ipc, bench:timeouts, bench:budget-deadline, bench:process-lifecycle, bench:ending-pumps-once, bench:receive-bad-record, bench:endpoint-destroy-open-calls, mutation:AbandonNoticeMissing, mutation:AbandonNoticeRepeated, mutation:BadRecordConsumesNotice, mutation:EndpointDestroyNoticeKept	built	A server pays for the calls it holds, abandoned ones too, until it replies (more)
DMA pages return to the pool only after every device that could write them confirmed a reset	I16 (DMA pages reset before reuse)	`kernel/src/dma.rs`	bench:dma-reset-reuse, bench:dma-reset-quarantine, bench:dma-destroy-quarantine, bench:dma-rules, host:redoubt-model::reset_at_one_death_does_not_cover_a_co_holder, host:redoubt-model::deaf_device_quarantines_the_co_holder_too, host:redoubt-model::exit_pools_after_reset, mutation:DmaFreeBeforeReset, mutation:DmaQuarantinedSlotCountsAsReset, mutation:DmaResetClearsCoHolderReach, mutation:DmaUnmapFrees	built, partly tested	The reset covers reuse, not a live driver (more)
Boot
No byte of the bundle is parsed or run before its signature checks	R15 (verified boot)	`loader/src/verify.rs`, `libs/signing/src/lib.rs`	bench:verified-boot-rejects-tamper, bench:verified-boot-rejects-bare-archive, bench:verified-boot-rejects-short-initrd, host:testbench::golden_signature_over_a_known_archive	built	The loader itself is unverified on QEMU; the development key is public; no rollback protection (more)
A module or application resource resolved by name, or a program launched from the userland disk, comes only from a verified volume (R76 (verified volumes)); a refused lookup never falls through to the code path	R75 (verified userland)	`image/manifest.json`, `userland/otp/redoubt/src/userland.rs`, `userland/otp/redoubt/src/pack.rs`, `userland/otp/redoubt/src/lib.rs`, `userland/otp/redoubt/src/bin/beamlet.rs`, `userland/otp/vm/src/vm.rs`, `userland/otp/vm/src/bif/info.rs`	bench:userland-bad-start, bench:userland-boot, bench:userland-read-only, bench:verity-flipped-tree, bench:verity-wrong-root, bench:pack-bad-truncated, bench:pack-bad-wrong-length, bench:pack-bad-wrong-name, host:beamlet-redoubt::a_pack_with_a_bad_entry_is_refused_whole, host:beamlet-vm::a_refused_system_module_never_touches_the_code_path, host:beamlet-vm::app_spec_uses_one_source_attempt_and_keeps_its_erlang_result, host:beamlet-redoubt::a_module_is_its_file_and_a_failed_read_is_refused, host:beamlet-redoubt::not_found_at_the_open_is_absent_and_every_other_error_is_refused_by_name, host:beamlet-redoubt::verified_module_lookup_propagates_found_absent_and_refused, host:beamlet-redoubt::verified_application_lookup_propagates_found_absent_and_refused	built, partly tested	Programs come from the volume when launching exists (BEAM4); `code:load_binary/3` still loads a session’s own bytes, within its authority (more)
The loader confines every image to its own area and refuses a truncated one	R16 (image confinement)	`loader/src/image.rs`	bench:loader-rejects-kernel-address, bench:loader-rejects-kernel-entry, bench:loader-rejects-truncated-elf, bench:loader-rejects-segment-data-cut, bench:loader-rejects-wx-segment	built	The kernel trusts the loader’s handoff (more)
A bad signature, a short random seed or a missing timebase powers the machine off	R17 (fail closed)	`loader/src/main.rs`, `loader/src/dt.rs`, `kernel/src/arch/riscv/timer_sbi.rs`, `kernel/src/platform/sbi/rand.rs`, `kernel/src/arch/riscv/process.rs`	bench:verified-boot-rejects-tamper, bench:verified-boot-rejects-bare-archive, bench:verified-boot-rejects-short-initrd, bench:boot-rejects-no-seed, bench:boot-rejects-short-seed, bench:boot-rejects-no-timebase, bench:boot-rejects-irq-past-plic, host:redoubt-layout::ram_one_page_past_the_physmap_end_is_refused, host:loader::a_boot_hart_without_an_s_mode_context_is_refused, host:loader::booting_on_hart_1_takes_hart_1s_s_mode_context, host:loader::a_33rd_mmio_region_is_refused, host:loader::a_33rd_interrupt_is_refused, host:loader::thirty_two_devices_are_kept, host:loader::an_interrupt_two_devices_raise_takes_one_slot, host:paging::the_asid_width_decision	built, partly tested	The kernel’s refusal of a missing `Seed` tag stands behind the loader’s and is not reached by a boot; the device tree is not signed (more)
A program runs only with a startup block that passed every rule	R31 (startup block checked whole)	`libs/rt/src/startup.rs`	bench:rt-host-tests, bench:session-hostile-launch, host:redoubt-rt::hostile_blocks_are_refused, host:redoubt-rt::fields_hold_whole_entries, host:redoubt-rt::handle_names_follow_the_manifest_rule, host:redoubt-rt::image_round_trips_and_is_validated, host:redoubt-rt::handle_counts_are_what_process_start_can_install, host:redoubt-rt::random_bytes_never_panic, fuzz:redoubt-rt/startup	built	The startup block’s fuzz target runs outside the bench (more)
No launcher parses an ELF; a hostile image hurts only its own process	R32 (a hostile image hurts only its process)	`stub/src/main.rs`, `stub/src/lib.rs`	bench:stub-launch, bench:session-hostile-launch, host:stub::plan_refuses_a_segment_overlapping_an_excluded_range, host:stub::plan_refuses_writable_and_executable, host:stub::plan_refuses_two_segments_that_overlap_each_other, host:stub::plan_refuses_a_segment_touching_page_zero, host:stub::plan_refuses_a_segment_reaching_into_the_stub_region, host:stub::image_in_bounds_refuses_an_image_overlapping_the_stub, host:stub::read_image_refuses_an_image_len_over_the_cap, host:stub::plan_refuses_a_segment_over_its_own_image, host:stub::the_fuzz_corpus_still_passes	built, partly tested	On target, the kernel’s refusal hides the stub’s overlap checks (more)
Only `init` and the steward ever hold a `system`-class budget	R33 (no server holds a system budget)	`servers/init/src/check.rs`; the policy is modelled in `model/src/steward.rs`	bench:init-refuses-budget-handle, host:redoubt-init::a_server_handed_a_budget_is_refused, bench:steward-boot	built	A system server that hands one across is at fault, not the kernel (more)
In a confined deployment no two label sets share a server, volume, endpoint, network or device, except the named control plane	R34 (confined placement)	`servers/init/src/confine.rs`, `servers/steward/src/own.rs`	bench:init-refuses-confined-server, bench:steward-confined-push, host:redoubt-init::confined_refuses_two_label_sets_on_one_endpoint, host:redoubt-init::confined_refuses_two_label_sets_on_one_volume, host:redoubt-init::confined_counts_a_home_for_the_principals_unlabelled_domain_alone, host:redoubt-init::the_steward_is_told_a_confined_manifest, host:redoubt-steward-server::a_confined_boot_leaves_a_labelled_sessions_home_unbound, host:redoubt-init::confined_gives_a_labelled_domain_no_network, host:redoubt-init::confined_refuses_two_label_sets_on_one_disk, host:redoubt-init::confined_refuses_a_server_instance_serving_two_label_sets, host:redoubt-init::confined_counts_only_a_shared_servers_own_label_set, host:redoubt-init::confined_does_not_count_an_exempt_server_handed_a_labelled_endpoint, host:redoubt-init::confined_lets_label_sets_that_share_nothing_share_the_cores, host:redoubt-init::confined_gives_each_label_set_its_own_userland_disk, host:redoubt-init::confined_gives_each_label_set_its_own_verifier	built	The named mediators are trusted across the labels they serve; a confined boot is checked once (more)
`keyd` never holds a key that authenticates anyone to the box	R35 (key separation)	`servers/init/src/check.rs`, `servers/init/src/bin/init.rs`; the policy is modelled in `model/src/steward.rs`	bench:init-refuses-held-login-key, bench:init-refuses-held-bundle-key, bench:init-refuses-second-keyd, host:redoubt-init::every_login_and_approval_key_then_the_bundle_key_is_asked_about, host:redoubt-init::init_calls_one_of_each_server_it_calls	built	The seeds live in `init`’s memory and the bundle (more)
The loader refuses a system bundle older than the counter outside both slots	R72 (no rollback below the counter)	planned: the loader	—	planned · M6 (persist, install, share)	A resettable counter undoes rollback protection (more)
Servers: the serving library and wire formats
A shared server lets data flow to a caller only from objects whose labels it holds, and into objects only with equal labels	R25 (the label check)	`libs/rt/src/server/label.rs`, `libs/rt/src/server/ninep.rs`	host:redoubt-rt::matches_the_set_definition, host:redoubt-rt::properties, host:redoubt-rt::labels_are_checked_on_every_request, host:redoubt-rt::every_write_needs_equal_labels, host:redoubt-rt::labelled_metadata_does_not_flow_down, host:redoubt-rt::an_unlabelled_caller_cannot_reach_labelled_data_to_destroy_or_probe_it, host:redoubt-rt::a_mint_at_its_own_root_reads_nothing, bench:net-attacks, bench:littlefsd-label-check, bench:steward-agent-escape	built	System servers are trusted to apply it (more)
One client cannot use up a shared server that serves others	R26 (admission fairness)	`libs/rt/src/server/admit.rs`, `libs/rt/src/server/minted.rs`	bench:walfsd-flood-turn, bench:vault-flood-turn, bench:walfsd-pools, bench:lease-code-load, bench:session-tcp-churn, host:redoubt-rt::the_key_is_the_account_and_the_label_set, host:redoubt-rt::an_agent_flooding_a_bucket_leaves_its_sponsor_a_share, host:redoubt-rt::a_root_fid_is_a_fixed_cost_outside_the_share, host:testbench::the_file_servers_fid_caps_leave_every_connection_its_root_and_working_share, host:redoubt-client::an_admission_refusal_of_the_moment_is_tried_again, host:redoubt-rt::an_agent_flooding_a_bucket_leaves_its_sponsor_a_share_and_its_lease_end, host:redoubt-rt::self_minting_does_not_multiply_the_share, host:redoubt-rt::a_connection_minted_for_another_account_is_admitted_there_from_its_first_request, host:redoubt-rt::a_first_request_on_a_connection_its_account_cannot_hold_is_refused_and_it_stays_pending, host:redoubt-rt::an_account_0_chain_holds_one_bucket, host:redoubt-rt::an_account_0_rooted_chain_holds_one_bucket, host:redoubt-rt::caps_are_big_enough_for_a_share_to_mean_anything, host:redoubt-rt::open_calls_leave_headroom, host:redoubt-rt::the_worst_order_never_passes_the_headroom, host:redoubt-rt::a_bucket_count_is_given_once_and_never_defaulted, host:redoubt-bootfsd::a_bad_public_list_stops_the_server, host:redoubt-consoled::a_console_with_no_device_does_not_start, host:redoubt-keyd::bad_key_arguments_stop_keyd_starting, host:redoubt-ipd::every_scope_and_the_milestone_parse, host:redoubt-ipd::a_heap_that_cannot_hold_every_socket_stops_ipd	built, partly tested	An undersized server is a channel (more)
A server never gives out one badge twice, across restarts too	R27 (badge allocation)	`libs/rt/src/server/minted.rs`	host:redoubt-rt::the_first_badge_is_random_and_leaves_room, host:redoubt-rt::badges_are_never_reused_and_ids_are_never_zero, host:redoubt-rt::the_badge_space_runs_out_cleanly, host:redoubt-rt::a_mint_that_fails_records_nothing	built	Two runs share a badge with probability 2^-62 (more)
A parked call holds exactly one admission slot of its caller until it is resumed, expires or is abandoned	R28 (parked-call accounting)	`libs/rt/src/server/parked.rs`	host:redoubt-rt::parking_is_admitted_per_bucket_and_share, host:redoubt-rt::parked_calls_are_served_abandoned_and_expired, host:redoubt-rt::a_waiting_write_is_parked_abandoned_and_expired, bench:net-pinned, bench:net-pinned-ssh	built, partly tested	A console read has no deadline (more)
A client holds no more of a server through a multiplexed connection than one share, however many requests it sends or completions it leaves uncollected	R77 (multiplexed requests)	`libs/rt/src/server/ninep_mux.rs`	host:redoubt-rt::a_never_polling_client_holds_only_its_share, host:redoubt-rt::a_sends_pages_count_once_and_go_back_with_its_last_request, host:redoubt-rt::death_with_requests_parked_frees_the_connection, host:redoubt-rt::a_death_between_completion_calls_is_found_at_the_session_bound, host:redoubt-rt::a_request_late_in_a_hold_leaves_the_session_its_whole_bound, host:redoubt-rt::a_flush_racing_a_completion_answers_once, host:redoubt-rt::a_flood_of_sends_at_wait_cap_never_blocks_the_server, host:redoubt-rt::a_reused_or_out_of_range_tag_ends_the_connection, host:redoubt-rt::a_second_completion_call_is_refused	built, partly tested	A console read has no deadline (more)
Decoding untrusted bytes never panics, never reads outside its input, and re-encodes exactly	R29 (strict decoding)	`libs/wire/src/codec.rs`, `libs/wire/src/ninep.rs`, `libs/wire/src/json.rs`	fuzz:redoubt-wire/ninep, fuzz:redoubt-wire/typed, fuzz:redoubt-wire/json, host:redoubt-wire::lengths_are_bounded_by_the_input, host:redoubt-wire::framing_is_strict, host:redoubt-wire::trailing_and_padding, host:redoubt-wire::words_must_fit_in_32_bits, host:redoubt-wire::buffer_length_is_bounded, host:redoubt-wire::heap_is_bounded, host:redoubt-wire::stack_is_bounded	built	The fuzz targets run outside the bench (more)
Each typed message has one layout, from one table, with generated codecs checked against it	R30 (one layout per message)	`libs/wire/src/typed.rs`, `libs/wire/tables`	host:redoubt-wire-gen::generated_files_are_current, host:redoubt-wire-gen::refuses_bad_tables, host:redoubt-wire-gen::every_row_is_read_or_refused, host:redoubt-wire-gen::malformed_is_code_one_everywhere, host:redoubt-wire-gen::ninep_marker_sets_the_opcode_floor, bench:wire-host-tests	built	Handle kinds are not checked on receipt (more)
Servers: the steward
Every id the steward hands out is unpredictable	R36 (unpredictable ids)	`libs/steward/src/machines.rs` (the core draws every id from the random words), `servers/steward/src/drive.rs` (the server’s words, top bit set); modelled in `model/src/steward.rs`	bench:steward-session-ends, bench:vault-no-leak, host:redoubt-steward-server::a_login_runs_the_session_batch_and_answers_the_session	built	Ids are only as unpredictable as the generator’s key (more)
A vault session’s work changes nothing an unlabelled session observes	R37 (vault non-interference)	`libs/steward/src/machines.rs` (each session carved from its label set’s fixed sub-budget), `servers/steward/src/lib.rs` (the carve), `servers/steward/src/bin/steward.rs` (the binding table), `libs/steward/src/guards.rs` (sees: a session’s contexts are its domain’s); modelled in `model/src/steward.rs`	bench:steward-vault-session, bench:steward-sub-budget-flood, bench:vault-flood-turn, bench:vault-no-leak, bench:shell-contexts, host:redoubt-steward-server::a_vault_login_carves_from_the_vault_s_sub_budget_and_has_no_network, host:redoubt-steward::a_session_sees_and_ends_its_own_domain_s_contexts_only, host:redoubt-steward-server::a_session_lists_detaches_and_ends_its_own_domain_s_contexts	built	The mediators are trusted across labels; a shared server’s own crash shows whose call it was serving, unless confined (more)
An approval counts only from `approve@box`, with the approver’s key, for the frozen request	R38 (out-of-band approval)	`libs/steward/src/guards.rs` (approval_key, owns_labels, rendered_here, hash_matches, pending_cap, fair_share), `libs/steward/src/effects.rs` (notify, render, drop_requests), `libs/steward/src/edges.rs` (approval), `libs/steward/src/render.rs` (screen, sanitize), `servers/steward/src/protocol.rs` (the principal from the key, the code), `servers/steward/src/drive.rs` (compose, hash_of_code), `servers/steward/src/approval.rs` (parse, Lines), `servers/steward/src/bin/steward.rs` (reader_thread, read_channel), `servers/sshd/src/bin/sshd.rs` (approve); modelled in `model/src/steward.rs`	bench:steward-approve-box, bench:steward-screen-inert, bench:steward-pending-cap, host:redoubt-steward-server::a_request_is_rendered_bound_to_its_screen_and_its_approval_starts_the_labelled_agent, host:redoubt-steward-server::an_approval_channel_opens_on_the_approval_key_alone, mutation:PolicyApproveIgnoresHash, mutation:PolicyApproveWithLoginKey, mutation:PolicyApproveOtherChannel, mutation:PolicyRenderNotWhitelisted, mutation:PolicyLabelledFreeTextShown, mutation:PolicyNotifyLabelledToAll, mutation:PolicyShowLabelledToAll, bench:steward-vault-note	built, partly tested	An approved text can carry a hidden message; `approve@box` shares `sshd` (more)
Every lease has a bounded deadline, sub-agents end with it, and the sponsor can always end it	R39 (leases end)	`libs/steward/src/guards.rs` (lease_bounded, sponsor_session, sponsor_of, sponsor_set), `libs/steward/src/effects.rs` (carve_lease, carve_session: a sponsored principal’s session under its sponsor’s with a deadline, notify_sponsor), `libs/steward/src/edges.rs` (end_lease, ahead of admission), `servers/steward/src/drive.rs` (the batches, the notice), `servers/steward/src/bin/steward.rs` (the lease’s launch, the notices endpoint); modelled in `model/src/steward.rs`	bench:steward-lease-ends, bench:steward-end-lease, bench:steward-sub-agent-dies-with-agent, bench:agent-login, host:redoubt-steward::a_sponsored_principals_session_is_a_lease_of_its_sponsors, mutation:PolicyUnboundedLease, mutation:PolicyEndLeaseFromVault, mutation:PolicySponsoredEndedByAnyone, mutation:PolicySponsoredVaultLogin, bench:steward-agent-escape, bench:steward-lease-cut	built	Steward work is paid by the steward (more)
Crash blame ends only the blamed (account, label set)’s sessions, and only after three crashes in ten minutes	R40 (blame by label set)	`libs/steward/src/guards.rs` (blame_window, not_locked), `libs/steward/src/effects.rs` (lock_out), `servers/steward/src/protocol.rs` (blame), `servers/init/src/blame.rs`, `servers/init/src/reconnect.rs` and `servers/steward/src/drive.rs` (reconnected, rebind: the restarted server’s sessions get their files back, so the count reaches three); modelled in `model/src/steward.rs`	bench:steward-blame-lockout, bench:steward-server-restart, host:redoubt-steward-server::three_blames_in_the_window_lock_the_domain_out_until_the_window_passes, host:redoubt-steward::blame_window_and_not_locked, host:redoubt-steward::a_leases_exit_is_its_end_and_no_blame, mutation:PolicyBlameNoWindow, mutation:PolicyNoLockout	built	Blame follows the current call; the vault arm and the window’s end are host tests; a lease’s connections at a restarted server stay dead (more)
A connection narrowed to a session’s life hangs on a revocation scope, never on a budget with processes	R41 (narrowing by revocation scope)	`libs/rt/src/server/ninep.rs` (new_connection’s and grant’s scope stamps the mint), `libs/rt/src/client.rs`, `servers/ipd/src/server.rs` (grant’s revocation scope), `servers/steward/src/drive.rs` (every Connect in the object’s scope, every shared server’s connection, 9P and the network alike; destroy, then disconnect), `servers/init/src/bin/init.rs` (the steward’s badges stamped users); modelled in `model/src/steward.rs`	host:redoubt-rt::a_connection_minted_in_a_scope_ends_when_the_scope_is_destroyed, host:redoubt-rt::a_connection_is_minted_in_the_scope_its_requester_sends, host:redoubt-ipd::a_granted_connection_in_a_scope_ends_when_the_scope_is_destroyed, host:redoubt-ipd::a_grant_is_minted_in_the_revocation_scope_it_brings, host:redoubt-steward-server::a_session_s_end_destroys_its_budget_before_it_releases_its_connections, host:redoubt-init::the_steward_s_entry_alone_is_given_the_manifest_lines, bench:steward-agent-escape, bench:steward-lease-cut	built, partly tested	none
Data crosses a label only as one owner-approved item, snapshotted and audited	R42 (one approved item)	`libs/steward/src/effects.rs`, `libs/steward/src/guards.rs`, `servers/steward/src/drive.rs`, `servers/crossing/src`	bench:steward-declassify, bench:steward-push, host:redoubt-steward-server::a_declassification_reads_through_a_crossing_and_its_approval_copies_the_snapshot_out, host:redoubt-steward-server::a_push_reads_the_source_unlabelled_and_its_approval_writes_through_a_crossing, host:redoubt-crossing::an_item_over_the_bound_is_cut_one_past_declassify_max, mutation:PolicyDeclassifyLive, mutation:PolicyDeclassifyWithoutReader, mutation:PolicyDeclassifyFromUnlabelled, mutation:PolicyDeclassifyUnfit, mutation:PolicyWriteUp	built, partly tested	An approved text can carry a hidden message; a push is one human action (more)
A domain holds at most one live session of a context’s name	R79 (one session per context)	`libs/steward/src/guards.rs` (the guard context_free), `libs/steward/src/machines.rs` (a login’s context checked as a name); modelled in `model/src/policy.rs`	bench:steward-context-login, host:redoubt-steward::context_free_holds_one_session_per_name, host:redoubt-steward-server::a_login_to_an_attached_context_takes_it_over, host:redoubt-model::steward_policy	built	none
A context’s console is attached to at most one channel, only after its login’s authentication, and only the steward ends a channel	R80 (one channel per context)	`libs/steward/src/effects.rs` (take_over, attach_relay, detach_relay), `servers/sshd/src/console.rs` (Consoles::may_end), `servers/consrelay`; modelled in `model/src/policy.rs`	bench:steward-context-login, bench:steward-session-ends, bench:steward-context-labels, bench:sshd-restart-detaches, host:redoubt-steward::a_context_is_attached_to_one_channel_at_a_time, host:redoubt-steward-server::a_login_to_an_attached_context_takes_it_over, host:redoubt-steward-server::closing_the_channel_detaches_the_context_and_a_login_reattaches, host:redoubt-steward-server::sshd_gone_detaches_every_attached_context, host:redoubt-sshd::a_login_s_two_consoles_and_only_the_steward_s_ends_the_channel, host:redoubt-model::steward_policy	built	none
A principal holds at most its cap of live contexts per label set; a login past it is refused after the key and before anything is carved, and nothing is evicted	R82 (the context cap)	`libs/steward/src/guards.rs` (the guard under_cap), `servers/init/src/check.rs` (holds, contexts_of); modelled in `model/src/policy.rs`	bench:steward-context-cap, bench:shell-contexts, host:redoubt-steward::the_cap_refuses_a_new_context_and_keeps_the_oldest, host:redoubt-steward-server::a_login_past_the_cap_is_refused_and_makes_nothing, host:redoubt-init::the_steward_s_sizes_fit_every_principal_s_smallest_share, host:redoubt-model::steward_policy	built	none
A detached context ends at its principal’s idle bound; an attached one never does; an attach clears the clock	R83 (idle contexts end)	`libs/steward/src/guards.rs` (the guard idle_due), `libs/steward/src/effects.rs` (attach_with, detach_relay), `servers/steward/src/bin/steward.rs` (the timer); modelled in `model/src/policy.rs`	bench:steward-context-idle, host:redoubt-steward::idle_ends_a_detached_context_only, host:redoubt-model::steward_policy	built	none
Servers: keys, files and devices
No `keyd` message returns a private key or changes the key set	R43 (no export)	`servers/keyd/src/server.rs`, `servers/keyd/src/keys.rs`	bench:r4-host-tests, host:redoubt-keyd::nothing_in_the_protocol_returns_a_key, host:redoubt-keyd::no_request_can_put_a_key_into_keyd, host:redoubt-keyd::random_requests_never_panic	built	The seeds live in `init`’s memory and the bundle (more)
A badge signs with one key, for one purpose, over a digest `keyd` computes itself	R44 (one key, one purpose, keyd’s own digest)	`servers/keyd/src/keys.rs`, `servers/keyd/src/ssh.rs`	bench:r4-host-tests, host:redoubt-keyd::a_badge_signs_only_its_own_key_and_only_its_own_purpose, host:redoubt-keyd::a_relayed_ssh_user_auth_blob_is_never_what_gets_signed, host:redoubt-keyd::parts_cannot_be_slid_into_each_other, host:redoubt-keyd::the_hash_matches_an_independent_implementation, host:redoubt-keyd::a_granted_capability_names_the_same_key_and_dies_with_release	built	`keyd` sees the SSH shared secret; an `ssh_host` badge speaks as the box (more)
Signing takes the same time whatever the key	R45 (constant-time signing)	`libs/sha256/src/lib.rs`, `servers/keyd/src/keys.rs`, the Ed25519 crate keyd links, at the version pinned in `Cargo.lock`	—	built, partly tested	The timing tests are ignored in an ordinary test run (more)
`/boot` shows exactly the public list’s entries, fixed at the seal	R46 (only the public list)	`servers/bootfsd/src/server.rs`	host:redoubt-bootfsd::a_session_reads_the_public_entries_and_sees_nothing_else, host:redoubt-bootfsd::a_walk_to_an_unpublished_name_is_the_same_as_to_one_that_never_existed, host:redoubt-bootfsd::setup_is_refused_after_seal_and_from_every_minted_connection, host:redoubt-bootfsd::nothing_is_visible_before_seal, host:redoubt-bootfsd::every_way_of_writing_is_refused, host:redoubt-bootfsd::a_client_cannot_publish_into_boot	built	Whatever is public is public to everyone (more)
Each `walfsd`, `littlefsd` or `erofsd` instance serves one volume and holds only its block range	R47 (one volume per instance)	`servers/init/src/check.rs`, `servers/init/src/bin/init.rs`, `servers/littlefsd/src/bin/littlefsd.rs`, `servers/erofsd/src/bin/erofsd.rs`, `servers/walfsd/src/bin/walfsd.rs`	bench:littlefsd-one-volume, bench:walfsd-one-volume, host:redoubt-init::a_walfsd_entry_is_a_volume_server_as_a_littlefsd_one_is, host:redoubt-init::an_erofsd_entry_is_a_volume_server_as_a_littlefsd_one_is, host:redoubt-init::no_server_is_handed_a_badge_at_blkd	built	A shared `littlefsd` is shared state (more)
Every connection’s root has a byte quota carved from its granter’s	R48 (a quota per attach root)	`libs/fileserver/src/quota.rs`, `servers/littlefsd/src/server.rs`, `servers/walfsd/src/server.rs`	bench:littlefsd-quota, bench:walfsd-pools, bench:walfsd-quota, host:redoubt-littlefsd::a_root_with_quota_0_cannot_create_but_can_read_and_remove, host:redoubt-littlefsd::a_write_past_one_roots_quota_is_refused_while_another_still_writes, host:redoubt-walfsd::a_root_with_quota_0_cannot_create_but_can_read_and_remove, host:redoubt-walfsd::a_write_past_one_roots_quota_is_refused_while_another_still_writes	built	A refused rename or remove says a live root is there (more)
Whatever bytes the medium holds, littlefs, erofs and walfs refuse them as corrupt rather than crashing	R49 (a hostile medium is corrupt, not a crash)	`libs/littlefs/src/mdir.rs`, `libs/littlefs/src/fs.rs`, `libs/erofs/src/read.rs`, `servers/erofsd/src/server.rs`, `libs/walfs/src/layout.rs`, `libs/walfs/src/fs.rs`, `servers/walfsd/src/server.rs`	bench:erofs-corrupt, bench:walfsd-corrupt-volume, bench:walfsd-flipped-block, fuzz:erofs/image, fuzz:littlefs/image, fuzz:littlefs/mutate, fuzz:walfs/image, fuzz:walfs/mutate, host:littlefs::corrupted_bytes_never_panic, host:littlefs::forged_file_sizes_do_not_amplify_allocation, host:littlefs::noise_never_panics, host:littlefs::skip_list_pointing_at_itself_terminates, host:littlefs::stale_handle_after_pair_drop_does_not_erase_another_files_data, host:littlefs::tail_list_cycle_is_refused, host:redoubt-walfsd::a_flipped_bit_in_a_file_is_corrupt_for_that_file_alone, host:redoubt-walfsd::noise_is_never_formatted_and_never_mounted, host:walfs::every_flipped_bit_is_corrupt_where_it_is_read, host:walfs::noise_never_panics	built	littlefs’s data is not checksummed (more)
A power cut at any block write leaves every metadata change done or not done, and on walfs every operation	R50 (power loss leaves before or after)	`libs/littlefs/src/fs.rs`, `libs/littlefs/src/mdir.rs`, `libs/walfs/src/fs.rs`, `servers/walfsd/src/volume.rs`	bench:walfsd-power-loss, host:littlefs::crash_at_every_write_random_workloads, host:littlefs::crash_at_every_write_small_blocks, host:littlefs::crash_at_every_write_torn_erases, host:littlefs::crash_during_repair, host:redoubt-walfsd::a_cut_at_every_write_of_a_write_and_a_rename_leaves_before_or_after, host:walfs::crash_at_every_write_fixed_workload, host:walfs::crash_at_every_write_random_workloads, host:walfs::crash_during_recovery	built	Attributes and data are two commits (more)
`blkd` points the device only at its own DMA region	R51 (DMA stays in its region)	`servers/blkd/src/queue.rs`, `servers/blkd/src/virtio.rs`	host:redoubt-blkd::a_broken_device_is_never_handed_a_clients_write_payload, host:redoubt-blkd::a_hundred_thousand_random_liars_never_panic_and_never_stray, host:redoubt-blkd::impossible_requests_never_reach_the_device	built	`blkd` is trusted without an IOMMU (more)
A lying disk makes a request fail, never corrupts `blkd` or mixes clients’ bytes	R52 (a lie is a failure, never corruption)	`servers/blkd/src/transport.rs`, `servers/blkd/src/queue.rs`	fuzz:redoubt-blkd/device, host:redoubt-blkd::rewriting_the_rings_changes_nothing_the_driver_believes, host:redoubt-blkd::a_device_that_lies_about_a_completion_is_refused_and_never_spoken_to_again, host:redoubt-blkd::a_lying_device_becomes_failed_and_stays_failed, host:redoubt-blkd::a_hundred_thousand_random_liars_never_panic_and_never_stray, host:redoubt-blkd::one_clients_read_never_carries_anothers_bytes	built	Wrong bytes are not detected (more)
A client’s badge names one partition, and overlapping partition tables are refused	R53 (a filesystem sees only its partition)	`servers/blkd/src/gpt.rs`, `servers/blkd/src/range.rs`	fuzz:redoubt-blkd/gpt, host:redoubt-blkd::a_range_cannot_name_a_sector_outside_itself, host:redoubt-blkd::hostile_partition_entries_are_refused, host:redoubt-blkd::a_badge_that_names_no_range_is_refused, host:redoubt-blkd::a_gap_in_the_table_does_not_renumber_the_volumes_after_it	built	`blkd` is trusted without an IOMMU (more)
A reader of a verified volume sees only blocks that hash, through the tree, to the root the signed manifest gives, or, for a signed volume, to the root its root block gives, signed under the manifest’s key at a version no lower than the manifest’s floor; otherwise a device failure, which `littlefsd` serves as corrupt	R76 (verified volumes)	`libs/verity/src/lib.rs`, `libs/signing/src/lib.rs`, `servers/verityd/src/volume.rs`, `servers/verityd/src/server.rs`	bench:userland-boot, bench:userland-bad-start, bench:verity-flipped-tree, bench:verity-wrong-root, bench:verity-bad-signature, bench:verity-rollback, host:redoubt-verity::a_flipped_bit_at_each_level_is_refused, host:redoubt-verityd::a_wrong_root_or_top_is_refused, host:redoubt-verityd::a_mismatch_is_failed_and_said_naming_the_block, host:redoubt-verityd::a_failed_block_is_never_kept, host:redoubt-verityd::arbitrary_media_never_panic, host:redoubt-verityd::a_root_block_that_does_not_verify_is_refused_naming_the_signature, host:redoubt-verityd::a_root_block_below_the_floor_is_refused_naming_the_version	built	Rollback is the bundle’s, a signed volume’s floor with it; writable volumes are unverified (more)
No labelled caller writes to the physical console	R69 (no write down onto the console)	`servers/consoled/src/server.rs`	host:redoubt-rt::labels_are_checked_on_every_request, host:redoubt-rt::every_write_needs_equal_labels	built, partly tested	Anyone with a connection reads the console (more)
A stuck or lying UART never hangs `consoled`	R70 (a stuck UART never hangs the console)	`servers/consoled/src/uart.rs`, `servers/consoled/src/server.rs`	host:redoubt-consoled::a_device_stuck_on_data_ready_does_not_hang_the_server, host:redoubt-consoled::a_flood_of_input_keeps_what_was_typed_first	built	QEMU’s UART neither sticks nor lies: only a fake one on the host does (more)
Servers: packages and services
Code runs with a principal’s grants only if a key on its trust list signed it	R71 (no new authority without trust)	planned: the steward and the pkg server	—	planned · M6 (persist, install, share)	A stolen trusted key; a hijacked agent runs code it wrote (more)
An untrusted archive never reaches the parser, and a trusted hostile one writes only its principal’s packages	R74 (a hostile package stays in its principal’s packages)	planned: the pkg server	—	planned · M6 (persist, install, share)	Every principal reaches the whole system-call interface (more)
A restarted service gets exactly its recorded grants, through fresh connections	R73 (a restart never widens)	planned: the supervisor	—	planned · M6 (persist, install, share)	A restart does not clean what the service wrote (more)
Network
`netd` points the device only at its two DMA regions	R54 (DMA stays in netd’s regions)	`servers/netd/src/ring.rs`, `servers/netd/src/virtio.rs`	host:redoubt-netd::scribbling_devices_change_nothing_netd_believes, host:redoubt-netd::randomized_hostile_devices, host:redoubt-netd::a_transmit_sends_exactly_its_header_and_frame	built	`netd` is trusted without an IOMMU (more)
A bad frame from the wire is dropped as content, never taken as a device lie	R55 (a bad frame is content, not a lie)	`servers/netd/src/receiver.rs`, `servers/netd/src/rxq.rs`	host:redoubt-netd::a_bad_frame_from_the_wire_is_dropped_never_a_lie, host:redoubt-netd::receive_lies_are_refused, fuzz:redoubt-netd/device	built	A frame flood costs `netd`’s CPU (more)
No byte of an earlier frame reaches a later one	R56 (no earlier frame leaks)	`servers/netd/src/rxq.rs`, `servers/netd/src/txq.rs`	host:redoubt-netd::a_transmit_sends_exactly_its_header_and_frame, host:redoubt-netd::an_inflated_length_reads_zeros_not_old_frames, host:redoubt-netd::frames_arrive_exactly_and_every_slot_comes_back	built	A reset stops the device for everyone (more)
On every way out `netd` controls, the device is reset first	R57 (the device stops before netd does)	`servers/netd/src/device.rs`, `servers/netd/src/bin/netd.rs`	host:redoubt-netd::a_panic_resets_the_device, host:redoubt-netd::the_receive_loop_resets_and_reports_a_lie, host:redoubt-netd::the_receive_loop_resets_and_reports_when_the_interrupt_fails, host:redoubt-netd::only_the_receive_threads_report_breaks_the_device	built, partly tested	A kill from outside gives `netd` no chance to reset (more)
A connection reaches only the addresses and ports its scope allows	R58 (a scope reaches only what it allows)	`servers/ipd/src/scope.rs`, `servers/ipd/src/stack.rs`	bench:net-attacks, host:redoubt-ipd::a_scope_permits_exactly_what_its_rules_contain, host:redoubt-ipd::connects_outside_the_scope_or_to_the_box_are_refused_and_send_nothing, host:redoubt-ipd::numbers_are_per_connection_and_invisible_to_others	built	A NAT hairpin is refused only if listed (more)
No connection reaches the box’s own addresses, whatever its scope	R59 (never the box’s own addresses)	`servers/ipd/src/scope.rs`, `servers/ipd/src/args.rs`, `servers/ipd/src/stack.rs`	bench:net-attacks, bench:bench-net-self-unrefused, bench:session-tcp-loopback, host:redoubt-ipd::the_self_set	built	A NAT hairpin is refused only if listed (more)
`ipd` refuses every labelled caller before reading its request	R60 (a sink refuses labels)	`servers/ipd/src/server.rs`	bench:net-attacks, host:redoubt-ipd::a_labelled_caller_gets_nothing_and_holds_no_bucket	built	Connection rates are observable (more)
A connection’s scope is always within the scope it came from	R61 (scopes only narrow)	`servers/ipd/src/scope.rs`, `servers/ipd/src/server.rs`	host:redoubt-ipd::a_grant_only_narrows, host:redoubt-ipd::a_grant_never_widens_or_adds_listen, host:redoubt-ipd::new_connection_keeps_the_scope	built	A shared `ipd` is shared state (more)
Initial sequence numbers come from the kernel’s random words	R62 (sequence numbers from the kernel)	`servers/ipd/src/stack.rs`	host:redoubt-ipd::each_active_open_takes_one_seed_and_its_isn_is_that_seeds, host:redoubt-ipd::each_passive_open_takes_one_seed_and_its_isn_is_that_seeds, host:redoubt-ipd::without_a_seed_nothing_opens	built	Blind injection within a guessed window (more)
The resolver queries and answers only allowed names	R63 (only allowed names)	planned: the resolver	—	planned · M5 (self-hosted development)	Upstream answers are believed; the upstream’s cache is shared (more)
A connection by name reaches one checked address for its whole life	R64 (connections by name are pinned)	planned: the resolver and ipd	—	planned · M5 (self-hosted development)	A name’s addresses are shared (more)
`gatewayd` sends only requests it built and checked against the caller’s capability and meter	R65 (a request only within its capability)	planned: gatewayd	—	planned · M5 (self-hosted development)	The service sees what the agent sends; metering trusts the provider (more)
No credential ever leaves `gatewayd`, except over TLS to its own service	R66 (no credential leaves gatewayd)	planned: gatewayd	—	planned · M5 (self-hosted development)	The keys sit beside the response parser and in the bundle (more)
A labelled session’s output reaches only its owner’s own pty channel	R67 (a channel keeps its labels)	`servers/sshd/src/console.rs`, `servers/sshd/src/bin/sshd.rs`	bench:sshd-loopback-r67, bench:steward-vault-session, bench:steward-vault-launch, host:redoubt-sshd::the_console_is_one_file_carrying_the_channel_s_labels	built	`sshd` is trusted across labels (more)
On `approve@box` only the steward draws and only the steward hears	R68 (only the steward on approve@box)	`servers/sshd/src/bin/sshd.rs` (approve), `servers/steward/src/bin/steward.rs` (reader_thread, screen)	bench:steward-approve-box, bench:steward-screen-inert	built, partly tested	`approve@` shares `sshd` with the most hostile input; a route back to the box the manifest does not list (more)

Residual risks by wall

What each wall leaves open, gathered from the pages’ residual risks. The four walls that are not the OS’s own are described on the tenets.

Boot.

On QEMU the loader itself is not verified, and whoever controls the host’s files chooses what boots; the development signing key is public; there is no rollback protection until the version counter (boot, packages).
The device tree is not signed, and the firmware is trusted. A device tree that hides a controller from the loader’s controller search and its device list defeats the kernel’s Ctrl check, whose list of controllers comes from the same tree (boot, devices).
The boot bundle’s confidentiality is not claimed: seeds in it are readable by whoever reads the image (boot).
A confined boot is checked once; a capability handed across label sets later is the handing server’s fault, not the kernel’s (init).

The kernel.

System-class servers are trusted to check labels; the kernel checks only between user budgets (IPC).
Destruction is uninterruptible kernel time, which follows the dying subtree (budgets, scheduling).
A driver that programs DMA is trusted: there is no IOMMU, and reset-before-reuse does not confine a live driver (devices).
Only virtio-mmio devices are reset: any other DMA device is never reset, so every process end that reaches it quarantines, and such a platform gets no driver restart (devices).
A co-holder keeps its mapping of a quarantined device, and of a device whose handle was revoked: the kernel does not unmap device ranges (devices).
A crash can blame nobody: corruption left by an answered call can crash a thread later, when it has no current call (processes).
PIDs are one global pool that untaken exit notices can hold (processes).
The kernel runs on one hart; completion races and flushes across harts are argued, not attacked (the kernel), until M2 (usable shell) brings several harts (several harts).

The servers.

The named mediators, the steward and sshd, are trusted across the labels they serve (the steward, sshd).
There is no non-collusion guarantee within one label set: agents with the same label set and each other’s handles can cooperate (the tenets).
A dead launcher leaks its children’s connections until its own connection is freed, against its own account and label set (serving).
An account-0 client can spend every bucket of a 9P server, and a server sized for fewer buckets than the label sets it serves is a channel (serving).
Server work is paid by the server’s weight, not the requester’s (the servers).

The session. A session is per-principal code: a bug in it reaches that principal’s own capabilities, which the kernel contains (trust tiers).

beamlet’s own code is memory-safe, but crates it links hold unsafe and parse hostile data (compressed streams, patterns, certificates) with the session’s authority, as any program’s libraries do. A memory bug there, reached by a file another principal wrote, an agent’s opened by its sponsor above all, has the sponsor’s session, whichever of its tools read it; the kernel keeps it to that principal, and keys and approvals out of its reach (beamlet, the shell).
The terminal guard stops hostile text, not the session’s own code, which can write to its own console; and it draws the bidirectional marks, which only settle weak and neutral characters (the shell).
The terminal guard draws every character that is there, not its likeness: a name made of look-alike letters (Cyrillic а for a) can still look like another (the shell).
Ed25519 is checked cofactored everywhere on the box, so signatures are malleable; nothing that holds a wall takes one as an identifier (beamlet, boot).
Until M6 (persist, install, share) a session has no wall clock and counts from 1970 at boot: a check that a date has begun fails, but a check only that one has not passed, a token’s expiry, passes whatever the token, and times from two boots cannot be ordered (beamlet).
A console that stops answering a write stops the session’s VM, until writes move to its I/O threads (beamlet).
A session makes a fixed number of waiting calls at once, and one past it is refused; memory off the Erlang heap, a large binary, is bounded only by the session’s own page limit (beamlet, the shell).

The supply chain.

Vendored crates are checked against checksums taken from the tree itself: that proves they have not changed since vendoring, not that they match their upstream release (vendored dependencies).
The vendored crates’ unsafe is outside the ratchet; recorded Miri runs cover their own tests and ipd’s (ipd under Miri).
The unsafe ratchet counts only what its budgets name; it fails when a no_std workspace member has a source in no budget, but a member it lists as uncounted is trusted to be off the target (the unsafe budget).

The network.

Upstream DNS answers are believed, and an allowed name’s address may host other services (the resolver).
A shared ipd is shared state; connection rates are observable (ipd).
The model service sees what an agent sends, and metering trusts the provider’s figures (gatewayd).

Walls the OS does not own.

The approval human: the requester can persuade, repeat until the human tires, or phrase a request that reads one way and means another; an approved text can carry a hidden message, and a push is one human action (the tenets, the steward).
Host virtio emulation: a bug in the host’s emulation reachable through a driver is outside the OS (the tenets).
Allowed egress: every allowed channel out can carry data: a model API, a git remote, the upstream resolver’s shared cache (the tenets).
Side channels: scheduling is observable, and so is server CPU spent on a caller’s behalf; every process has a perfect clock; CPU caches, the shared second-level cache and memory bandwidth are not partitioned; a shared server’s caches and the disk are shared unless the deployment is confined (scheduling, timer, the tenets).

Keyboard shortcuts

Redoubt

The security register

How to audit

The walls

The register

Residual risks by wall