The servers
Everything the kernel does not keep runs as an unprivileged server: drivers, file systems, the network, keys, logins and policy. A server is a process that receives on an endpoint and answers calls. It reaches hardware only through device handles, other servers only through endpoint handles, and the kernel only through the system calls every process has. This page is the map: who starts whom, which server is trusted with what, how servers apply labels, how a client gets a connection of its own, what happens when a server crashes, and which capabilities each server holds.
Purpose
The kernel enforces labels only between user-class budgets
(R1 (flow)). The servers every principal shares run in the system
class, where the kernel does not check, so their code is where separation between principals is
kept or lost. A reader auditing Redoubt needs to know, for each server, what it holds, whom it
serves, and which rule stops one client reaching another’s data through it. The pages below this
one take one server each; this page states what they share.
The server graph
Status: planned · M1 (sessions over SSH, kept apart)
The loader starts only the kernel and init (boot). init reads the boot
manifest and starts every system server from the bundle, through the loader stub
(init). It then starts the steward, which holds the users budget and starts every
session and agent. Nothing else starts a server.
flowchart TD
L[loader] --> K[kernel]
K -.-> I[init]
I -.-> CO[consoled<br/>the console]
I -.-> BF[bootfsd<br/>/boot]
I -.-> BL[blkd<br/>the disk]
I -.-> VD[verityd<br/>one per verified volume]
I -.-> FS[littlefsd:volume<br/>one per flash volume]
I -.-> EF[erofsd:volume<br/>one per read-only volume]
I -.-> WF[walfsd:volume<br/>one per writable SSD volume]
I -.-> ND[netd<br/>the network card]
I -.-> IP[ipd:network<br/>TCP/IP]
I -.-> KD[keyd<br/>keys]
I --> ST[steward<br/>principals and policy]
I --> SS[sshd<br/>logins]
ST --> SE[sessions<br/>Elixir VMs]
ST -.-> AG[agents<br/>under leases]
Figure: who starts whom. Solid arrows are built; dashed are planned for M1 (sessions over SSH, kept apart), and agents for M3 (agents, approvals and the attack suite).
init starts the drivers and the servers that need no principal first (consoled, bootfsd,
blkd, each verityd, each littlefsd, erofsd and walfsd, netd, each ipd, keyd), then the steward
and sshd.
It keeps each server’s receive right, so a restarted server receives on the same endpoint (Restarts
and crash blame, below). The servers planned for later milestones join the same graph:
the resolver and gatewayd in M5 (self-hosted development), and
the package server and the supervisor in
M6 (persist, install, share).
Open: whether the supervisor of M6 (persist, install, share) takes over restarting from
init or runs beside it (supervisor).
Trust tiers
Status: planned · M1 (sessions over SSH, kept apart)
| Tier | Members | Trusted for | A compromise reaches |
|---|---|---|---|
| TCB | firmware, loader, kernel; blkd and netd while there is no IOMMU | everything | the whole machine |
| Trusted system servers | init, the steward, keyd, sshd | crossing principals: logins, keys, approvals, launching | every principal |
| Shared servers | consoled, bootfsd, each littlefsd, erofsd and walfsd, each ipd; later the resolver and gatewayd | serving many principals and keeping them apart by badge and label | the principals that server serves |
| Per-principal code | sessions, agents, native programs, a session’s piped | nothing beyond their own capabilities | that principal’s own capabilities |
- The DMA drivers are TCB. A driver that holds a DMA-flagged device handle can point a bus
master at any physical address (devices).
blkdandnetdare small and parse only their own device’s structures for that reason. - Every trusted system server is Rust. Everything whose compromise could cross principals
(the steward,
keyd,sshd) is written in Rust and runs outside the Elixir VMs. The BEAM is userland: a compromised session VM holds exactly its principal’s capabilities, like a native program. - A shared server is split by network or medium, so one parser bug does not reach every
principal: one
littlefsd,erofsdorwalfsdper volume, oneipdper network or trust domain. - Server work is paid by the server’s weight, not the caller’s; no time is donated. Each shared server therefore bounds the work one request can cause and admits by caps (scheduling, serving).
Open: none.
Labels
The rule servers apply
Status: built · tested (6)
- 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
Labels are information-flow labels on budgets and volumes. The kernel checks them between user budgets; system servers check them themselves, on every request, using the label set the kernel attaches to each message (R14 (unforgeable sender)). A system server applies one check, written once in the serving library (R25 (the label check)):
- Read an object only if the object’s labels are a subset of the caller’s: no read up.
- Write an object only if the two label sets are equal: no write down, and no blind write up. A write up could truncate or remove what the writer cannot read.
- Metadata is a read. A 9P qid and a
statare reads of their node: a walk into a node the caller cannot read is refused, and a directory listing leaves out the entries the caller cannot read. Otherwise every write in a vault would change what an unlabelled caller sees.
Label sets are compared as sets. Data enters a label only by being read down: a vault session reads it from where it is. Nothing writes into a label from outside it.
The labels are the kernel’s; the server trusts only them, never a label named in a request. Two budgets with equal label sets are one trust domain: a handle passed between them crosses nothing.
Who checks, and sinks
Status: built · partly tested: only ipd’s refusal of labelled callers is attacked in a boot; the skeleton’s checks are attacked in host tests · tested: bench:net-attacks, host:redoubt-rt::labels_are_checked_on_every_request
- Every 9P server gets the check from the skeleton, against the labels its file server reports for each node (serving).
- A sink is a server whose output leaves a principal or the machine. A sink is cleared for no
label and refuses every labelled caller before it reads the request.
ipdis one (ipd); innet-attacksa labelled caller’s connect reaches nothing on the network while its unlabelled twin’s does. - User-level servers get no exemption. A server in a
userbudget is under R1: a vault session cannot call an unlabelled user server. A service that must serve several label sets runs one instance per label set, or in thesystemclass. - A receive right is never handed across label sets. R1 compares a sender with the endpoint’s owner, not with whichever process receives, so a badge-0 handle given to a budget with other labels would deliver messages nobody compared with it. A system server that does this is at fault, not the kernel.
Labels on the running system
Status: planned · M1 (sessions over SSH, kept apart)
The steward creates every labelled budget, after an approval, and a child inherits its parent’s
labels (budgets). A volume has one label set, fixed by
the boot manifest or the steward and never read from the medium (littlefsd). The steward
mounts known-sensitive places (~/.ssh, credential directories) on the principal’s labelled
volume, and keys belong in keyd, which uses them without releasing them. sshd is the one
sink cleared for a label, and only on the channel whose owner authenticated it
(sshd); gatewayd is a sink cleared for nothing (gatewayd). Each shared server’s
page states what its objects are and which label set each carries, so that nothing a labelled
caller influences is visible to a caller without that label: littlefsd keeps state per volume,
sshd per channel, and the steward applies the check to its own records.
Open: none.
Connections
Status: built · partly tested: `init-boot` exercises fresh child connections on the machine; their isolation and disconnect behavior are attacked only against the runtime's fake kernel · tested (7)
- bench:init-boot
- host:redoubt-rt::a_launcher_gives_its_child_a_fresh_connection_and_disconnects_it
- host:redoubt-rt::new_connection_is_rooted_below_the_callers_root
- host:redoubt-rt::a_disconnect_frees_its_fids_and_every_connection_minted_under_it
- host:redoubt-rt::a_strangers_id_is_refused_like_one_that_does_not_exist
- host:redoubt-rt::copies_of_one_badge_in_other_accounts_or_label_sets_share_nothing
- host:redoubt-rt::self_minting_does_not_multiply_the_share
A capability to a server is an endpoint handle whose badge names the grant: for a 9P server, a connection with its own attach root and fid table. The pattern is one endpoint per service and one badge per client (objects).
- One badge, one client. Every copy of a handle carries the same badge, and the kernel gives a
server no per-process identity, so every holder of a copy shares one connection. So a
launcher never passes its own connection to a child. It asks the server for a fresh one with
new_connection(9P servers) orgrant(typed servers) and passes that. Otherwise a hostile agent started from Alice’s shell could read, close or wipe her open files. - A second line of defence. Servers key per-client state by badge, account and label set, so holders of one copied handle in different accounts or label sets never share fids.
- Disconnect, not a kernel notice. The kernel does not tell a server when a client’s handles
are gone.
new_connectionreturns a random connection id with the handle; only the client that received the id candisconnect(id), which frees that connection and everything minted under it. Anyone else, like an id that does not exist, gets the samenot_yours.
The serving library implements all of it once (serving).
Cleaning up after a child
Status: planned · M1 (sessions over SSH, kept apart)
A launcher disconnects a child’s connections, and releases its grants from typed servers, when it
receives the child’s exit notice (processes); the steward
does the same at logout and at a lease’s end. A child’s grants never outlive its launcher’s
(wire). The serving library provides the
disconnect it uses.
Open: none.
Restarts and crash blame
Status: planned · M1 (sessions over SSH, kept apart)
initrestarts every server that ends, on the same endpoint. Calls the server had taken getDead, and clients retry; senders still queued wait and are served by the restarted server (R4b (a server dies)). A server keeps no state across a restart: what a badge meant lived in its memory. It draws its first minted badge at random, so its clients’ old handles do not name its new grants (R27 (badge allocation)).- More than five restarts of one server within 60 seconds reboot the machine: fail closed (init).
- Crash blame. A server’s exit notice blames the sender of the call it was working on
(R21 (crash blame)).
initpasses the blame to the steward, and three crashes blamed on one account and label set within ten minutes end every budget of that account and label set (steward). A crash that blames nobody counts only toward the restart limit. - Session VMs are not restarted. A dead session is a logout.
Open: none.
Capability holdings
Status: planned · M1 (sessions over SSH, kept apart)
| Server | Receives on | Holds | Never holds |
|---|---|---|---|
init | the exit endpoint of every server | root, system and users; every device object and the Reset right; every server’s receive right; the bundle’s pages | network, user data, keys |
| steward | its own endpoint | users; a badge at bootfsd, each volume’s walfsd or littlefsd, erofsd and ipd, through which it asks for each session’s connections; a keyd grant for the audit purpose, from M4 (files in and out) | any key; a budget of a server |
keyd | its own endpoint | the keys the manifest names | a key a person logs in or approves with; the bundle key |
sshd | its own endpoint | the network through ipd; a keyd badge for the host key; the steward’s endpoint | any login key |
consoled | its own endpoint | the UART’s MMIO and IRQ handles | anything else |
bootfsd | its own endpoint | the public bundle entries, pushed by init | the bundle itself |
blkd | its own endpoint | the disk’s MMIO (DMA) and IRQ handles | anything else |
verityd | its own endpoint | a blkd range for its verified volume | a device; a write to the range |
littlefsd:volume | its own endpoint | a blkd range for its volume, or a verityd range for a verified one | another volume |
erofsd:volume | its own endpoint | a blkd range for its read-only volume, or a verityd range for a verified one | another volume; a write to the range |
walfsd:volume | its own endpoint | a blkd range for its writable volume on the SSD | another volume |
netd | its own endpoint | the network card’s MMIO (DMA) and IRQ handles | anything else |
ipd:network | its own endpoint | a netd connection | a budget; a labelled caller’s request |
piped | the endpoint its session’s launch made | the buffers of one session’s pipes | any other handle; another session’s bytes |
crossing | the endpoint the steward calls it on, and one connection to the labelled volume at its root, in a budget with exactly that label set | one item read or written (the steward) | a second call; anything outside its label set |
No server’s startup block carries a budget handle. A manifest that gives a server one is refused,
because a budget handle is a destroy right and a create right: a compromised ipd holding its
budget could create system-class children with any labels and any account. A server that must
revoke a grant on its own is given a revocation scope, a budget with zero limits used only to
be destroyed (init, steward).
flowchart LR
I[init<br/>root, system, users,<br/>Reset, receive rights] -. places disk handles .-> BL[blkd]
I -. places NIC handles .-> ND[netd]
I -. places UART handles .-> CO[consoled]
I -- hands users --> ST[steward]
I -. pushes public entries .-> BF[bootfsd]
I -. passes seeds .-> KD[keyd]
FS[littlefsd:volume] -. range badge .-> BL
EF[erofsd:volume] -. range badge .-> BL
WF[walfsd:volume] -. range badge .-> BL
IP[ipd:network] -. netif connection .-> ND
ST -. audit grant .-> KD
SS[sshd] -. host-key badge .-> KD
SS -- login and sessions --> ST
SS -- connections --> IP
ST -- connections --> FS
ST -- connections --> WF
ST -- scoped grants --> IP
Figure: the capabilities each server holds. An edge from init is a handle it places; any other
edge runs from a holder to the server its handle reaches. Solid edges are built; dashed ones are
planned.
Open: whether init keeps a copy of each device handle it places, so it can restart a driver,
and so stays a co-holder (devices).
Naming
Status: built · tested: bench:init-boot, bench:userland-boot
A file server is named for the format it serves, and its endpoints for the volumes: erofsd
serves EROFS and erofsd:system is the system volume; walfsd serves walfs and walfsd:data
is the data volume; littlefsd serves littlefs. The name says what parser stands between a
client and the medium, which is what
R47 (one volume per instance) bounds. Servers that
serve no format keep their role’s name (blkd, bootfsd, verityd). What the volume servers
share beside their formats, their arguments, their client of blkd’s range and the quota ledger,
is one crate beside the serving library, redoubt-fileserver
(serving), so a volume server’s own code is its format’s.
The network path
netd and ipd
Status: built · tested: bench:net-tcp, bench:net-attacks, bench:session-tcp-echo
netd, the network card’s driver, moves Ethernet frames between the card and one client, ipd.
ipd, the TCP/IP server, serves the /net tree to its callers, each scoped to the prefixes and
ports its badge allows (ipd, netd). A test program in the first program’s
place launches the real netd and ipd through the loader stub and starts the cases’ clients:
net-tcp carries TCP both ways through them, and net-attacks shows a scope’s refusals
from the bench’s own network peers. A session’s VM reaches ipd through the /net of its
namespace: gen_tcp over the tree’s files, by address
(beamlet; session-tcp-echo).
flowchart LR
S[a session's VM: gen_tcp over /net] --> IP[ipd]
P[a person's session] -. name-scoped TCP .-> R[resolver]
R -. pinned connection .-> IP
A[agent] -. gateway capability .-> G[gatewayd]
G -. TLS .-> T[tlsd]
T -. TCP .-> IP
C[client with a scope] --> IP
IP --> N[netd]
N --> V[virtio-net]
Figure: the network path. Solid is built; dashed is planned: the resolver and gatewayd
for M5 (self-hosted development), tlsd beyond M6.
The path for people and agents
Status: planned · M5 (self-hosted development)
Agents never get sockets. An agent holds gateway capabilities to gatewayd, which makes the
request itself, over TLS, to one allowed service, checks it and logs it
(gatewayd). Only people get TCP, and only by name: the resolver answers only the
names in the caller’s allowlist, and a connection is made by name and pinned to what the name
resolved to (resolver). The host’s and the cloud metadata addresses, the box’s
own services from inside, and inbound traffic other than SSH are always refused.
Open: whether TLS for gatewayd runs in a separate tlsd in M5 (self-hosted development) or
inside gatewayd until the web stack needs tlsd beyond M6.
Residual risks
- System servers are trusted to check labels. The kernel does not check a flow into or out of
a
systembudget (R1). A shared server that mixes two label sets’ data breaks label separation, and nothing below it can see that. - A dead launcher leaks its children’s connections. A launcher that dies without disconnecting leaves its children’s connections in each server until its own connection is freed; the leak counts against its own account and label set (serving).
- Server work is paid by the server’s weight. A client that floods a shared server takes that server’s share of the CPU from its other callers, never more (scheduling).
- The DMA drivers are TCB while there is no IOMMU (devices).
- Volumes are kept apart by placement. The image’s
initrunswalfsd:dataanderofsd:system, one instance per volume, so one volume’s data is out of another’s instance only becauseinitplaces each volume once (R47 (one volume per instance)).
Why
- Servers, not kernel code. A driver, a file system or a TCP stack in the kernel would put its parser in the TCB. As a server it holds only its handles, and a bug in it reaches only what those handles reach.
- One endpoint per service, one badge per client. Endpoints cost their owner a page each and are not reclaimed until the owner budget goes (objects); badges cost nothing and carry the grant.
- Servers keep no authority across a restart. A server that saved what its badges meant could be made to write itself a root badge. Endpoints outlive servers, so clients keep their handles; the grants behind them are re-made by whoever made them.
- Sinks refuse labels. Whatever enters a sink can leave the machine, so a sink cleared for a label would be a declassification nobody approved.