Your first system in QEMU

A NoWayOS system is a set of protection domains, the parts of a device, booted together on seL4. Every system boots in QEMU first, inside the dev container, and checks its own output. This page boots the smallest one, then a few that show more.

Boot hello

make qemu-test SYSTEM=hello

This builds the hello system, checks its grants, boots seL4 headless in QEMU and watches what it prints. It passes when every line the system must print has appeared, in order, and nothing forbidden has.

To boot it yourself and watch, run make qemu SYSTEM=hello. Quit QEMU with Ctrl-A, then x.

The three files that define a system

Each system is three files in systems/, beside the Rust code in pds/.

hello.system is the Microkit system description: every protection domain, memory region, channel and interrupt the system has. hello has one protection domain and nothing else:

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

hello.grants lists everything the system grants, one fact per line. The build fails if the description grants anything not listed here, or lists anything it does not grant, so a change to what a system may do is always visible in review:

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect lists the lines the system must print, in order, and, after a !, text that fails the test at once wherever it appears:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

The same expect file checks the system on a Raspberry Pi 5, from the board's serial log.

The protection domain itself

pds/hello/src/main.rs is the whole program. It follows the minimal shape of rust-sel4's Microkit example: init runs once at start, and the handler would receive notifications if the system gave it any channels.

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

There is no heap (any allocation would fail to link), no unsafe and no device. Printing works only because this is a debug build: a release kernel has no debug console.

Watch seL4 stop a part

make qemu-test SYSTEM=isolation-test

Two probe protection domains each try something they were not granted: one reads memory that is not mapped into it, the other writes to a page it may only read. seL4 stops each one with a fault, and a bystander keeps running untouched. The test's last line says so:

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

More systems to try

Run any of them with make qemu-test SYSTEM=NAME, or every system with make qemu-test-all.

Click through the user interface

make qemu SYSTEM=ui-interactive VNC=1

QEMU's screen is published over VNC on your machine's localhost:5900, with a password printed for that run only. On macOS, open vnc://localhost:5900 (in Finder: Go, Connect to Server) and click through the demo screens.

What the build leaves beside each image

In build/BOARD/SYSTEM/ (for these, build/qemu_virt_aarch64/hello/ and so on), next to loader.img:

• sel4-config.txt: the image's seL4 configuration, and whether it is inside seL4's proofs. A debug build says plainly that it is not. See Security.
• sbom.cdx.json: a CycloneDX software bill of materials for the image: the kernel, the loader, each protection domain and the crates in it, each with its hash.
• The licence files of what the image contains, such as the font and icon licences.