Getting started

Build NoWayOS's dev container and run its clickable demo, every frame checked, with no hardware and no seL4 knowledge needed.

NoWayOS builds inside one pinned dev container, so your machine needs very little of its own. This page takes you from nothing to the demo running. The next page boots a real seL4 system in QEMU, and a later one puts it on a Raspberry Pi 5.

What you need

Podman and GNU Make. Docker works too: add ENGINE=docker to each make command.
git, to clone the repositories.
No Rust and no seL4 tools on your machine. The Rust toolchains, the Microkit SDK and QEMU are all inside the dev container, pinned to exact versions.

On macOS, Podman runs containers in a virtual machine. Create and start it once, giving it a few CPUs and several gigabytes of memory, for example:

podman machine init --cpus 4 --memory 8192
podman machine start

NoWayOS is developed on Apple silicon (arm64). x86-64 hosts are not yet tested.

Give NoWayOS a folder of its own

The dev container mounts the folder above your clone, so that repositories cloned side by side can build against each other. Make a folder for them first:

mkdir nowayos && cd nowayos
git clone https://github.com/NoWayOS/nowayos.git nowayos
cd nowayos

Build the dev container

make container

This builds the pinned dev image: the Rust toolchains, the Microkit SDK, QEMU and the checking tools. The first build takes a while. Run it again whenever tools/container/Containerfile changes; every other target refuses to run on a stale image and tells you so.

Run the demo

make demo

The demo is a small form application with a scripted session of taps, clicks and keys. It runs as a host simulation, with no seL4 and no QEMU, and draws every step's frame with NoWayOS's real UI core and renderer. Each frame is compared with an approved image, and the run ends:

demo: PASS - … steps, every frame as approved

If any frame differs by a single pixel, the run says which step and fails.

Look around

make # every target, with a line on each
make test # unit, property, doc and golden-image tests
make lint # rustfmt, then clippy with warnings as errors

Every target runs in the dev container and starts it for you. The repository's DEVELOPING.md lists them all, with the layout of the code.

If something goes wrong

error: … was not built from the current … Containerfile: the container's definition has changed since you built it. Run make container again, as the message says.
Podman cannot be reached: on macOS, start its virtual machine with podman machine start.
A build runs out of memory: give Podman's virtual machine more memory. The whole gate, make ci, runs model-checking proofs that need far more than the demo does (Checks and evidence).