Beyond M6
Ideas past the plan. None is a goal: the hard goals are M1 (sessions over SSH, kept apart) through M6 (persist, install, share), and nothing here is built toward until the owner makes it one. Each page says what the idea is, why it is not a goal, and what it would need, including the attack cases it would have to pass. Some are kept so they are not redesigned from scratch; some are recorded as ruled out, with the reason, so they are not proposed again without one.
| Page | The idea |
|---|---|
| The FPGA platform | Redoubt on softcores: a DE10-Nano scale model and a Kintex-7 PCIe card with DMA confined in hardware |
| The card’s host backend | one locked-down Rust process serving the card’s console, disk and network over VFIO, never parsing a guest pointer |
| rv32 | the full stack on 32-bit RISC-V, booted in every milestone |
| Other runtimes | Python and Java, ported to Rust |
| The web stack | serving HTTP through isolated TCP, TLS and HTTP servers, reached only through SSH forwarding |
| Unattended operation | backup, crash records, field updates, monitoring and a rescue console |
| Swap | a userspace swapper under per-budget limits |
| Disk encryption | authenticated encryption of every block, for a disk outside the trust boundary |
| Linux on reserved cores | Linux driving messy hardware and serving virtio to Redoubt |
| IOMMU | hardware confinement of DMA through an IOMMU or IOPMP |
| An OS debugger | a debug capability and a GDB server, never issued in production |
| A shared content store | packages stored once for everyone, by hash (ruled out as a channel) |
| A shared image cache | program images shared read-only between principals (ruled out as a channel) |
| The link layer | VLANs, rate limits and routing, in linkd and routerd |
| A browser GUI | a desktop in the browser (conflicts with the no-GUI non-goal) |
| Hardware approval | high-stakes approvals signed by a FIDO key |
| ASLR | randomised address-space layout |
| Scheduling extensions | time donation and CPU quotas |
| Label extensions | taint-on-read and integrity labels |
A direction, the owner’s: the system-call ABI is kept free of the MMU (a transport trait, lends and transfers stated as ownership), so that a backend without one, cooperative and in one process, could implement it. Nothing builds that backend.