The words, in plain English.

Everything an attacker could try to use against a device: its code, services, interfaces and inputs. Less code and fewer features leave less of it.

A device proving to a remote service, cryptographically, which software it started. It shows what was loaded at boot, not everything that has happened since. Planned for NoWayOS on production hardware; not yet built.

A proof that a property holds for every input up to a stated size. NoWayOS proves its message decoders this way, with Kani.

In seL4, an unforgeable token naming one kernel object and the rights held over it, like a keycard for one door. A protection domain can touch only what its capabilities name.

In Microkit, a declared connection between two protection domains, for notifications (signals with no data, interrupts among them) and protected procedure calls.

A start from power off, as opposed to a reset. Only a cold start brings a NoWayOS device back from its fail-safe state.

The rule that a message is copied out of shared memory before it is validated, so the sender cannot change it between the check and its use. It prevents a double-fetch.

An open standard format for software bills of materials. NoWayOS writes one for every workspace and every system image. See SBOM.

Raspberry Pi's USB-to-serial adapter. On the Raspberry Pi 5's debug connector it carries the boot log and loads test images.

The pinned container image that holds NoWayOS's whole toolchain: the Rust toolchains, the Microkit SDK, QEMU and the checking tools. Every make target runs in it, so your machine needs only Podman and make.

A bug in which code checks data in shared memory and then reads it again, letting the other side change it in between. Prevented by copy, then check.

A Rust 2D graphics library for devices with no operating-system graphics stack. NoWayOS's user interface draws with it.

systems/NAME.expect: the lines a system must print, in order, and the text that fails the test if it appears anywhere. The same file checks a system in QEMU and on the Raspberry Pi 5.

Where a NoWayOS device goes when faults keep coming: only the supervisor, the watchdog and, where possible, the display keep running, until a cold start.

What seL4 reports when a protection domain does something the kernel will not allow, or panics. The part stays stopped until its fault handler acts.

Mathematical proof, checked by computer, that software meets its specification. seL4 has it for specific configurations. NoWayOS's own code relies on Rust, isolation, testing and bounded proofs instead.

Testing a parser with millions of generated inputs until one crashes it or breaks a check. Every NoWayOS parser of outside input has a fuzz target.

A font drawn in advance, at build time, into images of its characters, so a device draws text without ever parsing a font file.

systems/NAME.grants: everything a system grants, one fact per line: priorities, budgets, memory, devices, interrupts and channels. The build fails if the system description and the grants file disagree.

NXP's family of industrial Arm processors, and NoWayOS's intended production hardware. Not yet supported.

A system that tries to reach what it was not granted, which seL4 must stop. A variant with a grant widened on purpose must fail, which shows the test can fail.

A model checker for Rust that proves properties for every input up to a bound. NoWayOS uses it to prove that its message decoders never panic, overflow or read out of bounds.

A mistake such as reading past the end of a buffer or using memory after it has been freed. Microsoft and Google have each reported that around 70% of their serious security bugs are of this kind; safe Rust rules them out.

A kernel kept as small as possible, with drivers, networking and the screen running outside it, each in its own compartment. seL4 is one.

The seL4 Foundation's framework for static seL4 systems built from protection domains declared in a system description.

An interpreter for Rust that detects undefined behaviour. NoWayOS runs it over the few crates allowed unsafe code.

The configuration of seL4 with scheduling budgets and periods, which Microkit builds. Its AArch64 proofs are in progress, so no NoWayOS image is inside seL4's completed proofs today.

Time counted from boot, never set and never going backwards. Every NoWayOS timeout uses it, and it never mixes with wall-clock time.

One isolated part of a Microkit system: a program with its own memory, holding only the capabilities it is explicitly granted. NoWayOS's sealed compartments.

An open-source machine emulator. Every NoWayOS system boots in it, and checks its own output, before it touches hardware.

The low-cost board NoWayOS uses as its reference hardware.

A programming language whose safe code rules out memory-safety bugs. NoWayOS's own code is Rust throughout.

The seL4 Foundation's Rust support, including the crate for writing Microkit protection domains.

A TLS library written in Rust. NoWayOS's TLS 1.3 client is built on it, with RustCrypto.

A software bill of materials: a list of every component and version in a piece of software. NoWayOS writes one in CycloneDX for every workspace and every system image.

NoWayOS's build-time tool that converts React screens, written in TSX to a supported subset, into Rust for NoWayOS's user interface. It refuses anything outside the subset rather than approximating it.

The seL4 Device Driver Framework: a reference design for drivers on Microkit, using shared-memory queues. NoWayOS's network queues follow it.

A device refusing to start software not signed by its maker. Planned for NoWayOS on production hardware; not yet built.

Making a general-purpose device safer by changing its settings. The features are still there, and one bug can bypass every setting.

Making a device that cannot do the risky things because they were never built in. NoWayOS's approach.

A microkernel of about 10,000 lines, maintained by the seL4 Foundation, with machine-checked proofs of correctness and security for specific configurations. NoWayOS runs on it.

The record written beside every NoWayOS image: its seL4 configuration, and whether that configuration is inside seL4's completed proofs.

An operating system built for one device's one job, rather than built to run anything and then locked down to one thing. Three things make one: it is built for one job (its image holds the application, the drivers it uses and the kernel, and nothing else); it is sealed inside (each part in its own compartment, reaching only what it was granted); and it shows its working (the evidence of what is inside comes with it). Not kiosk mode, which locks a secure by configuration system to one app. NoWayOS is a Single Purpose OS: a computer with nothing else to do.

A TCP/IP stack in Rust that allocates no memory as it runs. NoWayOS's network stack is built on it.

The protection domain that receives the other parts' faults, reports them and restarts the system clean.

The Microkit XML file that declares every protection domain, memory region, channel and interrupt of a system. It is the system's security design, and a change to it is reviewed as one.

Everything a security property depends on being correct. For a NoWayOS system: the seL4 kernel, the Microkit loader and monitor, and the protection domains that property relies on.

A fixed-size record with an explicit layout, passed between protection domains through shared memory and checked on receipt. See copy, then check.

Rust code the compiler cannot check for memory safety. Forbidden in every NoWayOS crate except a short, reviewed list that CI enforces.

The date and time of day, from an authenticated source. NoWayOS keeps it apart from monotonic time, as a different type.

A hardware timer that resets the board unless software services it. NoWayOS's watchdog protection domain services it only while every other part answers its heartbeat.