How a system fits together

Every NoWayOS device is a system: a fixed set of parts, declared before it is built, each sealed off from the others by seL4. Nothing is added at run time. This page explains the pieces and how they connect.

Protection domains

A protection domain is one part of a system: a program with its own memory, holding only the capabilities it is granted. In seL4 a capability is an unforgeable token naming one kernel object and the rights held over it, like a keycard for one door. A protection domain can touch nothing its capabilities do not name, and seL4 enforces that.

A typical system has a protection domain for each concern: a display driver, the input path, the network stack, the user interface, the application, a timer, a supervisor and a watchdog. Each is a small Rust program, no_std, that allocates nothing after it starts.

The system description

The Microkit system description (systems/NAME.system, an XML file) declares the whole system: every protection domain with its priority, budget and stack; every memory region and who maps it; every channel; every interrupt.

• Descriptions name devices, never addresses: phys_addr="@NAME". The addresses come from the board's file in platforms/, each with its source, so the same description builds for QEMU and for the Raspberry Pi 5.
• Channels connect two protection domains, for notifications (signals with no data, interrupts among them) and protected procedure calls (synchronous calls into a higher-priority part).

The description is the system's security design, so a change to it is reviewed as a security change.

The grants file

Beside each description, systems/NAME.grants lists everything the system grants, one fact per line: priorities, budgets, memory, devices, interrupts and channels. The build fails if the two disagree in either direction.

Each protection domain also has a role (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock or test), and the build refuses a grant that its role must never have. A user interface cannot be handed a network device by mistake, and a test instrument cannot slip into a product.

Typed messages

Protection domains talk through typed messages: fixed-size, versioned records with an explicit layout, passed on single-producer, single-consumer rings over shared memory.

• Copy, then check. A receiver copies each record out of shared memory before validating it, so the sender cannot change it between the check and its use (the bug called a double-fetch).
• Decoders cannot panic. Each decoder returns a typed error for anything malformed, and has bounded Kani proofs and a fuzz target.
• Each side has its own view. The producer and the consumer see the ring through separate memory views, and shared indices use acquire and release ordering.

Input

Applications see canonical input events, keys, pointer movements and touches, checked against the screen and rate-limited. They never see USB or any other device protocol; the input path parses those in protection domains of its own, treating every byte as hostile.

Faults, the supervisor and the fail-safe state

When a protection domain does something seL4 will not allow, or panics, seL4 stops it and reports a fault to its parent.

• The supervisor is the parent of the other parts. It receives each fault, reports it, and resets the board so the system starts again clean. It is built and tested in QEMU test systems.
• The fail-safe state is where a device goes when faults keep coming: by default, at the fourth restart since a cold start, or at the second fault in a security-sensitive part such as storage or updates. Only the supervisor, the watchdog and, where possible, the display keep running, and only a cold start, from power off, brings the device back.
• The watchdog protection domain services the hardware watchdog only while every other part answers its heartbeat. If one stops answering, the hardware resets the board.

Memory and time

• Memory is fixed when the image is built. Device code allocates nothing: every buffer and queue has a set size, from nowayos-bounded. The one exception, the TLS client, works in a fixed arena of its own.
• Two kinds of time that never mix. Monotonic time counts from boot and never goes backwards; every timeout uses it. Wall-clock time, the date and time of day, comes from an authenticated source. They are different Rust types, so one cannot be passed where the other is meant.

Building your own systems

Your product's own systems and protection domains live in a repository of their own, beside nowayos, never inside it. That repository's Makefile sets SYSTEM_REPO := $(CURDIR) and includes NoWayOS's make fragments:

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

Then make image, make qemu-test, make qemu-test-all and the checks work on its systems/ and pds/, with NoWayOS's dev container, board files, grant rules and checks. The variables are documented at the top of tools/make/system.mk. The Showcase is built exactly this way.