What a proof can promise

Software is usually trusted because it was tested. Somebody thought of the ways it might go wrong, tried them, and watched it cope. That works well, right up to the case nobody thought of.

A proof starts from the other end. It doesn't try cases. It shows, by mathematics, that a statement holds for all of them.

Every case, not the ones we tried

Take a small promise: this code never reads past the end of its buffer. A test can feed it a thousand inputs, or a billion, and report that none of them broke it. A proof says something of a different kind: there is no input that breaks it. Not one was found, and not one exists.

The price is rigour. A proof needs an exact statement of what the code should do, called its specification, and an argument that connects every line of the code to it. For real software that argument is far too long for a person to check by eye. So a computer checks it.

Checked by machine

That is what “machine-checked” means. The proof is written out in full, in a language a program called a proof assistant can read, and the program checks each step against the rules of logic. It doesn't get tired on page nine hundred, and it doesn't take anyone's word for anything.

seL4's proofs are checked this way, in a proof assistant called Isabelle/HOL. They are public, and anyone can run them again.

What seL4's proofs say

seL4 is the kernel every NoWayOS system runs on: about 10,000 lines of code, and the only code with total control of the device. Its size is the point. An argument about ten thousand lines can be finished. An argument about tens of millions cannot, not yet.

The seL4 Foundation sets the proofs out in layers:

• The code does what the specification says, and nothing more. From that follows a list of things the kernel cannot do: overrun a buffer, follow a null pointer, leak memory, divide by zero.
• The program that runs matches the code that was proved. A compiler sits between the two, so a further proof checks its output.
• The kernel can keep the parts of a system apart. One part cannot change another's data, read it, or take the resources it needs, unless it was granted the right to.
• A system can start in the state it was designed to have, with exactly the grants its description lists.

Not every layer is finished for every processor and every configuration. That matters, and we will come back to it.

What a proof takes for granted

A proof is exactly as wide as its statement, and it stands on its assumptions. seL4 writes its own down: that the hardware behaves as its model says, that a few hundred lines of the lowest-level code are right, that the code which runs before the kernel starts has done its job. The proof of secrecy does not cover timing.

It says nothing about whether the specification asks for the right thing, and nothing about the software above the kernel. A proved kernel will faithfully isolate a program that has a bug in it. The bug is still there. It just can't reach anything else.

That is not a weakness in the proofs. It is what makes them worth having: they say precisely what they cover, so you know precisely what is left.

Where NoWayOS stands

Here is the plain position. NoWayOS runs on seL4, but no NoWayOS image is inside seL4's completed proofs today. NoWayOS uses seL4's mixed-criticality configuration, whose proofs for our processors are in progress. And seL4's proofs never did cover NoWayOS's own code. So we don't call NoWayOS “formally verified”, and we won't.

Every image says where it stands. A file beside it lists its kernel's configuration, option by option, against the one seL4 has proved. Security shows a real one.

Smaller proofs of our own

NoWayOS's code gets its assurance another way: Rust, isolation, review, testing, and proofs of a more modest kind.

Every decoder of the messages that pass between parts of a system has bounded proofs, made with a model checker called Kani. A bounded proof covers every input up to a stated size, here the longest record a decoder accepts. Inside that bound it is a real proof: no input makes the decoder panic, overflow or read out of bounds. Beyond the bound it says nothing, which is why the bound is the longest input there is.

Then we break the decoders on purpose, to make sure the proofs notice. A proof that can't fail is no better than a test that can't.

The honest size of it

A proof doesn't make anything “unhackable”. It makes one statement true, in every case, under assumptions you can read. Know the statement and the assumptions, and you know what you have.

That is why NoWayOS is built on the kernel that has them, and why it tells you, image by image, how far they reach.