We attack our own build on every change

Here's an uncomfortable question for any security test: has it ever failed? A test that has never failed might be passing because the system is sound, or because the test can't see anything at all. From the outside, the two look exactly the same.

So NoWayOS doesn't just test its security. It attacks it, on every change, and checks that the attacks are caught.

Reaching for what isn't yours

Each part of a NoWayOS system runs in its own compartment on seL4, holding only what it was granted. The isolation tests send probes across those boundaries on purpose. One reads an address it was never given. One writes to a page it may only read. One, holding exactly what the user interface holds, tries to write the display's control page, which the interface may only read. Another, holding exactly what the network client holds, tries to write into the network driver's memory.

seL4 must stop every one of them, and a bystander part must carry on running, untouched.

A test built to fail

Then comes the twist. Beside the user interface's isolation test sits a variant with one grant widened on purpose: the interface's stand-in is given the display's private page. That variant's test must fail. If it ever passed, the isolation test would be blind, and the build would say so.

The same idea runs through the rest of the checks. Every decoder of messages between parts has bounded proofs, from the Kani model checker, that it never panics, overflows or reads out of bounds. Mutation checks then break the decoders deliberately, to show the proofs notice. Every parser of outside input is fuzzed with hostile data.

All of it is part of make ci, the gate every change must pass. The isolation tests run every time; a proof or a fuzz run is repeated whenever the code it covers changes.

Gates out of reach

A gate is only as strong as the hand that can change it. So the checks every contribution to NoWayOS must pass are defined in Defence Agent, a public repository of their own. A pull request that touches a gate is flagged for the maintainer.

Defence Agent tests itself the same way: twenty planted pull requests, each hiding something a reviewer could miss. There's hidden right-to-left text in a comment, a letter swapped for its Cyrillic look-alike, a dependency fetched straight from a git repository, a workflow that would run untrusted code. Each must be caught, while three real past changes must pass.

Proof, not adjectives

None of this makes a device “unhackable”. Nothing does, and we'll never say it. What it gives you is evidence: a record of what was tried, what was stopped, and the command that shows it. Read one real image's evidence, or the gates themselves.