Platform
Built from the job down.
You write your application in Rust. NoWayOS builds it, with only the drivers it uses, onto the seL4 microkernel. The image that comes out holds that, and nothing else.
From application to image
A NoWayOS device is built, not configured. Four steps take your code to a device that does its one job, and each step leaves something you can check.
Write the application
In Rust, as one or more protection domains. Build its screens with NoWayOS's small declarative UI core, or design them in React and convert them at build time with the Screen Compiler.
Describe the system
A Microkit system description declares every protection domain, memory region, channel and interrupt. Beside it, a grants file lists everything the system grants, and an expect file lists what it must print when it runs.
systems/hello.system systems/hello.grants systems/hello.expectBuild it
In the dev container. The build checks the grants against the description, then writes the image with its software bill of materials and a record of its seL4 configuration.
make image SYSTEM=helloBoot it, and let it check itself
In QEMU first: the system boots headless and must print every line its expect file lists, in order, and nothing the file forbids. Then on the Raspberry Pi 5, checked against the same file.
make qemu-test SYSTEM=hello
Sealed compartments
Each part of a NoWayOS system (the screen, the input, the network, your application) runs in a protection domain of its own on the seL4 microkernel. A protection domain has its own memory and holds only the capabilities its system description grants it: a capability works like a keycard for one door. seL4 enforces them, so a part reaches only what it was given, and a bug in one part is designed to stay in that part.
- A supervisor receives the other parts' faults, stops the part that faulted and restarts the system clean. When faults keep coming, the device enters a fail-safe state, and only a cold start brings it back.
- A watchdog protection domain services the hardware watchdog only while every other part answers its heartbeat.
- Roles limit what each part may be given: the build refuses a grant that a part's role must never have, such as a device for a part that should only draw.
Typed messages, copied before they are checked
Protection domains talk through fixed-size, versioned records with an explicit layout, passed on single-producer rings over shared memory. Every record is copied out of shared memory before it is checked, so the sender cannot change it between the check and its use.
Every parser of outside input is fuzzed and built never to panic, and every message decoder has bounded proofs, made with the Kani model checker.
A native screen, and no browser
The user interface is a small declarative core: layout, focus and hit-testing in bounded memory, drawn with the Rust library embedded-graphics and repainting only what changed. Text comes from glyph atlases drawn in advance at build time, so the device never parses a font file. Applications see key, pointer and touch events, never USB or any other device protocol.
Designers can keep working in React. The Screen Compiler converts screens written to its supported subset into Rust at build time, and refuses anything outside the subset rather than approximating it.
What's inside
| Area | What NoWayOS gives you |
|---|---|
| Runtime | Protection-domain patterns on Microkit and rust-sel4; a supervisor that stops a faulted part and restarts the system clean, with a fail-safe state after repeated faults; a watchdog |
| Messages | Typed records with an explicit wire layout, and single-producer rings over shared memory |
| Drivers | Display (QEMU's ramfb, the Raspberry Pi 5's framebuffer); input (virtio, USB keyboards, mice and tablets); network (virtio-net, the Pi 5's Ethernet); USB host (xHCI); UART; timers; the Pi 5's fan |
| Networking | An IP stack on smoltcp with DHCP and TCP, connecting only to the destinations a system allows; a TLS 1.3 client on rustls and RustCrypto |
| Time and trust | Monotonic and wall-clock time as types that never mix; ECDSA P-256 signature checks; the records of signed updates; seeds from a health-tested hardware random source |
| User interface | A bounded declarative UI core with layout, focus and hit-testing; a renderer on embedded-graphics; glyph atlases and icons drawn in advance |
| Tooling | The dev container; make fragments that product repositories build with; the grants, unsafe, licence and secrets checks; SBOM and release-evidence tools; QEMU and Raspberry Pi runners |
Hardware
| Where | Its role |
|---|---|
| QEMU (AArch64) | Every system boots here first, inside the dev container, and checks its own output |
| Raspberry Pi 5 | The low-cost reference board anyone can buy. The user interface, USB input, timers and the watchdog run on it today |
| NXP i.MX8 | The intended production hardware, with a hardware root of trust. Not yet supported |
NoWayOS is developed on Apple silicon (arm64) machines. x86-64 hosts are not yet tested.
Built on
NoWayOS stands on other people's work, and says so: seL4, Microkit, rust-sel4, the seL4 Device Driver Framework's network queues, smoltcp, rustls, RustCrypto and embedded-graphics.