M1 (sessions over SSH, kept apart)

Goal

Alice and Bob log in over SSH, on QEMU, and on the console, into Elixir sessions, and are kept apart: each session runs in a fixed sub-budget for its principal’s label set, with files (the system read-only, /home writable). A dead steward restarts without a reboot, and the scheduler’s targets hold. The attack suite is the kernel cases below and the cases for what this milestone builds.

The milestone is one thin vertical slice through the whole system: the kernel, init and the boot manifest, the drivers, the file servers, the steward, keyd and sshd, and beamlet running the shell in each session. A session in this milestone needs only the console, files and launching native programs. The rest of the shell is M2 (usable shell); agents, approvals and the scripted hostile agent and user are M3 (agents, approvals and the attack suite).

Attack suite

Each attack is a deterministic program in the test bench. Its outcome is judged by a party the attacker cannot impersonate: the kernel, a victim, or a clean power-off, never the attacker’s own output (rule F). A covert channel an attack finds is recorded as an observation against the side-channel wall, not as a breach.

Kernel cases

The gaps the kernel’s own cases leave (R1 (flow) across label sets on the real kernel, R2 (fair waiting)’s turns between groups, completion races between harts) are listed in kernel attack gaps.

Remaining work

Each part lands with the attack cases for what it builds. The order the parts run in, and which are under way, is kept with the project’s work plan (AGENTS.md), not on this page.

• The client library. redoubt-client: the namespace, files over 9P, the file server’s typed operations, the console, launching, a launcher’s grants and one typed call, the API every userland binds to, tested on the host against real servers (native programs). init and beamlet’s platform are built on it, and an Rerror keeps its name by one table (wire); a session binds each typed server through a generated Elixir client (wire). Still planned: dropped files’ fids that come back, calls by path, and whole reads and writes (native programs).
• The VM’s remaining platform work. The VM and shell boot on the UART console, and its I/O is asynchronous through the client library’s hub, files over 9P included (beamlet, files), and its system natives (the namespace, typed calls, serving, budgets, labels and launching) run on the machine in a session a tester starts in the steward’s place, and budgets and launching in the steward’s own sessions over SSH, a vault session’s among them (beamlet); Elixir’s File in a steward’s session waits for the session’s namespace to reach its VM.
• The steward. Principals from the manifest, fixed sub-budgets per label set, and sessions on the console and over SSH run (the steward, sub-budgets, sessions), on the server graph, trust tiers and capability holdings (the servers). Still to come: a dead steward restarts without a reboot: init empties the users budget, which ends every session, and relaunches the steward (the steward, init).
• Files. The system volume read-only, and /home writable, served by walfsd (walfsd).

Every follow-up page is placed above.

Progress

Built and attack-tested today:

• The kernel, except SUM and MXR clearing: handles and objects, IPC, memory, budgets, scheduling, the timer, processes, devices and DMA, verified boot (the kernel), and the executable model with its mutations (the model).
• The kernel containment gate: hostile leases preempted, ended at their deadlines and revoked by hand with their calls and lends in flight, while the victims stay responsive, on both widths (containment).
• The serving library and the wire formats: admission, the label check, minted connections, parked calls, typed dispatch, the 9P skeleton (serving, wire).
• The drivers and the network: blkd and netd attacked by hostile devices in host tests, blkd, netd and ipd on the real kernel under init (blkd, netd, ipd).
• The file system’s core: littlefs against a hostile medium and power loss (littlefsd).
• The flash file server: littlefsd over blkd, placed by init, with one volume per instance, quotas and typed operations (littlefsd).
• walfs, the format for the SSD’s writable volumes: its library against a model, a power cut at every write and hostile volumes, the bench’s packer, and its server, walfsd, serving the image’s data volume under init, with a power cut on the machine before or after (walfsd).
• bootfsd, consoled and keyd, attacked in host tests and booted under init (bootfsd, consoled, keyd).
• Launching: the startup block and the loader stub (init).
• init and the boot manifest: the loader loads only the kernel and init; init checks the manifest, builds the budget tree, hands each server its devices, and starts every server through the loader stub with fresh connections. It restarts a server that ends, a driver on its reset device, and reboots when one cannot stay up. Every server’s case boots init (init, starting a case’s programs).
• The client library, with launching exercised by init-boot on the machine and its other tested operations exercised on the host against real servers (native programs).
• beamlet on the host and under init on Redoubt, with console, clock and randomness; its modules come from the userland disk, a volume verityd checks block by block against a root the signed manifest pins, those the shell’s prompt loads from one boot pack read whole before the VM starts (beamlet, verityd). Its I/O is asynchronous through the client library’s hub, and its files are 9P files in its namespace (files).
• The shell on beamlet on the host: the loop, the commands, the file and text commands and help, with hostile text drawn visibly and the cell protocol held to its vectors (the shell, the cell protocol). The shell also boots on Redoubt’s UART console, and in a session its exec launches a native program from /boot (native programs); its files wait for a session’s namespace (the shell on the machine).
• The steward: its policy core, tested on the host, and the server, which carves the principals from the manifest, logs in sshd’s users and starts each session as a beamlet VM in its label set’s sub-budget, and the console principal’s on the UART (the steward). A steward that dies is restarted with every session logged out, users emptied by the kernel’s budget_reap, and the console session starts again; the machine does not reboot (failure and restart). Each principal’s home holds the manifest’s quota, shared by all its sessions, its console session among them (home quotas and vaults).
• sshd’s core on its host platform, which the bench’s SSH sessions run against, with OpenSSH’s server as the reference (sshd, SSH sessions), and on the box’s, logins through the steward (sessions over SSH).

Not built: a session’s files, and a steward restart without a reboot.