Every program on NØNOS already had to prove it was exactly the approved program before it could run. Today that guarantee reaches the kernel itself, the proof survives a quantum computer, and the code that checks the proof has been machine-checked by four separate tools. One transparent STARK, one shared prover and verifier, verified end to end.
Two layers, one guarantee
Kernel self-attestation
Kernel self-attestation. The bootloader already measures the kernel with BLAKE3. Before it jumps, it now verifies the kernel's STARK trailer, carried in the image footer, against the enrolled kernel root, bound to the measurement and the boot epoch. If the kernel is not exactly what was enrolled, it does not run. The code is in nonos-bootloader/src/kernel_verify/stark_attest.rs.
Capsule attestation. The kernel gates every spawn. It verifies each capsule's STARK trailer against the policy root, bound to the capsule's ELF measurement, its granted capabilities, and the policy epoch. This replaced the old PLONK path, which was forgeable. The code is in src/security/capsule_attest/stark.rs. No unsigned path, no override: no code runs, kernel or application, unless it proves what it is.
One verifier, no drift
A proof only means something if the code that writes it and the code that reads it agree to the bit. We moved the whole STARK implementation, 101 files, into a single shared crate, nonos-stark, linked by both the kernel and the bootloader. It carries its own Keccak and BLAKE3 so prover and verifier digests are byte-identical. There is no second implementation to drift, and only seven external hash call sites had to change to adopt it.
The cryptography
Transparent FRI-STARK: hash-based, post-quantum, and with no trusted setup. It works over the Goldilocks field, p = 2^64 minus 2^32 plus 1, with a quadratic extension for the challenges. The statement is Merkle membership: a measurement, the BLAKE3 of an image, is a leaf of a tree whose root the verifier trusts, bound to a context. Soundness is money-grade, through extension-field challenges near 2^-128, proof-of-work grinding, and a blown-up FRI rate. Keccak drives the Fiat-Shamir transcript and the Merkle trees, BLAKE3 measures the image, and Poseidon is the in-circuit sponge.
Proven, not asserted
The trusted path is checked in continuous integration by four independent tools:
- Lean 4, 203 theorems, covering Merkle soundness, context and capability
binding, the money-grade soundness budget, the wire format, the composed gate, and signing-key lifecycle.
- Verus: the parser never over-reserves, the cursor stays in bounds, and the
gate accepts only when all three checks hold.
- Kani: the untrusted-input parser is total, with no panic or undefined
behavior on any input.
- 165 runnable tests against the real code, including a denial-of-service
proof of concept.
Design, arithmetic, and parser are each checked by a different tool.
A real bug, closed
The proof deserializer read a 32-bit length from an untrusted capsule trailer and handed it to an allocation before any data backed it: a multi-gigabyte allocation that a hostile capsule could trigger at the spawn gate itself. Every length is now capped at the bytes actually remaining. It is proven closed three ways, by Kani totality, a runnable proof of concept, and a Verus invariant. The trusted gate cannot be turned into a denial of service. The fix is in nonos-stark/src/air/deserialize_ext.rs.
Build it yourself
A configurable build system ships with this work. make menuconfig is a dependency-free, step-by-step feature picker that writes a .nonos-config. make from-config builds exactly the profile and options you chose. make nonos-mk-zerostate produces the canonical image with the gate enforced, dual Ed25519 and ML-DSA-65 signatures, an anti-rollback index, and TPM measured boot. Under the hood, 45 profile recipes that repeated the same command now route through one build macro. One interactive command, your own verified kernel.
Honest status
We say precisely where this stands.
- Proven today: the Lean, Verus, Kani, and runnable proofs; kernel and
bootloader compiling with the gate; the enrollment loop; menuconfig; the DoS fix.
- Wired, not yet boot-proven: the capsule pipeline switch, kernel
self-attestation, and the default build flip.
- Pending: landing the build submodule patch, and a full QEMU boot proving
bootloader to kernel self-attestation to desktop, end to end.
The numbers
203 Lean theorems, four proof tools, 165 runnable tests, one shared verifier crate, 101 files extracted, seven coupling points, 45 build recipes folded to one macro, one real denial-of-service bug closed, a depth-8 policy tree, and a dual Ed25519 and ML-DSA-65 signature.
The work landed across four pull requests: #375, #376, #377, and #378.