NØNOS 0.9.1

410 commits since 0.9. This is what changed and, where it matters, what is not finished yet.

The TPM is spoken to directly

The TPM is spoken to directly. The bootloader drives the chip over its command-response buffer interface rather than through firmware helpers. It requests locality the way the specification says to, submits commands over CRB, and reads the endorsement key through the same transport. Buffers are touched with volatile scalar accesses, because a compiler is entitled to coalesce writes to memory it believes nothing else is watching, and a TPM is watching.

Two signatures on everything. Every capsule and the kernel carry an Ed25519 signature and an ML-DSA-65 signature. The second is a post-quantum lattice scheme, so an image signed today stays verifiable by someone who later holds a quantum computer, and an archive of today's releases does not become forgeable.

A transparent STARK attestation per capsule. 81 capsules are enrolled under one policy root. The proof carries no trusted setup and no toxic waste, and verifying one does not require the ability to produce one.

An anti-rollback floor in the TPM. A correctly signed but superseded image is refused before anything unverified runs. This release halts on a machine whose recorded floor is above its index, and says so on screen rather than continuing.

Key rotation no longer changes what gets signed. A rotated signing key used to make the build system rebuild a featureless kernel over the path the full one occupies, and the signer would then sign and attest the wrong image while reporting the right name. That is fixed, and it is worth stating plainly, because it is precisely the failure a signature is supposed to make impossible.

The kernel

Memory is wiped before the machine stops

Memory is wiped before the machine stops. The shutdown path clears the heap, process memory and kernel stacks, and there is a proof that the wipe reaches what it claims to reach. An operating system that keeps nothing on disk still holds everything in RAM while it runs.

Four faults on the trusted path, found and fixed: frame aliasing, a keylogging channel, reply injection, and service squatting. Each is proved fixed in Lean and demonstrated in a runnable proof of concept rather than asserted.

IOMMU. VT-d remapping units are probed at boot and reported. The register decode and table encoding are implemented, and the code refuses to report an isolation that is not actually happening, which is the failure mode that makes an IOMMU worse than not having one.

Paging. Address space identifiers are used properly: invalidation is by ASID and callers are routed through it, so a context switch does not throw away translations belonging to other address spaces. Demand faults the tracking table cannot hold are metered rather than dropped silently.

SMP. The TLB shootdown has its own interrupt vector, the reschedule IPI is delivered, and the per-CPU assembly offsets are derived from the structure definition instead of being written twice and kept in step by hand.

PCI. Configuration space is reached through one accessor on every architecture, choosing ECAM where the platform publishes a window and the port pair otherwise, and reporting failure instead of silently enumerating an empty bus. BARs the firmware left unassigned are now assigned, and the window allocator's alignment and bounds are proved.

Station addresses are drawn, not announced

Station addresses are drawn, not announced. A factory hardware address is burned into one piece of silicon and is the first field every access point records. A system that keeps nothing on disk still arrived everywhere under the same name. Both network drivers now draw a random locally administered address instead. Being amnesic and being unlinkable are not the same thing, and this release closes that gap. The rule is proved in Lean and covered by Kani harnesses over every octet of every input.

Nym mixnet routing. The mixnet client speaks the real protocol: Sphinx packet construction against the published vectors, gateway frames encrypted with connect-time registration, hops addressed by socket address, bandwidth allowance claimed, the directory fetched from the network rather than compiled in, and exits taken from the live topology. A SOCKS5 front end serves clients concurrently and opens tunnels through it, and the browser can send pages that way.

Confirmed working on physical hardware in this release, over Wi-Fi, as well as under emulation. Browsing also works with it switched off.

Wallet

Real transfers of ETH and NOX. Staking with the contract's own lock terms and weights, position unstaking, and the ZeroState Pass count read live. Amounts are held in wei with decimal entry rather than whole tokens. A stake that exceeds the balance is refused before it is signed, rather than paying gas for a transaction that can only revert.

A trading screen shows what a trade will do before it is made, with constant-product quoting and 256-bit arithmetic.

Custody invariants are proved in Lean, including custody of a signing seed at rest.

A transaction signed inside the operating system settled on Ethereum mainnet.

Wi-Fi works on real hardware

Wi-Fi works on real hardware. Two faults, one hiding the other. The station address draw needed a capability neither network driver had been granted, so it failed closed and the radio was never configured, and ethernet was broken the same way. Underneath that, the efuse read could not tell a dead register window from a blank one, and the board description it returned selected a radio front-end the hardware does not have. Both are fixed, and a bring-up that stops now names the step it stopped at instead of blaming the wrong one.

Audio. An Intel HDA driver and an audio service capsule.

Multi-architecture. Substantial aarch64 bring-up: console before anything that can fail, memory mapping with a direct window, the frame allocator kept out of the kernel image, the CPU roster and kernel context wired, SVE where the part has it, ECAM at the high window, and the desktop capsule set cross-built. The shared kernel now reaches the architecture through a boundary rather than calling x86 directly: control registers, the trap layer, the TLB, the interrupt controller, the wall clock and the idle wait all sit behind it.

Applications

Terminal. History search, command completion with the exit status of the last command, syntax colouring as you type, and correct handling of wide characters.

Browser. A real script environment under test, timers run against the clock and not the queue, page navigation, repeat(auto-fill) and auto-fit grid tracks resolved against the container, and fragments that move to a new row taking their clip rectangles with them.

Settings. Every setting the system actually has, clickable switches, complete keyboard navigation, per-panel key hints, and layout that follows the window rather than the size it opened at.

Lean proofs covering the trusted-path fixes, the station address rule, wallet custody invariants, the aarch64 leaf encoder, and the guarantee that nothing powers off unwiped. Kani harnesses over the address rule. Kernel constants are held against the numbers Lean states, so a proof cannot quietly drift from the code it describes. The evidence manifest counts harnesses from source rather than from build output.

Build and reproducibility

Images pin every timestamp that reaches them: the FAT volume serial, file modification times, and the ISO volume descriptor. Two packagings of one build are byte identical.

Two build faults that could publish a wrong artefact silently were found and fixed: the key rotation problem described above, and a clean that left the tree unable to link while reporting success.

On reproducible builds, precisely. Two builds of the same source produce an identical kernel and a different attested image. The difference is the STARK trailer, which is randomised because the proof is zero knowledge, and a proof that came out the same every time would leak what it hides. So the published image hash identifies the file we released, and is not something a reader regenerates. What a reader can do is rebuild the kernel from source, compare it, and verify our signatures and the attestations carried in the image. Checking a proof does not require reproducing it.

Not yet done: capsule level reproducibility is untested, and a rebuild on another machine will not match until dependency paths are remapped out of the binary.

• Networking does not work inside VirtualBox. VirtualBox presents an Intel

PRO/1000, and that driver is not bringing the link up. Everything else runs: the machine boots, attests, and the desktop is fully usable. QEMU presents a virtio adapter and a different driver, which is why this was not caught earlier. A fix is in progress. If you want the network today, use QEMU or real hardware.

• VirtualBox needs EFI enabled, which is not its default, plus 4 GB of memory. See

the VirtualBox guide.

• Capsule level and cross machine reproducibility are untested.

Get it

The download page has the ISO for virtual machines and the USB disk image for real hardware, with SHA-256 and BLAKE3 for both. The ISO carries no partition table of its own, so use the .img for a USB stick.