Security
It minds its own business.
A NoWayOS device leaves out what its job doesn't need and seals what remains in compartments. This page sets out what that rests on, what is proved, what isn't yet, and what stays yours to get right.
What is left out
A NoWayOS image holds its application, the drivers that application uses, and the seL4 microkernel. There is no browser engine, window system, shell, package manager or user account: none was ever built in, so none is there to exploit, patch or misconfigure. NoWayOS is designed to reduce unnecessary software and services: if the job doesn't need it, it isn't in the image.
That is the meaning of the name: no way to exploit what was never built in. It is a statement about what is absent, not a promise that nothing can go wrong. What is built in can still have bugs; the claims are that there is far less of it, and that a bug stays in its compartment.
Locking down a general-purpose system is secure by configuration: the locked-away features are still present, and one bug can bypass every setting. NoWayOS aims to be secure by construction: the features were never there.
How a fault is contained
- Each part runs in its own protection domain, with its own memory, holding only the capabilities its system description grants. seL4 enforces them.
- Every grant is listed in the system's grants file, and the build fails if the description grants anything the file doesn't list, or the reverse. Widening a grant is reviewed as a security change.
- Messages between parts are fixed-size records, copied out of shared memory before they are checked, so a sender cannot change a record after it has passed.
- Input is hostile until checked. Every parser of outside input is fuzzed and built never to panic, and applications see key, pointer and touch events, never device protocols.
- A supervisor stops a part that faults and restarts the system clean. Repeated faults put the device in a fail-safe state until a cold start.
What seL4's proofs cover, and what they don't
seL4 is a microkernel of about 10,000 lines, with machine-checked proofs of correctness and security. The proofs are a rare achievement, and they hold for specific configurations on specific platforms. This is the exact position:
NoWayOS runs on the seL4 microkernel, which has machine-checked proofs of correctness and security for specific configurations on our hardware; NoWayOS uses seL4's mixed-criticality configuration, whose proofs are in progress.
- Platform: seL4's AArch64 verified configuration lists the Raspberry Pi 5 and NXP's i.MX8M Mini, Plus and Quad.
- Scheduling: Microkit builds seL4's mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress. So no NoWayOS image is inside seL4's completed proofs today.
- Cores: the proofs are for single-core kernels. An image that uses several cores is outside them, and says so.
- Above the kernel: Microkit's tooling and NoWayOS's protection domains and drivers are not covered by seL4's proofs. Their assurance comes from Rust, isolation, review, testing and NoWayOS's own bounded proofs.
Every image records its configuration in a sel4-config.txt beside it. Here is what the record for a development build of the hello system says about itself:
system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list
Even an image whose kernel matched every option of the verified configuration would not be called “verified” here. The record states the facts, and the facts are enough.
The evidence, and the command for each
Every claim on this page comes with its evidence, and every piece of evidence comes from a command anyone can run in the dev container. make ci runs them all, in order; Checks and evidence explains each.
| The claim | The evidence | Run it |
|---|---|---|
| Every grant is written down. | Each system's grants file, checked against its system description at every build. | make qemu-test SYSTEM=hello |
| A part cannot reach what it was not granted. | Isolation tests whose probes make ungranted reads and writes, which seL4 must stop, and a variant with a grant widened on purpose, which must fail. | make qemu-test SYSTEM=isolation-test |
| Message decoders hold for every input up to a bound. | Kani proofs of every message-record decoder, with mutation checks that show the proofs can fail. | make kani |
| Parsers of outside input survive hostile input. | A fuzz target for every parser of untrusted input. A crash, once fixed, becomes a regression test. | make fuzz |
| Unsafe code is only where it is approved. | An allow-list of the few crates and files that may use it, enforced in CI, with Miri run over those crates. | make unsafe-audit |
| Every component is known. | A CycloneDX software bill of materials for every workspace and every system image, each component with its hash. | make image-sbom SYSTEM=hello |
| Licences and advisories are checked. | cargo-deny over every workspace: licences, sources, banned crates and known advisories. | make deny |
| There are no secrets in the code. | The tree and every commit scanned, offline, for keys and credentials. | make secrets |
| Each image's seL4 configuration is on record. | A sel4-config.txt beside every image, and a check that the record's reference values match the pinned Microkit SDK. | make sel4-config-check |
What stays yours
NoWayOS is a platform, not a certified product. A secure device also depends on how it is deployed and run, and that part belongs to whoever builds and operates it.
- Physical security. A plugged-in device or a hand on the power cable can still take a device out of service. Enclosures, ports and power belong to the design of the product built on NoWayOS.
- What each system grants. NoWayOS checks that a system and its grants file agree. Whether those grants are right for the job is a design decision, and should be reviewed as one.
- Networks and back ends. A device connects only to the destinations its system allows. What those services do with what they receive is theirs to secure.
- Keys and updates. Signed updates that fall back safely are designed, not yet built. Who holds the signing keys, and how a release is approved, is an operating decision.
- Certification. Regulated products running on NoWayOS carry their own certification. NoWayOS is designed to supply the evidence they need; it is not certified itself.
Not built yet
- Secure boot and attestation belong to production hardware with a hardware root of trust. Neither is built.
- Signed updates applied on the device. The update records and their checks exist; the path that applies an update on a device does not, yet.
- The Raspberry Pi 5 is a development board, not a hardened device. Someone holding one can swap its software, and the memory access of USB devices is not yet confined on it.
Words you won't find here
We don't call NoWayOS “unhackable”, “tamper-proof” or “bulletproof”, and we don't claim a “zero attack surface”. Nothing is, and you would be right to stop reading. The claims on this page are smaller than that, and each comes with its evidence.
Reporting a vulnerability
Please report a vulnerability privately, as the SECURITY.md file in each repository describes, and not in a public issue. Because each part runs in its own compartment, a flaw is designed to stay where it is while a fix is made.