Init

init is the first process. It reads the boot manifest from the signed bundle, starts every system server from the bundle’s pages through the loader stub, gives each its handles, names and arguments in a startup block, and restarts a server that exits. It holds the boot budgets and every device, and it has no network and no user data. The startup block and the loader stub every launcher uses are described here as well.

Purpose

Something must turn the kernel’s handful of boot handles into a running system, and it must do so from one signed, checked description rather than from code that decides as it goes. init is that step: the manifest says what runs, with which devices, volumes, labels, weights and arguments, and init refuses a manifest that breaks a rule before anything runs. It parses only that one file and no ELF, so the most privileged process after the kernel has the smallest input.

Interface

The boot manifest

The boot manifest is one strict JSON file (wire) in the signed bundle, and init’s only input. Its entries:

• Types. Each field has one JSON type. A 64-bit quantity (a label id, an account, a size in pages or bytes, a deadline) is a decimal string; a small count (processes, a weight, a depth, a restart limit, a port) is a number. heap_pages is a decimal string of at most 4294967295, the startup block’s u32; a larger one is the wrong type. A wrong type, an unknown member or a repeated one is an error, and an error refuses the boot.
• Names. Every name (device, label, volume, server, endpoint, principal) is 1 to 64 bytes of [a-z0-9_:+-], starting with a letter (walfsd:data, alice+secrets), compared byte for byte. Names become endpoint names, volume names and 9P paths, so no empty name, NUL, U+FEFF or control character may reach them. The startup block applies the same rule (valid_name). A principal’s and a label’s name hold no : or + either, so that a login’s user name, principal[+label][.context], splits one way only, and no principal is named approve, the approval terminal’s user name (contexts).
• Stacks. A server’s stack_pages is the size of its first thread’s stack, charged to its budget. init refuses zero, more than 128 pages, or a stack not smaller than its budget’s pages, before it starts any server. A budget that holds the stack but not the image beside it makes that server’s launch fail, which refuses the boot, or on a restart reboots the machine (restarts and reboots). The bench measures each server’s peak across the required boot and userland paths and requires the declaration to hold at least twice the largest peak (the memory budget).
• Heaps. A server’s heap cap is the most pages its runtime’s allocator holds; past it an allocation fails in the runtime before the kernel is asked. The budget stays the bound on everything else. init refuses 0, or a cap and stack the budget cannot hold. The bench requires each image server’s cap to hold at least twice its largest heap peak (the memory budget). A shared server’s entry follows the entry rule besides: its pages hold its buckets=N at their caps beside the heap cap and the stack (walfsd), which the server checks at start from the budget and heap cap its startup block carries, and refuses to start without.
• One entry per device. A devices entry names one device, by its register region and its interrupt, and init hands that device’s objects together to the one server that holds the entry. They go under the name the server’s entry gives the device: NAME for the register region and NAME-irq for the interrupt, whichever exist. Two entries for one device would let a manifest split it between two holders, and the interrupt’s holder could then mask the other’s device and time its activity. A device name, and a name a server looks a device up by, is at most 60 bytes and may not end in -irq, so NAME-irq never collides and fits the name rule. consoled takes uart and uart-irq, so two machines’ manifests may call the same UART by different names. A devices entry is held by at most one server, and an endpoint is received on by at most one; a manifest naming either twice is refused, confined or not.
• No server gets a budget handle. A servers entry names the budget init creates for the server, never a handle to one; a manifest that grants a server a budget handle is refused (R33 (no server holds a system budget)). root, system and users are reserved: no endpoint takes one of those names, and a receives or handed item that names one is refused as a budget grant.
• Arguments are opaque strings. init passes them unchanged and in order as the startup block’s argv and never interprets them; each server’s page defines its own (keyd’s keys, ipd’s addresses and bucket count). init checks only that each is UTF-8 with no NUL, and that together they leave the startup block inside its page. A badge a server’s arguments name for a caller is that caller’s handed badge, written in both places by the manifest’s author; init mints it from the handed item, never from the argument. Where init calls a server itself (keyd, consoled and bootfsd, at the first endpoint each receives on), its own handle carries the smallest badge from 1 that no handed item there uses; at the steward’s entry it is badge 3, the class the steward accepts blame on, which no handed item may name there (restarts and reboots). A manifest names each of these programs at most once, keyd exactly once: a second would run beside the one init calls, unchecked, and a second keyd could hold keys init never asked about (R35). A program that may run more than once (blkd, one per disk; walfsd, littlefsd or erofsd, one per volume) is told the endpoint it receives on by its argument endpoint=NAME, which the manifest gives it; a blkd‘s must name the endpoint it receives on first, where init mints its volumes’ ranges.
• Volumes. A volumes entry is one GPT entry of its disk, which no other entry names on that disk, and at most one server attaches it, and no entry is handed a badge at the endpoint any blkd receives on (R47 (one volume per instance)). Its disk names the servers entry of the blkd serving its disk: required when the manifest has more than one blkd, and refused if it names no blkd; with one, it may be left out. For the attaching server init mints the range badge, the entry number + 1, at the endpoint its disk’s blkd receives on first, hands it as volume, and adds labels= the volume’s label ids after the entry’s own arguments (none for an unlabelled volume); it gives each blkd one labels.P=ID,... per labelled volume on its disk, P its entry number (blkd). A volume a server attaches without its disk’s blkd, and an entry carrying one of these arguments itself, are refused.
• Verified volumes. A volume with verity is read through its verifier, a verityd entry (verityd): its server still lists the volume, but init mints that server’s volume badge, 1, at the verifier’s endpoint instead of at blkd, and mints the range badge at the disk’s blkd for the verifier, handed as its volume. The verifier gets endpoint= the endpoint it receives on first, labels= the volume’s ids, and root= and blocks=, or, signed, key= and floor=, bundle given in hex as the key the loader verified the bundle with, named so no copy drifts (verityd). Refused, each naming the field: both modes, neither, or a part of one; a root that is not 64 lowercase hex digits, or a block count of 0 or one whose tree does not count in sectors; a key that is neither 64 lowercase hex digits nor bundle; a floor that is not a decimal string (the wrong type); a server naming no entry, or one that is not a verityd; a verifier named by two volumes, or by none; a verifier attaching a volume itself, receiving on no endpoint, or carrying any argument (each is init’s); a verifier whose labels differ from its volume’s; and a handed item at a verifier’s endpoint, since the one badge there is the volume’s range.
• Sizing. Every shared server takes buckets=N as an argument, parsed once in the serving library; none has a compiled-in count. init refuses the boot unless N is at least the number of (account, label set)s the manifest declares (each principal’s unlabelled set and every label set it works under) plus the root badges init mints at that server, one per system caller. It counts every declared domain at every shared server, not only those a session will reach: an over-count costs buckets, and an under-count would bind. So a principal added to the image raises every shared server’s count by its domains: the image’s three principals declare four, and each server’s buckets= is at least those plus its system callers (keyd 6, ipd 7; walfsd:data and erofsd:system need 5 and carry 6, the spare for a case’s extra client; sshd 4, its connections served at once, one channel for each domain (sshd)), within what the server’s own budget holds. init reads buckets=N from a server’s arguments, with the serving library’s parser, and no other argument. So a server’s bucket count never binds in normal use, and a full server cannot tell a latecomer that others hold state (serving). A server whose block has no buckets=N, or one outside 1 to 32, does not start.
• Weights. One stride queue serves every budget (scheduling), so the manifest’s weights are the whole scheduling policy. init, the steward and the drivers (consoled, blkd, netd) get weights an order of magnitude above a session’s (1000 against a principal’s 100), so they are served promptly without running ahead of the queue; the servers that work for principals (bootfsd, the file servers, ipd, keyd, sshd) get ordinary weights and bound the work of one request. The weights carve the system budget like every other limit. The kernel sizes system, not the manifest, and init refuses a manifest whose servers’ pages, processes or weights add up to more than system holds (budgets).
• Devices are matched by address. init asks the kernel which device each of its handles names, finds each devices entry’s base and interrupt among the answers, and the DMA flags must agree (devices).
• What /boot shows. bootfsd serves exactly the entries public names, matched byte for byte, as one flat read-only directory. init pushes their bytes to bootfsd itself (bootfsd), and refuses a public list that names an entry the bundle does not hold, or the manifest. The manifest is never public: it holds keyd’s seeds and every principal’s account and keys.

{ "servers": [ { "name": "walfsd:data", "program": "walfsd", "volume": "data",
                 "budget": { "pages": "4096", "processes": 1, "weight": 100 },
                 "receives": ["walfsd:data"], "args": ["endpoint=walfsd:data", "buckets=4"] } ],
  "principals": [ { "name": "alice", "account": "1001", "labels": ["alice-secrets"],
                    "ssh_keys": ["ssh-ed25519 AAAA..."], "home": "data:/home/alice",
                    "home_quota": "8388608",
                    "net": [ { "prefix": "0.0.0.0/0", "ports": [22, 443] } ] } ] }

A fragment: one file server and one principal.

The attack tests: a manifest that splits a device between two entries, or names a device ending in -irq, is refused; a manifest giving a server fewer buckets than it serves refuses the boot.

Sizing a server when principals are added at run time is the steward’s, in M6 (persist, install, share).

Home quotas

A principal’s home holds at most its home_quota bytes, all its sessions together: the steward carves one connection per principal with it and mints each session’s home through that one (steward). init refuses, naming the field:

• a home without a home_quota, a home_quota of 0, or one with no home;
• a home equal to another principal’s on the same volume, inside it or holding it: the volume’s server would count one under the other’s root, so each would spend the other’s room;
• a volume homes are carved from that gives no bytes, or whose homes’ quotas sum past its bytes: so the steward can carve every principal’s home at once;
• a labelled volume that two principals’ label sets name: a vault is one principal’s, and has no quota of its own, bounded by its volume’s room.

bytes is a promise about the disk that init cannot read: it never sees a partition table. So the disk’s packer refuses a recipe whose manifest gives a volume bytes other than its partition’s size, and the bench refuses a case whose disk and manifest disagree the same way (the test bench). The volume’s server bounds what a carve may take all the same: it refuses a quota its room cannot hold (walfsd), and a session then has no home.

Contexts

A principal’s contexts caps its live contexts in each label set and bounds how long a detached one lasts (steward). init writes both into the principal’s manifest line, contexts=N idle=S. Absent, max is what one label set’s share holds: the share’s pages, less a budget’s own cost, over the steward’s session size, or its processes over a session’s, whichever is fewer, and at most 16; idle_secs is a day, 86,400. init refuses, naming the field, a max of 0, above 16, or above what the share holds, so the cap, not a failed carve, is what refuses a login; a max below 2 for the console principal, whose console session counts against its unlabelled set’s cap and would leave it no SSH context there; and an idle_secs below 60 or above 604,800, a week.

The confinement check

A manifest may set confined, a deployment profile for the whole boot, never per domain. Set, it makes init refuse the boot whenever two entries with differing label sets share any of:

• an endpoint: one name in a servers entry’s receives or handed list both hold;
• a volume: one volumes entry both attach;
• a network instance: one ipd or netd both use (a labelled domain gets no /net at all);
• a device object: one devices entry both hold, since a shared disk or NIC is a shared scheduler, cache and timing surface;
• a server instance: one servers entry serving both.

The kernel and the cores are not on the list. Every label set shares the one kernel, which is the trusted base, and its cores, whose timing is no more partitioned than the caches around them (side channels).

The label set compared is a budget’s labels (a server’s labels, a principal’s label sets) and, for a volume, its volumes entry’s label set. Two sets differ when they are not equal: {a} differs from {}, from {b} and from {a,b}. A system server such as the steward carries no labels, so it is a domain of its own. A confined manifest in which a labelled domain’s principal has a home on a shared unlabelled volume is not refused: the check counts the home’s volume for the principal’s unlabelled domain alone, because the steward binds a home to unlabelled sessions alone under confined, which init tells it as one of its own lines, leaving a labelled session’s home unbound and offering the push; data enters such a domain by an audited push from the steward (steward). So the static half of R34 (volumes, disks, servers, endpoints) is this check’s, and the one dynamic half, which domain a home is bound for, is the steward’s. Every other refusal is a boot failure, not a warning (R34 (confined placement)).

The domains compared are each servers entry, under its labels ({} if none), and each principal’s label sets. A server’s users are the servers handed one of its endpoints, or a volume’s range at it (a volume’s server on that blkd’s disk, or a verified volume’s verityd; the server attaching a verified volume at its verityd, which counts at the verifier’s first endpoint too), and, for a shared server (one that takes buckets=N), every principal domain with the server’s own label set. Only such a domain may later be granted a connection there, since the steward grants within a label set by this same rule, so a server a session may later reach is never missed; a domain with another set is not counted, and the bucket rule still sizes the server for every principal domain. An exempt server (the steward, sshd) handed an endpoint is not counted as its user either. It is not the user: it mints a session’s connection in that session’s scope, and the session is the user. The steward binds a labelled volume only to a session in exactly that volume’s label set (its binding rule, which the model’s routes check and the vault’s exact_labels guard keeps), and the server it mints at admits only a caller whose labels equal its volume’s (R25 (the label check)), so a steward that routed a labelled endpoint to another set would be refused by the server it routed to. The steward itself never reads a vault: a declassification reads through a crossing carrying the item’s labels (R42 (one approved item)). So the exemption says only who is not counted; it widens nothing the steward may route. The kinds are checked in the order listed, and the refusal names the kind. So in a confined boot each disk holds one label set’s volumes, and its blkd carries that set, and each label set reading a verified volume has its own verityd.

The one named exception is the control plane: the steward and sshd may reach across label sets, and only by three kinds of edge: the request and owner-approval path; per-item reader and writer budgets, each carrying exactly one label set and dying after one item (declassification and push); and lease-ending supervision. No shared data server or device is exempt. init checks the declared graph at boot, and the steward enforces the same rule for the budgets and grants it creates later.

It is a check on the manifest, not a run-time invariant: a capability handed over after boot (by mint, by a grant, by a system server) is outside it, and a system server that hands one across label sets is at fault, not the kernel. Without confined, a shared server is ordinary multi-tenancy and the serving library’s residual risks apply.

Starting the servers

The kernel gives init the root, system and users budgets, every device object and the Reset right. The loader maps the bundle into it, read-only (boot). init then:

1. parses and checks the manifest, and refuses the boot on any error, or if what the manifest will cost init does not fit in what root keeps for it (budgets), or if it names more servers than init can watch, one thread each beside its own: at most MAX_THREADS - 1. Until consoled starts, init writes its own lines to the UART, which it maps for itself, each inside the console’s hold (the console’s one writer). A refusal is printed there, and the machine powers off with a system-failure status, before any other process has run;
2. creates every endpoint the manifest’s servers receive on. Each is owned by and charged to root, so it outlives any one instance of its server, and R1 (flow) does not bind it because root is system class (IPC). init keeps the receive right, hands the server a copy, and mints, for each handed item that names the endpoint, a handle with the item’s badge for the server whose entry lists it, and at blkd’s, each volume’s range badge for the server attaching it;
3. starts keyd and runs the key-separation check against it. A manifest with no keyd entry is refused at step 1, since the bundle’s key always needs asking about;
4. unmaps the UART and starts consoled with it. From then on, init writes through its own connection to consoled, and it prints each child’s console connection id when it starts the child (consoled). The check refuses a manifest that hands any server an endpoint consoled receives on: a root badge there writes bare lines, and only init holds one. Without a consoled entry, init keeps the UART;
5. starts the rest of the drivers and the servers below the steward: bootfsd, blkd, each volume’s walfsd, littlefsd or erofsd, netd, ipd and sshd, then pushes the public entries to bootfsd, whose arguments named each with its length from the bundle (bootfsd);
6. starts the steward, the entry steward.server names, after the public entries, since it starts sessions from /boot: handing it the users budget (that entry alone, by name in its startup block; no handed item names a budget), its handed badges at bootfsd, each volume’s server and ipd, through which it asks each server for a session’s fresh connections, and the manifest lines as its arguments, after its entry’s own.

Each server runs in a budget of its own, carved from system, and is started through the loader stub straight from the bundle’s pages, so no file server is needed to start anything. init holds every device and places each driver’s handles, by name, in that driver’s startup block (R33).

sequenceDiagram
    participant L as loader
    participant K as kernel
    participant I as init
    participant S as system servers
    participant KD as keyd
    participant ST as steward
    participant SH as sshd
    Note over ST,SH: planned
    L->>K: verified bundle: kernel and init
    L->>I: the bundle, read-only
    K->>I: root, system, users budgets,<br/>devices, Reset
    I->>I: parse and check the manifest,<br/>make the servers' endpoints
    I->>KD: launch keyd with its keys
    I->>KD: holds(each login, approval and bundle key)
    KD->>I: no (a yes stops the boot)
    I->>S: launch through the stub:<br/>consoled, then bootfsd, blkd, netd, ipd
    I->>S: launch walfsd, littlefsd or erofsd,<br/>one per volume
    I-->>ST: launch, with the users budget
    I-->>SH: launch, with keyd's host-key badge
    SH-->>ST: a login: whose key is this?
    ST-->>ST: carve the session budget,<br/>launch the first session

Figure: the boot from the loader to the first session. Dashed: planned (the steward and sshd).

The attack tests: a manifest whose servers do not fit in system, or whose device entries do not match the kernel’s device objects, is refused before any server runs. The verdict is init’s refusal line, printed when nothing else has run, and the power-off status.

The key-separation check

init refuses a manifest that hands keyd a key the box is authenticated by: a key listed both as a principal’s login or approval key and as a keyd key, or the key the loader verifies the boot bundle with, which init carries as the same compiled-in constant. keyd cannot see either itself: it is given seeds and purposes, not what the rest of the system does with the public keys. init holds no cryptography, so once keyd is started and before anything else runs, it asks keyd holds(public key) for each such key (keyd), and a yes stops the boot (R35 (key separation)).

The startup block

A launcher gives each child one read-only page, the startup block, naming the handles it installed in the child’s slots 1 to n (process_start, processes). process_start’s argument register carries the page’s address; there is no fixed address. The runtime (libs/rt/src/startup.rs) parses it before the program’s main runs, and a program started with no block (address 0) gets an empty one.

The page holds the block’s length as a little-endian u32, then one typed message, startup, laid out as a typed operation written into a file: its opcode as a u32, then the buffer-shape encoding of its fields (wire). The rest of the page is not read.

Checked whole. The parent may be hostile, so the parser bounds everything and checks everything before handing the block to the program: every handle is in 1 to n, paths are unique and clean, names are unique and valid, each bytes field holds whole entries and nothing else, image_addr is 0 exactly when image_len is, is page-aligned, and does not overflow with its length, and the block fits its page. A block breaking any rule is refused whole, and the process exits with code 102 before main runs (R31 (startup block checked whole)).

Using it. resolve(path) finds the namespace entry with the longest matching prefix and the rest of the path; handle(name) finds a named handle; args gives the arguments. The runtime notes the handle bound at /dev/cons for its panic report, caps its heap at heap_pages, and marks its heap record with tag, all before main; budget_pages it gives the program to read. StartupBuilder writes a block for a launcher, and its finish runs the parser on the result, so a launcher can only write blocks a child accepts.

The table: libs/wire/tables/startup.md.

Launching through the loader stub

Every process after init starts the same way, and no launcher parses an ELF: the loader stub (stub/), a small flat binary mapped into the new process, does it there, where a hostile image can hurt only the process it was going to become.

1. The launcher creates the child’s budget and process (process_create) with an exit endpoint.
2. It maps into the child, with process_map: the stub, read-only and executable, at STUB_ENTRY (0x1FF0_0000); a copy of the program’s ELF image, read-write, placed 64 pages at a time; the stack, zeroed, or painted with a pattern the bench reads when the launcher tags it, as init tags each server’s (the memory budget); and the startup block, read-only, naming the image with image_addr and image_len. Where each goes is on memory layout.
3. It starts the child’s first thread at STUB_ENTRY, with the startup block’s address as the argument, installing the child’s handles.
4. The stub reads image_addr and image_len from the block, checks that the image lies clear of the stub and the startup page and is at most MAX_IMAGE_LEN, and plans every PT_LOAD segment before mapping any (stub::plan, pure and allocation-free).
5. It maps each segment at its link address with map_fixed, copies its bytes in, sets its final permissions, unmaps the image copy, and jumps to the ELF’s entry with the startup block’s address in a0. From then on the process is the program.

What the stub refuses, whole, before mapping anything: an ELF that does not parse, is not ET_EXEC, is not RISC-V of the stub’s own width, or has more than 64 program headers; a segment whose bytes reach outside the image, whose pages touch page 0, reach past STUB_ENTRY, or overlap the image, the startup block, the stub or another segment; a segment both writable and executable, or writable without readable; a p_align that is not a power of two or disagrees with the segment’s offset; an entry outside every executable segment. The stub holds no writable data and depends only on redoubt-sys and redoubt-wire.

Exit codes. The stub exits with 110 for a startup block that is missing, does not parse or names no image, or whose image overlaps the stub or the startup block or is over MAX_IMAGE_LEN; 111 for a hostile image, including a segment the kernel refuses to map (one over the stack); 112 when map_fixed is out of memory in the child’s budget; and 101 if it panics. After the jump, the exit code is the program’s.

The stub allocates nothing. It links the wire crate, which declares an allocator, so it installs a zero-sized global allocator, NullAlloc (stub/src/lib.rs), whose alloc returns null and is never reached: the typed decoding the stub uses does not allocate.

The bench’s launcher, stub-launch, and init both launch this way (R32 (a hostile image hurts only its process)).

Fresh connections per child

A launcher never passes its own connection to a child. Every handle in a child’s namespace is a fresh connection the server made for that child with new_connection (wire), rooted where the child’s view of that server begins, and the launcher disconnects it when the child exits (releasing grants). A copied connection would share the launcher’s fids and admission with the child, and the launcher could not free the child’s state without losing its own.

The steward, which launches sessions, is handed a fresh connection in place of the root badge at each server its manifest entry names: init mints the badge, makes the connection through it with new_connection at the badge’s own root, hands the connection and closes the badge. At the steward’s exit init mints the badge again for one call, disconnects the connection, and closes it, so every connection the steward minted under it for its sessions goes too (steward). init holds none of these between the calls. A server that makes no connection, because it mints none (keyd), refuses (a file server whose volume is corrupt) or does not answer within a second, is handed the badge instead, as every server is, and init says so (init: <endpoint> made the steward no fresh connection: the badge is handed): the steward starts and meets that server’s own answers. Only then can a dead steward’s session connections outlive it at that server, if it serves sessions later.

A shared server’s restart strands the steward’s fresh connection there, and every session’s minted under it, in the dead instance’s tables. So after restarting a server, and after the fault’s blame, init makes the steward a new connection at each of that server’s endpoints the steward is handed, as above, waiting up to three seconds for the new instance to serve (a file server recovers its log before it serves, and under a test feature checks its volume: on the image’s data volume the first restart’s recovery measured 589 to 953 ms on both widths, one run past a second unmeasured, and the restarts after it 8 to 71 ms; the bound is twice the measured maximum plus a second’s margin for the run the old bound cut short, rounded up to the next whole second: 2 × 0.953 s + 1 s = 2.9 s, so 3 s, reconnect::SERVER_TIMEOUT), and hands it over with reconnected(server, connection) through its own badge at the steward (the one blame goes on), within the same second a blame waits; the connection replaces the one in init’s list, so the release at the steward’s exit frees the new one. init says how long the new instance took to serve and what became of the connection (init: walfsd:data reconnected for the steward after 812 ms: the steward took it, or lost: the steward did not answer within 1 s, lost: the steward ended, lost: the steward refused it), and a connection the steward did not take is disconnected again: its sessions keep their dead connections there, and the steward stays stranded at that server until its own restart, nothing retried (residual risks). A login that reaches the steward between the restart and reconnected fails its home step and is refused; the person retries. A server that makes no connection within the bound is said too (init: walfsd:data made the steward no new connection within 3 s of its restart), and is stranded the same way. The steward tells its sessions and they re-bind (steward). A restarted consoled is not on this path (residual risks).

Restarts and reboots

• Restart. A server that exits is restarted on the same endpoint. Calls it had taken get Dead (R4b (a server dies)), and clients see the error and retry; senders still waiting on the endpoint are served by the restarted server. The new instance gets the same manifest name, arguments and receive endpoint, but a new startup block: init, as its launcher, disconnects the dead instance’s connections at every server (releasing grants) and mints new ones. The server’s own tables start empty, with a newly drawn first badge (R27 (badge allocation)), so a client’s old connection ids are dead.

• A fresh budget. init destroys the dead instance’s budget and carves a new one from the manifest entry, so nothing the dead instance made or held outlives it (R10 (destruction)). The receive endpoint is init’s, owned by root, so the budget’s destruction does not reach it, and every client’s handle to it stays good. The badges init hands the instance are stamped with its budget (R9 (stamps)), so a copy it passed on dies with it, and the badge minted again for the next instance has no other holder. The steward’s entry alone has its badges, and its console connection, stamped users, so that a session’s or lease’s revocation scope, which lies under users, narrows the connections the steward mints through them (R41 (narrowing by revocation scope)); what the instance stamp bought, the steward’s restart gets below: init disconnects its fresh connections and reaps users to nothing, so no handle the dead steward made or passed on outlives its restart, their only holders being sessions and leases, all under users.

• A driver gets its device handles again from init’s copies. The kernel reset the device at the dead instance’s end, before its DMA pages were reused (devices), and the new instance brings it up from a reset of its own. A driver whose device was quarantined is not restarted: init finds its own copy of the device handle closed, and reboots (devices).

• The boot’s own steps, again. A restart repeats what the boot did after starting that server: keyd is checked again (the key-separation check), init attaches to a new consoled again, and it pushes the public entries to a new bootfsd and seals it again. Until then a client meets the new instance as the boot left it: bootfsd answers “does not exist”, never a half-written entry. If one of these steps fails, init reboots.

• During the boot too. A server that exits before the boot is done is restarted and counted the same way, and a step that was calling it waits for the new instance and tries again. So a server that cannot start reboots the machine by the rule below: consoled refusing a buckets=N its budget cannot hold is one.

• Blame. Each exit notice for a fault names the account and label set of the call the faulting thread was serving (R21 (crash blame)). init passes them to the steward in one typed call, blame(account, labels, server), in the steward’s table, where server is the faulting server’s manifest name for the audit record; the steward’s rule counts by (account, label set) only (steward). The fault line says whom the notice named (init: walfsd:data (PID 9) faulted, code 10, serving account 1002, labels none), and a second line, after the restart, what became of the blame (init: walfsd:data's fault blamed on account 1002, labels none: the steward took it).

• Only init can blame. The steward accepts blame only through a root badge it gives init alone, badge 3 on its endpoint, which init mints for itself at each of the steward’s starts and the manifest check hands to no server: anyone who could send it could have another principal’s sessions ended by forging three crashes.

• Reconnected. After the blame, init hands the steward a new connection at the restarted server (fresh connections), so the sessions the server served get their files back, and a login after the restart its home. The blame goes first because its second must not be spent behind the server’s recovery, which the new connection waits for.

• A wedged steward cannot stall restarts. init restarts the server first, then blames, with a timeout of one second (blame::TIMEOUT, the same as a dead child’s grant releases); a blame lost to the timeout is reported on the console (... : lost: the steward did not answer within 1 s) and counts toward no lockout, and nothing is retried. A fault before the steward runs, or of the steward itself, is reported on the console and blamed on nobody (; blamed on nobody: no steward); a fault whose notice names nobody says so (; blamed on nobody).

• Reboot. More than 5 restarts of one server within 60 seconds, not stopped by blame, reboots the machine: failing closed beats a server that cannot stay up. So does a restart init cannot make: a budget it cannot carve, a badge or console connection it cannot mint, or a launch the kernel refuses.

• The steward is part of the trusted base; its crash is a bug. If it dies, init logs every session out and ends every lease before it starts the steward again, in this order:

  1. The dead instance’s budget is destroyed and carved afresh, as every server’s is (above). The sessions’ process objects are charged to the steward, their creator, so R10 frees them with that budget, their processes killed first and no notice owed: the sessions end there. init disconnects the fresh connections it made for the steward (fresh connections), which frees every session’s connections at the shared servers.
  2. init empties users with budget_reap until no child is left (R10 (destruction)): every principal’s budget, its label sets’ sub-budgets, and their sessions’ and leases’ budgets, endpoints and handles go, one principal’s subtree per kernel entry, the work billed to init. Every session’s VM ends with its budget; an sshd channel stays open until sshd is told (steward). init says init: emptied users: N budgets reaped; a reap the kernel refuses is a restart init cannot make, and it reboots.
  3. The steward starts, finds users empty and carves afresh, and starts the console principal’s session again, as at boot.

  The steward’s own check at its start stays: a steward that finds users holding anything exits, and the reboot rule above is the bound on a steward that dies the same way every time.

stateDiagram-v2
    [*] --> Running: launched through the stub
    Running --> Exited: exit or fault
    Exited --> Blamed: fault notice names<br/>(account, label set)
    Blamed --> Running: steward told,<br/>restarted on the same endpoint
    Exited --> Running: clean exit,<br/>restarted on the same endpoint
    Exited --> Reboot: more than 5 restarts<br/>in 60 seconds
    Reboot --> [*]

Figure: a system server’s restarts. Until the steward runs, a fault is reported on the console and blamed on nobody.

The attack tests: blame from any badge but init’s is refused; a restarted server’s old connection ids are dead; a killed driver, netd among them, is restarted and its clients are served again (netd); more than 5 restarts in 60 seconds reboot the machine.

A worked configuration

Status: planned · M1 (sessions over SSH, kept apart)

Alice and Bob each log in over SSH; Alice has a vault label alice-secrets and an agent, alice/researcher, on a two-hour lease.

kernel
└── init                                              root
    ├── consoled bootfsd blkd walfsd:data walfsd:alice-secrets  system
    │   netd ipd:lan keyd steward sshd
    ├── session alice-1                               users/alice/{}/session-1
    ├── agent alice/researcher [lease 2 h]            users/alice/{}/researcher
    ├── vault session alice+secrets-1                 users/alice/{alice-secrets}/session-1
    └── session bob-1                                 users/bob/{}/session-1

Figure: the budget tree. {} and {alice-secrets} are the fixed sub-budgets, one per label set.

• Weights: Alice 100, Bob 100; the agent 20, carved from Alice’s, sharing her account. init, the steward and the drivers are 1000 each in the same queue.
• The vault session reads and writes walfsd:alice-secrets, reads (never writes) her home on the unlabelled walfsd:data, which is how data enters the vault, has no /net, and prints only to its own channel.
• The agent has its own principal, /work only and no /net; its escalations wait for Alice’s approval, and the lease’s end destroys its budget and everything it passed on.
• No session or lease holds a keyd grant until M6 (persist, install, share): keyd’s purposes are the host key and audit signing.
• Bob crashing walfsd:data three times is blamed on his account each time: his sessions end and he is locked out for a while; Alice is not affected.

Open: none.

Authority

• init holds the root, system and users budgets, every device object, the Reset right and the bundle’s pages. It gives each driver only its own device objects, each server only the endpoints the manifest names, and the steward the users budget.
• It keeps what it needs to restart a server: the receive right of every endpoint it made, a copy of every device handle it placed, and the bundle. It never receives on a server’s endpoint, and it maps no device once consoled has the UART.
• Beside those it holds only its own handle at each server it calls, its own connection to consoled, and each server’s exit endpoint. It closes its copy of every badge it minted for a handed item or a volume’s range, and of each child’s console connection, once the child is started, so it calls as no system caller and writes as no child.
• It holds no keys and no cryptography, and parses no ELF: launching goes through the loader stub, inside the child.
• It has no network and no user data, and after boot it receives only exit notices.
• The loader stub holds nothing but what the child holds: it runs as the child, in the child’s budget, with the child’s handles.

Security properties

R31 (startup block checked whole)

A program runs only with a startup block that passed every rule: handles within what process_start installed, clean unique paths, unique names under the manifest’s rule, whole entries, a well-formed image range. A block breaking one is refused whole and the process exits before main, so a hostile or buggy parent cannot hand its child a namespace the program would read two ways, or a name no rule allows.

R32 (a hostile image hurts only its process)

No launcher parses an ELF. The loader stub, running as the child, refuses an image whose segments overlap each other, the image, the stub, the startup block or page 0, reach past the link range, or ask to be writable and executable, before it maps anything; a segment the kernel refuses (one over the stack) makes the child exit too. So a hostile image can at most exit or fault the process it was going to become. stub-launch launches hostile images on both widths and checks that each only exits or faults the child, that the parent’s budget returns to the same usage after each, and that a well-formed child still runs afterwards and finds the image copy unmapped. A segment the child’s budget cannot hold exits 112, and the same image runs in a budget that holds it. session-hostile-launch launches hostile images from a user’s session, through the launch native (native programs): an image cut to 40 bytes, one cut in half and one of zeros, read from her home, each exit the child 111 with its budget holding nothing; an empty image and a startup block naming a handle outside the rule are the client’s refusals before any kernel call; the session’s processes in use are the same after, and a well-formed program runs. The stub’s parser was fuzzed for an hour; its kept corpus (stub/fuzz/seeds/plan) reruns in the stub’s host tests.

R33 (no server holds a system budget)

Only init and the steward ever hold a handle to a system-class budget. A server’s startup block carries no budget handle, and init refuses a manifest that grants one. A compromised server holding its budget could create system-class children with any labels and any account, and so forge admission keys and crash blame at every other server. The attack test starts a server from a manifest that grants it a budget and expects the boot refused.

R34 (confined placement)

With confined set, no two entries with differing label sets share a server instance, volume, endpoint, network instance or device object, and no labelled domain reads a shared unlabelled volume: a manifest that would place entries so fails the boot, and a labelled session’s home, the one shared unlabelled volume a principal’s domains would share, is left unbound by the steward, which init tells of the profile. The one exception is the control plane: the steward and sshd, by the request and owner-approval path, per-item single-label reader and writer budgets, and lease-ending supervision only. The attack verdict is the boot failing, not the manifest’s claim.

R35 (key separation)

keyd never holds a key that authenticates anyone to the box: not a principal’s login or approval key, and not the key the loader verifies the bundle with. init asks keyd about each before anything else runs, and a yes stops the boot. So the boot root and a key some badge may sign with are never one key, and no badge at keyd can sign a login.

Failure and restart

Status: built · partly tested: the runtime’s exit on a refused block is read from the code, not attacked · tested: bench:stub-launch, host:redoubt-rt::hostile_blocks_are_refused

• A child’s startup block is refused: the runtime exits with 102 before main; the stub exits with 110 if it cannot find the image or the image lies outside its bounds.
• A child’s image is refused or does not fit: the stub exits with 111 or 112, and only the child is affected; its launcher sees the exit notice and the child’s budget returns what it held.
• What init does when a server exits is under restarts and reboots.

Residual risks

• The manifest is a secret held in the bundle. It carries keyd’s seeds, so whoever can read the bundle image holds the box’s private keys; the bundle is signed, never encrypted, and what keeps the seeds off /boot is that the manifest is never public. Sealing the keys to the machine is keyd’s.
• A labelled session in a confined boot still reads code volumes. The check counts no read-only code volume (/boot, the system volume) for a labelled domain, and the steward binds both for a labelled session as for a plain one: a labelled domain reading code it shares with every other is R25 (the label check)’s business, not a flow out; the data volume it would share, its principal’s home, is the one left unbound (steward).
• A confined boot is checked once. Capabilities handed over after boot are outside the check; a system server that hands one across label sets breaks confinement without the kernel noticing.
• Every child pays for a copy of its image. There is no shared text: a launcher copies the ELF into pages charged to the child, and the stub copies each segment again. This is decided, for M1 (sessions over SSH, kept apart) and after. A read-only image-page cache shared between principals is not planned: it would be a cross-principal timing surface (a shared image cache). The steward may still cache an image’s bytes, to avoid reading them again, because each child still gets its own copy.
• A blame can be lost. If the steward does not take init’s blame within its timeout, the crash is reported on the console but counts toward no lockout. A session’s end no longer holds the steward past that timeout: the end is answered once its scope is destroyed, and its ended to sshd and its disconnects are the steward’s cleanup thread’s, each within the client’s call bound, never the loop’s (steward); steward-blame-lockout and steward-server-restart forbid lost for a blame.
• A new connection can be lost the same way. If the steward does not take init’s reconnected within its second, the restarted server’s sessions keep their dead connections and the steward mints no home there until its own restart; init says so and retries nothing (fresh connections).
• The mediators are trusted across labels. The steward and sshd are the confinement check’s one exception; a bug in either reaches every label set they serve.
• The stub cannot see the stack. A segment that names the stack’s pages is refused by map_fixed, but nothing checks for a gap between a segment and the stack (memory layout).
• The startup block’s fuzz target runs outside the bench. Its host tests and the stub’s run in rt-host-tests; the fuzz target needs cargo fuzz, which a host-tests case does not run, so it is run by hand.
• On target, the kernel’s refusal hides the stub’s overlap checks. Dropping one still ends in exit 111, because map_fixed never replaces a mapping; only the host tests pin the stub’s own.
• A restart loop reboots the machine. A client that can crash a server repeatedly without being blamed (a bug the blame rule does not reach) can reboot the box.
• A restarted consoled forgets every server’s console. The servers’ connections lived in the dead instance’s tables, and init has no way to hand a running server a new one, so a server’s lines are refused until it restarts too. init attaches again and says so. The steward alone is handed new connections after a restart, at the servers it is handed (fresh connections); consoled is not among them.
• A console that cannot start reboots silently. init has given up the UART, so its lines about consoled’s restarts and the reboot go nowhere.

Why

• One signed manifest. A boot decided by code is reviewed by reading code; one checked file is reviewed by reading the file, and a rule it breaks stops the boot before anything runs.
• The stub, not the launcher, parses ELF. An ELF parser is a large surface on hostile input. Run inside the child, a bug in it compromises only the process being made, never init or the steward, which launch everything.
• The startup block as one typed message. A second framing format would need its own parser and fuzzing; the typed-message codec is already both. The parent writes both sides, so checksums would protect nothing.
• Strings for 64-bit numbers in the manifest. Every JSON tool agrees on integers up to 2^53; an account or a page count written as a string is read the same way by every tool.
• A fresh connection per child. A launcher that could not free a child’s state without freeing its own would leak every dead child’s fids for its own lifetime.
• Reboot on a restart loop. A server that cannot stay up is a server whose rules are not being enforced; stopping the box is the closed failure.