x86-64 microkernelC + no_std RustMIT licensedresearch-grade
Horus is an operating-system kernel in which no program has any power by default.
Every privileged action, reading a file, talking to a driver, creating a kernel
object, requires the caller to hold a specific unforgeable token for it. There is
no root flag that opens every door, and no code path that trusts a
caller because of who it claims to be.
It is a real system, not a paper design: it boots on x86-64 hardware and under QEMU, drops to an unprivileged shell, and runs ordinary C programs including GNU coreutils and the Tiny C Compiler, on a kernel whose filesystem and console driver are themselves unprivileged programs. The kernel image is byte-for-byte reproducible, the boot chain is measured into a TPM, and the disk encryption key is sealed against those measurements.
The problem, and the shape of the answer: no operating-systems background assumed.
The kernel is the one program on a computer that hardware trusts completely. Code running there can read any memory, touch any device, and change any protection the machine offers. Everything else on the system runs at the mercy of that trust.
The trouble is what conventional systems put inside that boundary. Linux and Windows place tens of millions of lines in it: every filesystem, the network stack, the graphics driver, the driver for a webcam you plugged in once. A single memory-safety bug anywhere in that mass is not a bug in a driver; it is total control of the machine. The privileged code is enormous, so the thing you must trust is enormous.
A microkernel attacks that directly by making the privileged part
small and moving everything else out. In Horus, the filesystem is a normal program
called fs_server. The console and serial driver is a normal program
called console_server. They have no special powers; they run in the same
unprivileged mode as the shell. A memory-safety bug in the filesystem server
compromises the filesystem server, not the machine.
That leaves a question conventional systems answer badly: if the filesystem is just another program, what stops any program from impersonating it, or from reading its traffic? The answer is the second idea, and the one Horus is built around.
"Is this caller allowed to do this?"
The kernel receives a request, looks up who the caller is, and consults a table of
rules, user IDs, group membership, file modes, whether the caller is
root. Authority is ambient: it comes from your identity, and
it applies to everything you name.
Every privileged operation therefore needs its own correct check, and the checks are scattered across the whole kernel. Forgetting one is a vulnerability, and no one can enumerate what a program is able to do without reading all of them.
"Does this caller hold the token for this?"
A program's power is the list of capabilities it holds, tokens the kernel issued, each naming exactly one object and exactly one set of rights over it. The kernel keeps them; a program refers to one only by its slot number, so it cannot forge, guess, or widen one.
There is no identity to consult and nothing to forget to check: a program either holds the token or it does not. What it can do is a list you can print, and authority spreads only when something deliberately hands a token over.
Horus takes a third position too, on how the kernel is written. The C kernel is about
23,000 lines; the code that parses untrusted bytes or enforces an algebraic security
property is 6,200 lines of memory-safe no_std Rust linked into it; ELF
parsing and relocation, the capability algebra, the cryptographic primitives, the
CSPRNG, the pointer and range validators. That split is argued empirically rather than
aesthetically: moving the ELF loader into Rust uncovered two real
out-of-bounds bugs in the C original.
The central idea, worked through on a real example from the running system.
A capability in Horus is a small record the kernel owns:
{type, rights, object, badge, serial, generation}. It lives in a
per-task capability space of 256 slots, and userspace only ever sees the
slot number. That indirection is the whole reason it cannot be forged; there is no
struct in your address space to modify and no name to guess.
Six fields, and a C assignment writes them one at a time — which is why every write to a slot is made under one lock. Revocation reads every task's capability space and decides from what it finds which capabilities a revoke reaches and which kernel objects nothing names any more; an unlocked writer can show that sweep a slot whose type is already set while its object still describes the slot's previous occupant. On 2026-09-12 five writes were found that did not take the lock, thirteen days after the same defect had been diagnosed and fixed at a sixth site. Which functions write a capability slot, and what makes each write safe, is now declared in a manifest a CI job checks. One site does not take the lock and is exempt by a written argument instead — and the guards that argument leans on, which live in other files, are pinned in the manifest so the exemption cannot quietly expire when one of them is edited.
A capability naming the right object is only half of it — the object has to be the one the design says it is. Every task here is born holding exactly one endpoint capability, to a reply endpoint that is supposed to be private to it. On 2026-09-12 that turned out to hold for task ids below 64 and not above them: the table was sized 128 while the region it was meant to contain ran to 320, and the index space's own dividing line sat at the table's end — so a high-numbered task's “private” endpoint resolved to one carved out of another task's memory. The table's size is now derived from the task ceiling rather than written next to it, and three separate guards fail the build, refuse the index, or reduce the task count if that ever stops being true.
The example below is not an illustration; it is how the shell actually reaches the filesystem. Step through it.
When init starts the filesystem server, the kernel gives it a
capability naming that server's endpoint, carrying READ and
WRITE. Here READ is the right to
receive, the right that makes you the server rather than one
of its clients.
Nothing else in the system holds this. A program with no capability to the endpoint cannot name it at all, which is a stronger statement than being denied access to it.
init mints a child capability into the shell's capability space with
rights & WRITE. The masking is the point: minting computes an
intersection, so a derived capability can only ever carry a subset of
the parent's rights.
Widening is not a policy the kernel declines to allow. It is an operation that does not exist. There is no syscall that adds a right to a capability.
Suppose the shell tries to receive on its capability, an attempt to
read other clients' filesystem traffic, or to answer requests as though it were
the server. It calls sys_ipc_recv(9).
The kernel looks up slot 9, finds a real capability of the right type, and checks
for the READ right. It is absent, so the call returns
SYS_ERR_PERM and the receive handler is never entered. Impersonating
the filesystem server is not blocked by a check somewhere; it is
unrepresentable with the token the shell holds.
When init revokes its capability, the kernel nulls it and
everything transitively minted from it, sweeping every task's capability
space. The shell's slot 9 becomes CAP_NULL; it was not asked, and
it cannot decline.
Scope is exact: ancestors, siblings, and independent capabilities to the same endpoint survive. Two mechanisms enforce it. The structural sweep walks the derivation tree, and each capability's serial keys a generation counter bumped on revoke, so even a stale copy that somehow escaped the sweep fails validation. Both must hold; revocation carries Kani proofs that the subtree hit is exactly right.
This part of the system changed because an audit found it wanting. Until 2026-07-27, IPC endpoints were addressed by a raw integer, so any program could intercept or forge messages to any server; the diagram above described the design, not the code. That finding (C-1) is fixed, and the conformance suite that missed it was rebuilt and then run against the vulnerable kernel to prove it now detects the bug.
Where the rule is enforced; the whole of it, in about twenty lines.
A security model is only worth as much as the code that enforces it. In Horus the enforcement is not spread across handlers; each syscall declares the capability it needs in a dispatch table, and one gate checks it before the handler exists as far as the caller is concerned.
The ABI defines 117 syscall numbers. The dispatch table is sized to
the highest of them plus one, and a default build installs 97
handlers, the remainder are reserved, or are test-only calls compiled out
entirely. Every one of those gaps answers SYS_ERR_NOSYS. That difference
is the fail-closed property, not an oversight: a shipping kernel denies the debug
surface exists rather than merely declining to document it.
This is what a call actually passes through. Both exits on the left are refusals; a handler runs only if nothing on the way out fired.
syscall_handler(). A compile-time assertion
ties the table's size to the highest syscall number plus one, so a new syscall number
cannot be added without a table entry; the build fails instead of the kernel
silently accepting an unauthorised call.
The gate settles what a caller is allowed to do. It says nothing about who the caller is, and a filesystem needs to know that, because POSIX permissions are defined in terms of a user. Letting the client supply its own user ID would hand every program the authority the permissions exist to withhold.
So a server never trusts what a client says about itself.
SYS_IPC_SENDER returns the user ID the kernel recorded for the
sender of a message, established only by a successful login and unforgeable by the
sender. fs_server authorises every file operation against that value
rather than against anything in the request, which is why the filesystem can enforce
rwx correctly while being an ordinary unprivileged program with no way to check
identity itself.
What is inside the trusted boundary, and what deliberately is not.
The kernel supplies address spaces, threads, capabilities, message passing, and an encrypted block store whose keys it never releases. Everything a user would recognise as "the operating system", file names, directories, permissions, terminal behaviour, which program to load and how, lives outside it, in ordinary programs reached over message passing.
init, which
is the source of all delegated authority; fs_server, which decides who
may read a file; and console_server, which sees all terminal traffic.
The shell, coreutils, TCC and every program you write are outside it.
Per-task four-level page tables, demand paging, copy-on-write, non-executable
stacks, kernel W^X swept for violations at boot, unmapped stack guard pages, and
30-bit address-space randomisation for user programs. fork clones an
address space by marking it copy-on-write on both sides, mark only the
child's and the two tasks are one process sharing one stack.
Synchronous send, receive, call and reply over bounded FIFO endpoints, plus asynchronous notifications and byte-stream pipes. Replies use one-shot capabilities naming the sender, so answering a client you never heard from is impossible rather than merely refused.
smoke-captest
Kernel objects are carved out of CAP_UNTYPED regions with
SYS_RETYPE, following seL4. A task holding no untyped capability
cannot create a kernel object at all, and the region it holds bounds the kernel
memory it can consume.
SMP is on by default: ACPI enumeration, AP bringup, a shared runnable pool, acknowledged TLB-shootdown IPIs, and a microarchitectural flush when switching between tasks that do not trust each other. SMT siblings are parked in software.
smoke-smp · smoke-flush
Each (inode, block) gets its own AEAD subkey with a fresh nonce per
write, under a Merkle rollback tree. The encryption happens entirely inside
the kernel; the ring-3 filesystem server never holds a key.
Those nonces used to live in a complete in-RAM mirror of the volume, under a flat MAC recomputed over every one of them on each write — which is also why the volume could not grow, since both scale with the disk. They live in a bounded cache now, under a Merkle tree: a write touches four hashes instead of a megabyte, and mounting checks one node instead of reading the whole region.
Two things are worth naming about that. A full mirror is self-healing against a lost metadata write, because it holds every entry and can regenerate the one that was lost; a bounded cache cannot, so the write-ahead log is now the only thing keeping a block's nonce and its ciphertext in the same atomic unit. And the tree catches partial rollback — a subtree rewound while the rest of the volume moves on. On its own it could not catch the whole volume being replaced with a consistent earlier snapshot, because its root lives in the superblock it protects: rewind both together and every check inside the disk still passes. Nothing on the disk can tell “this volume” from “this volume, last week”.
So the anchor is somewhere the attacker holding the disk isn't: a TPM counter that only goes up. The volume records the value it was last written at, bound into the tree's root so it can't be edited, and a volume behind the counter is refused. The test restores an entire earlier disk image between boots — the actual attack, not a model of it — and requires the refusal. It applies to volumes formatted on a machine that has a TPM, at a granularity of one boot; the volume records which kind it is rather than leaving you to guess.
Both of those are what a 16 GiB volume needed: the mirror would have been 128 MiB of static kernel memory against a 16 MiB budget, and the flat MAC would have hashed a megabyte on every metadata write and read the whole region at every mount. A file reaches 512 GiB now, so the disk is what you run into rather than the layout.
smoke-fs · smoke-meta-crash · smoke-merkle-replayThe kernel refuses to format a volume it does not recognise just because someone typed a password at the login prompt — a mistyped password on a machine whose disk it did not know used to destroy that disk, silently. Formatting became a deliberate act instead, and for a while that act had no caller at all: a refusal that is absolute because nothing can reach it is a weaker claim than one that is deliberate.
It has a caller now, and the caller answers to a capability of its own.
CAP_STORAGE_FORMAT is held by init and passed to the
installer alone. It is deliberately not a permission bit on the storage
capability the filesystem server and the shell already hold: those are handed out
with every right there is, so defining the bit would have granted it to both, with
nothing in the diff to show for it. A separate capability fails closed where a new
bit inside “all rights” fails open.
The same capability answers the survey — what disk is here, how big, does it already carry a volume — because that readout is the first screen of the same act. A task that cannot destroy the volume is not told what is on it.
Since September 2026 that survey can count past one. The driver probes both devices on the bus, each is a block device carrying its own identity rather than writing through a global “current disk”, and the kernel mounts the first device that actually carries a volume rather than simply the first device — with one disk those are the same sentence, and with two they are not. Asking about a device that is not there is refused rather than answered about a different one. That last part is not politeness: a clamped index faults nothing and overruns nothing, it hands back a complete and well-formed description of the wrong disk, to the one program whose next act is erasing the disk it was just told about.
And the call that erases a disk now names the disk it erases. Not “choose the device” followed by “format it”: that is a confused deputy by construction, because the act that destroys would depend on a global somebody else set, with any amount of anything in between. The target is an argument, refused if it names no such device or one already carrying a mounted volume.
Making that work meant finding two variables that had been standing in for the target all along and were never noticed, because with one disk they were always equal to it. The driver selected a drive and then waited for whichever drive was selected before. Thirty-one places reached the disk through a global “current” pointer while the format wrote through the device it had been handed. Neither produced an error — the first simply stopped the machine doing disk I/O at all. Both were found by the first test that ever wrote to the second disk, which is the argument for having the test.
The caller is an installer, and it is the only task that gets a copy. It cannot read
the volume it replaces, and it cannot create a task, so nothing it does outlives it.
Before it erases anything you type the word FORMAT — not a
menu choice, because a menu whose default is Cancel still becomes a format with two
keystrokes, and somebody holding return through a wizard has not decided anything.
Install media may replace a volume that is already there, and what
makes that safe is a distinction rather than a relaxed gate. A volume the machine
merely recognises is mounted but locked — which is the state install
media is always in, because it never logs in. A volume that has been
unlocked means somebody proved they own the machine and is using it, and
the kernel refuses to reformat that one whatever the installer asks. Replacing is
also a different question to answer: the disk menu marks a disk that holds a volume,
and the last screen asks you to type REPLACE rather than
FORMAT, so consent to one is never consent to the other.
That word is the last thing it asks. It used to be the second: you consented, then answered five more screens about passwords and account names, and by the time the disk was erased the consent was about a machine state you could no longer see. Now the installer shows what is at stake, collects every answer, shows them back on a review screen you can correct any of, and only then asks for the word — with nothing between it and the format.
The test installs onto a blank disk, powers the machine off, boots it again and logs in with the password that was typed. That last step is the whole claim: a format that returns success is not an install, and an installer that sealed the volume but left the root account on its built-in password would produce a perfectly installed disk nobody can log into — which the first boot cannot detect, because everything it can see succeeded.
A second test powers the machine off at the login prompt, before anyone
types anything, and requires the boot after that to finish the install. That gap is
where an installed machine actually lives: the base system is copied into the store
when the volume unlocks, so an install nobody logs into leaves the copy unfinished,
and finishing it is the next boot's job. It was not being done. A sealed volume is
mounted and locked, and the object store answered anyway — the encryption
layer refused, because it needs the key, but the inode table is plaintext on disk
and nothing there refused at all. The filesystem server asks the store whether it
is usable, was told yes by a volume nobody had opened, copied into a locked disk
where every write failed, and recorded the job done. /bin was then
empty on that machine for good. The store now answers only an unlocked volume, in
one place rather than in eight handlers.
It asks for two passwords, not one. A machine whose only login is root is a machine every session is administered from, so the install creates an everyday account alongside it — and either password opens the disk at boot. That last part was the missing piece rather than a convenience: the volume is sealed to key slots, and the kernel unlocks it with the typed password before it can read the account table, so an account without a slot of its own opens nothing and is not found. It worked perfectly on a machine somebody else had already unlocked, which is why nobody noticed — every test and every operator logs in as root first. The test now logs in as the unprivileged account, on a machine nobody has opened.
The install also deletes the account the kernel compiles in. A fresh volume's account table is seeded from that built-in image, so until this landed every installed machine shipped a working login whose password is printed in the source. It is replaced by the one you named.
A third checks who a password command actually writes. Creating an account and
giving it a password is the ordinary next thing an operator does, and the shell was
matching the account argument and then discarding it — so
passwd 1001 reported success and changed the administrator's own
password instead. Not a cosmetic mis-print: changing your own password re-seals the
volume to it, so the string typed for somebody else became the disk's, and the only
place that showed was the next power-on, where the password chosen at install no
longer opened the machine. A malformed argument is now refused rather than quietly
treated as a request to change your own, and the reply names the account it wrote.
It installs onto a laptop's soldered eMMC, which is not the same disk as the one every earlier test used. A budget machine's internal storage sits behind an SD host controller that neither the IDE driver nor the SATA driver can reach, so an install scenario that only ever attached IDE said nothing about the hardware the driver exists for. Driving the whole install onto a card found two defects the driver's own tests could not. The register file is memory-mapped, and the probe maps it into the kernel's address space — but a syscall reaches the driver on the calling program's, where it was not mapped at all, so the format wrote to a page that was not there and the installer was killed. The second is quieter: the card addresses 512-byte sectors and the filesystem addresses 4096-byte blocks, and the first version handed one to the other unconverted. Block zero is sector zero either way, so the volume header read back, the install reported success and the next boot recognised the disk — and every other block came from an eighth of the right place. What failed was the login, seconds later and a layer above the mistake. A test that stopped at “the volume is there” would have passed on it.
smoke-installer · smoke-installer-replace · smoke-replace-live · smoke-installer-refuse · smoke-installer-provision · smoke-installer-accounts · smoke-passwd-target · smoke-captest · smoke-storage-survey · smoke-installer-sdnewlib as the C library, a shell with pipelines over bounded in-kernel pipes, eleven ported GNU coreutils, man pages, and the Tiny C Compiler, so you can compile a program on the machine it runs on.
smoke-coreutils-shell · smoke-tccFive steps between firmware and a mounted volume. Order matters here, so it is numbered.
The capability model governs a running system. It says nothing about how that system got there, which is a separate problem with a separate answer. Each step below is tested by breaking it deliberately and asserting that the next step refuses.
A Multiboot2 handoff brings up a higher-half 64-bit kernel. The modules are the
userland: init, the two servers, the shell, coreutils, man pages.
A SHA-256 manifest of every module is generated at build time and compiled
into the kernel image, so it cannot be swapped alongside the payload it
describes. A module that fails its hash becomes unreadable, and because
installing a program into /bin goes through that same read path, an
unverified module can never become a root-owned executable.
Falsified by smoke-modules-tamper, which corrupts a payload
inside the ISO and asserts the refusal.
The kernel's SHA-256 is packed inside the boot image the firmware measures into PCR 4, and GRUB refuses a kernel that does not match. A kernel-identity token goes into PCR 8 and each module's digest into PCR 9, over the TIS interface; a host-side script recomputes those independently and CI asserts they match. The volume key is sealed to all three — PCR 4 being the one the kernel does not extend itself, so the seal is not bound to the kernel's own word about itself.
The volume's key-encryption key is sealed to those PCRs under a
PolicyPCR session. A measured-good boot unseals it. Change the
kernel or any module and the PCRs change, so the TPM will not release the key and
the volume stays locked; the tamper is not detected after the fact, it is
prevented from mattering.
Falsified by smoke-tpm-tamper, which asserts the PCRs
diverge, and smoke-tpm-seal, which asserts the volume stays locked.
The reverse of the property above, and the one with the downgrade in it. A
volume formatted on a machine with no TPM opens on its password alone, forever
— so presenting a re-formatted drive to a machine that requires measured
boot would make the requirement evaporate, with the TPM present, the PCRs
extended and nothing else out of place. A kernel built with
MEASURED_BOOT_REQUIRED=1 refuses to unlock it. The ephemeral RAM
volume is exempt, because its key is generated each boot and discarded at
power-off: there is nothing there for a measurement to protect.
Falsified by smoke-measured-persist-control, which deletes
the refusal and requires the unsealed disk to unlock; the gate it extends,
smoke-measured-persist, formats a real disk on a machine with no TPM
and presents it to one that has. The opposite direction is
smoke-measured-persist-sealed, which requires a volume sealed under
the policy to open again on the next boot — without it, a check that
rejected every disk would pass.
init launches fs_server, endows it, resumes it, then
does the same for console_server and the shell. From this point the
capability graph is a complete description of who can do what, and it only ever
narrows.
One more link in the chain is worth naming because it is where most projects are
weakest. The single network dependency in the build (the newlib tarball) is pinned by
SHA-256, verified on every invocation rather than only after a fetch, refused
before unpacking, and quarantined rather than left in place when it fails.
smoke-newlib-tamper checks both directions, because a gate that refused
everything would pass the negative test alone.
Two commands from a clean checkout to a login prompt.
An x86-64 Linux host, Debian or Ubuntu; no cross-compiler needed. This is what the
boot looks like, abridged for width, and with the microsecond timestamps stripped.
On a real boot every line above the banner carries one — including the
lines ring 3 printed, which is the half that used to go unstamped. The console changes
hands part way down that list, so both writers stamp, in one format, from one epoch.
The real log is readable afterwards with dmesg.
The banner is not a constant. Everything to the right of the eye is asked of the
running kernel when it prints — uptime, the tasks this caller may observe, the
shell’s own pid and how many capabilities init chose to delegate to
it, and the watermark of the untyped region every spawn is carved out of.
Facts the shell holds no capability to ask for are left out rather than guessed at,
which is why there is no line here for RAM, CPUs or the disk.
Booting `Horus 64-bit Secure Microkernel' [ OK ] boot modules verified against the embedded manifest smp: 4 cores online kernel ready, starting init (PID 1) [fs_server] userspace FS server starting (encrypted object store). [fs_server] registered; serving. init: fs_server ready init: console_server launched [console_server] ready (ring-3; owns serial + VGA framebuffer) init: starting, launching shell _.-------------._ Horus Secure Microkernel .-' `-. capability-based - privilege-separated .' _.-------._ `. -------------------------------------- / .' `. \ Arch x86_64 | | ( o ) | |___ Uptime 1.57s \ `. .' / Tasks 5 visible `. `-._____.-' .' Shell pid 4, 7 capabilities `-._ _.-' Untyped 24K of 3.5M used, 3 objects `-.._______..-' Console ring-3 server | \ | `--.__ |__ _) horus login:
Log in as root / rootpass. Then try ls /bin,
ps, dmesg, man hier, tcc -v, or
cat /etc/motd | wc -l; the pipeline runs over a real bounded in-kernel
pipe.
# build and boot $ rustup target add x86_64-unknown-none $ make # kernel.elf $ make run # horus.iso + QEMU # Ctrl-A X quits $ make run-tpm # with an emulated TPM
# check the claims on this page $ make smoke # boot to ring-3 login $ make smoke-captest # 195 capability checks $ make smoke-modules-tamper # expect a refusal $ make smoke-tpm-seal # expect a locked volume $ make reproducible-build # run twice, diff the record
Every configuration flag, every one of the 355 test targets, and the troubleshooting notes are in BUILDING.md and TESTS.md.
Working means implemented and gated by a named test. Nothing is listed on the strength of having been written.
| State | Subsystem | Witness |
|---|---|---|
| Working | Capability engine, mint, grant, transitive revoke, lineage generations | safe Rust · Kani |
| Working | Capability-addressed IPC, every syscall names a capability slot | smoke-captest |
| Working | One-shot reply capabilities (CAP_REPLY) | smoke-captest |
| Working | Endpoints as bounded FIFO queues (4 slots, fixed at compile time) | smoke-fs-conc |
| Working | Untyped memory and retyping, cspaces, endpoints, notifications, memory frames | smoke-captest · smoke-frame |
| Working | Preemptive scheduling, timer-driven, in ring 3 | smoke-preempt |
| Working | SMP on by default. MADT enumeration, AP bringup, TLB-shootdown IPIs | smoke-smp |
| Working | SMT siblings parked; microarchitectural flush between distrusting tasks | smoke-smt · smoke-flush |
| Working | Ring-3 init (PID 1) supervising the shell | smoke-session |
| Working | Ring-3 console_server, single writer, owns UART and framebuffer | smoke-console-smp |
| Working | The machine's own PS/2 keyboard, read in ring 3 under the port grant console_server already held — including on a machine with no serial port, where the console once believed a floating bus and never polled the keyboard at all | smoke-keyboard, smoke-keyboard-noserial |
| Working | Every boot-console line timestamped, by the writer, across the console handover | smoke-console-timestamps |
| Working | Raw terminal mode, termios and winsize | smoke-term |
| Partial | Shared library text, private library data, a shared object is loaded once into frames and mapped read+exec by many tasks through capabilities that never carry write, so no task can modify code another executes. Its writable segment is not shared at all: each task gets a private copy, carved from the library’s initial image and endowed read+write and never exec. The library’s load address is drawn afresh on every boot rather than compiled in, and a task learns it only by presenting a capability over the library’s own text, so the address of shared code is not something an attacker reads off the binary, nor something any task can simply ask for. The security argument matters more than the size one, sharing a libc’s text is an optimisation, but sharing its data means one task reading and writing another’s errno, stdio buffers and malloc arena, which is worse than the per-program static copies it replaces. The shared libc now builds, is gated, and a ring-3 task calls newlib out of it, 36 pages, 34 of shared text and 2 of per-task data, with the library’s own reentrancy state resolving inside each task’s private copy, and a program now links against it, ordinary C calling printf by name, carrying no libc of its own, 106,392 bytes static against 13,088 shared, and it is not a dynamic linker: there is no symbol resolution, and a program’s direct reference to a libc data symbol cannot be redirected without a GOT | smoke-shlib |
| Partial | Device capabilities, a CAP_IO_DEVICE names one device in a boot-time table (a PCI bus-0 scan plus the non-enumerable legacy platform hardware) and confers only that device’s frames, port ranges and interrupt lines; until 2026-08-28 the capability’s object was never read, so holding the type was holding the console. DMA is confined by VT-d since 2026-08-28; each device gets an address space that starts empty. An interrupt reaches its ring-3 driver either as an MSI on a vector the kernel chose, an MSI’s data word is the vector, so the driver is given nowhere to name one, or through the I/O APIC, masked until acknowledged so an unserviced device cannot livelock the machine. A device’s MSI-X vector table is unmappable by its driver, it lives in a BAR rather than in configuration space, so the vector-choice question had to be answered a second time and in a different way. MSI-X is protected but not yet enabled; no interrupt remapping, no bridge walk | smoke-devcap |
| Working | DMA confinement (VT-d), every device has an address space of its own and every one starts empty, so a device reaches exactly the frames its driver mapped and faults on everything else. Not an identity map: that would have been easier and would have made the mechanism decorative. Each device gets its own domain, so a mapping made for one is unreachable by another | smoke-net |
| Partial | A network driver in ring 3, netd brings up an Intel e1000 holding one device capability and one untyped region, and completes a full DMA round trip: the device reads its descriptor ring, reads the packet buffer, and writes completion status back, every address of which its driver had to map. It drives e1000 rather than virtio deliberately, because a paravirtual device accesses guest memory directly and is not on the far side of the IOMMU at all. It receives on the 82574L (5 boots in 5, which is what smoke-net gates on) and has been seen to receive exactly once on the 82540EM, so reception is a property of the device model here rather than of the driver. Nothing above Ethernet exists: no ARP table, no IP, no TCP, no socket capabilities | smoke-net |
| Working | Ring-3 fs_server over an AEAD-encrypted object store | smoke-fs |
| Working | POSIX rwx against a kernel-attested uid, never a client-supplied one | smoke-fs-perms |
| Working | Measured boot. Kernel pinned in the firmware-measured boot image; TPM 2.0 PCR 4/8/9, disk KEK sealed under PolicyPCR | smoke-boot-pin · smoke-tpm-bootimg · smoke-tpm-seal |
| Working | Boot-module SHA-256 manifest embedded in the kernel image | smoke-modules-tamper |
| Working | ELF parsing and relocation in memory-safe Rust, under W^X, randomised base | smoke-elf · smoke-elf64 |
| Working | SMEP/SMAP in CR4, kernel W^X swept, CSPRNG-reseeded stack canary, CR4.TSD | smoke-cpu · smoke-wx · smoke-stackguard |
| Working | The CSPRNG refuses to emit keystream before it is seeded, a draw from an unseeded pool halts the kernel rather than returning a stream derived from a published constant | smoke-rng-seed |
| Working | Per-task VFS namespace; the shell and the libc resolve every path through one walker, over the capabilities each task already holds | smoke-vfs · smoke-newlib |
| Working | Six syscalls with no caller anywhere in the tree retired, including one that created a task on the capability every task already holds | smoke-passwd-probe |
| Working | Kani proofs of the capability algebra that gate, mint, grant, lookup and revocation, over the whole input space, on every pull request | kani-bounded |
| Working | The capability graph is observable; capview prints every task's slots, under a capability that observes and cannot be widened to write | smoke-session · smoke-captest |
| Working | The security core is interpreted for undefined behaviour on every pull request, aliasing and pointer provenance across the whole C FFI boundary | miri |
| Partial | Monotonic clock, deliberately coarse (one timer tick), so a syscall does not hand back the cycle-accurate timer CR4.TSD denies; no per-task timers yet | smoke-captest |
| Working | newlib libc, shell pipelines over in-kernel pipes, eleven coreutils, TCC | smoke-pipe · smoke-tcc |
| Working | Programs and man pages loaded from the filesystem as boot modules | smoke-modules |
| Working | Forward-secure audit log, history before a compromise cannot be rewritten | cargo test |
| Working | Reproducible builds, kernel.elf byte-for-byte deterministic; the ISO is not, and the reason is grub's, not ours | required CI check |
| Working | Boot interrupt policy recorded and gated at five named milestones | smoke-irq-policy |
| Working | IPC receive, bounded queues, one-shot reply capabilities, and a receive that sleeps on an empty queue rather than polling it | smoke-recvblock |
| Partial | Kernel object lifecycle, retyped objects are destroyed; well-known service objects and tasks[] are still static | roadmap 0.3 |
| Working | Crash-atomic filesystem, write-ahead journal, mount-time fsck, and ATA FLUSH CACHE barriers bracketing the commit record | smoke-fs-wal-flush · smoke-fs-wal-order |
| Partial | Copy-on-write, zero-page and generic breaks both tested; the only producer is the demand pager, and nothing breaks COW over a shared frame yet | smoke-cow · smoke-nzcow |
| Partial | SMP scheduling, a shared runnable pool with a linear scan; no affinity, no priorities | roadmap |
| Partial | Virtual-memory objects, frame capabilities, capability-mediated shared memory, multi-page mapping and sized frames landed; copy-on-write over a kernel object is refused by design | smoke-frame |
| Partial | Process model, fork gives a child a copy-on-write clone of its parent's address space, and refuses outright while a frame capability is mapped; the child inherits its parent's capabilities as derived copies, so revoking one still sweeps the child's; exec then replaces the image and touches no capability, so fork(); exec(); cannot turn delegated authority into a root of its own; there are no process groups, job control or /proc | smoke-fork · smoke-forkexec |
| Partial | A VFS and mount points, a per-task mount table routes each path to the capability for that mount, and a second filesystem server proves it; the existing clients still carry their own path walkers | smoke-vfs |
| Not yet | KASLR, USB, sound, windowing or graphics beyond a text grid, interrupt remapping | roadmap 3.8 (KASLR); the rest are out of scope for now |
Compile-time ceilings still apply to most of the system: 256 capability slots per
task, a 256-byte message, a 16 GiB volume. The volume is no longer among them
either — that number is a ceiling, and the actual size is read from the disk at
boot. The number of tasks is no longer
among them — it is worked out at boot from the memory the machine actually has.
Getting there is a small lesson in taking a codebase's own account of itself on trust.
The ceiling was 64, and every document here blamed the table of task records: 72 KiB.
Beside it sat the per-task kernel stacks, a 4 MiB static array — fifty-six times
larger, and the actual constraint. Moving those lifted the ceiling fourfold and made the
image smaller. Then the table itself moved, into the same memory every other
kernel object is allocated from, so creating a task costs something a program has to
hold permission for. And the thing that would genuinely have capped the count next was
neither: a scratch buffer in the revocation code, sized by the task count and placed on
a 32 KiB kernel stack — a fifth of it at 256 tasks, and past the end of it at 2048.
Nobody had measured it. Three obstacles, and the first two guesses were both wrong.
How the claims above are established, and the several times this project got it wrong.
The security argument rests entirely on the tests, so they are treated as engineering artifacts rather than an afterthought. There are three layers: Rust unit tests and Kani proofs on the host; 172 QEMU integration targets that boot a purpose-built kernel and assert a marker on the serial console; and scripted sessions that type into the real ring-3 shell over serial and read what comes back.
The defect is deliberately reintroduced and the suite must go red. This is not
ceremony. The first draft of the capability conformance suite asserted
< 0 rather than an exact error code, and passed with the
vulnerable IPC handler restored, because sys_ipc_recv returns
-2 for an empty mailbox, so a negative return could not distinguish "the
kernel refused me" from "I was allowed to read and there was nothing there". The
suite now asserts exact codes, and every new syscall ships with a negative test.
Falsification runs in both directions where it can. A refusal-only suite would be
passed by a kernel whose SYS_RETYPE denied everything unconditionally,
so the untyped-memory checks also assert that a held capability really does produce
usable, mutually distinct objects. One check was renamed after
falsification showed it did not test what its name claimed, a green check whose name
overstates it is worse than no check, because it is a claim nobody will re-derive.
Falsifying a gate says nothing about the claims that have no gate. Every
security property in SECURITY.md is now checked by CI against the tree:
a property whose witness names nothing runnable fails the build, and so does a
witness naming a target that does not exist, a target no workflow runs, or a
defect-reproducing flag that would go unstamped at boot. The table is the registry;
there is deliberately no second copy of these claims to drift from the first.
It was written because of what it found. One property; a task cannot read another's XMM register file, had carried an em-dash where its witness should be, against code that was real and ran on every ring transition. No earlier sweep caught it: they looked for gates that were missing or vacuous, and this one was neither. It was present, correct, and attached to nothing.
Intermittent failures are quoted as rates over pinned boots, never as one passing run. The reason is specific: under QEMU's TCG each guest CPU is a host thread, so on an idle many-core workstation the scheduling windows never open and a failing kernel scored 10 out of 10 green. The bug only appears where guest CPUs outnumber host cores, which is exactly what a CI runner is. The stress harnesses build once and boot the same ISO many times with QEMU pinned to a small set of host CPUs.
Sample size is part of the argument, not a detail. A 30-boot run witnesses a 2% event less than half the time; when the scheduler's claim invariant had to be excluded as a cause, the run was 150 pinned boots, all passing, and that is what made the exclusion sound.
This project has been wrong in both directions and publishes both.
smoke-console-smp failed about a third of the time for months and was
treated as noise; it was correctly reporting an intermittent kernel
deadlock. Later, a scheduler invariant checker accused a correct kernel of a
capability leak and blocked a roadmap item for a fortnight; the checker's model of
"what this CPU is running" was the thing that was wrong. A checker reporting
a violation is making a claim about the code, and it can be the one at
fault.
| Change | Before | After | How it was measured |
|---|---|---|---|
Ring-0 preemption deadlock (smoke-console-smp) | 6 failures / 12 | 0/24, 0/24, 0/30 | pinned boots |
| IPC lost-reply race under SMP | 9 hangs / 45 (20%) | 0 / 25 | interleaved ISOs · Fisher p ≈ 0.014 |
| Scheduler claim auditor (impersonation declared) | 10 failures / 20 | 0 / 30 | pinned to two host cores |
| Permanent IPC refusal retried forever | 3 and 5 hangs / 30 | 0 / 40 | starved single-core boots |
| Two CPUs on one kernel stack (G-8) | 31 failures / 800 | 0 / 800 | adjacent-boot alternating, -smp 4 · Fisher p = 6.9 × 10⁻¹⁰ |
| Exec re-entry taken by the wrong CPU (G-9, exec component) | 5 thefts / 20 | 0 / 30 | pinned, -smp 4 · Fisher p ≈ 0.008 · one of three components |
| Page tables recycled under a live CPU (G-10) | 6 faults / 30 | 0 / 30 | pinned, -smp 4 · unguarded arm frees in use on 20 / 20 |
A foreign staged image spawned by sudo (G-11) | 3 spawns / 3 | 0 / 3 | deterministic single boot · the control arm removes the owner check |
| Endpoint queue depth 1 → 4, four concurrent clients | 7042 ms mean | 5162 ms mean | 12 boots each · EP_QUEUE_SLOTS=1 rebuilds the old design |
The endpoint-queue result is quoted for its shape rather than its 27%. The single-slot build's completion times arrived in three discrete clusters about 520 ms apart, each step one more collision-and-retry round. The queue removes the quantisation, which is contention disappearing rather than the same work merely going faster.
Published because a security project that hides its weaknesses is not making a security claim.
Horus is research-grade, has not been independently audited, and should not be trusted with anything real. These are the findings worth knowing before you draw a conclusion about it. The full and deliberately unflattering account is in LIMITATIONS.md.
Fixed 2026-08-22, and worth reading as a pattern rather than a bug. Every task in Horus is born holding a capability in slot 3 that names a fixed memory window and authorises nothing. Four ways into the kernel's internal filesystem; including the file the user database is written to, checked for a capability in slot 3, of any type. Every task passed. A gate everyone passes is not a gate.
It survived two previous sweeps for ambient authority, and the reason is the interesting part: both looked for gates that were missing. These were present and vacuous, which is a different shape and matches neither search. The project's own limitations page carried a table calling itself the complete list of ungated paths; it listed the four gated on nothing and missed the four gated on something equivalent to nothing.
What it exposed was less than it looks: the 32 bytes recoverable from the user database file are an integrity tag, not the password hashes, because a second bug means only the last of four writes to that file survives. The hashes were one bug-fix away from being world-readable. The four doors are now removed outright rather than re-gated.
The same shape had a second home, and it took until 2026-08-30 to find and close. The five calls that create a task — spawn, fork, and their variants — checked the same slot 3, so every task in the system could create tasks and the check could not fail. It gave away nothing, because a spawned child is only ever endowed from what its parent holds; what it gave away was the description, and two comments in the source disagreed with each other about a restriction neither of them enforced. The fix was not a better check but a real cost: a task's capability table is kernel memory, and creating one is now paid for out of the memory budget the parent holds a capability to. A task given no such budget cannot create tasks — which is what that check had always claimed to mean.
And a third home, closed 2026-09-03 — the part that changed how this is checked. Two more calls still carried the identical row in the shipping kernel: one dropped the caller into user mode at an address it chose, the other armed a program image for execution. Neither had a caller anywhere in the tree, and the second read its image from a serial port nothing in the project connects. What makes this worth publishing is not the two calls but how they survived: the project had already written the fact down. A machine-readable manifest of syscall test coverage had said of one of them, for two weeks, that “the slot-3 check does not stop a caller, and a successful call arms an image” — sitting under a heading that made the same claim about three calls which had since been fixed. One true sentence beside three stale ones, in a field nothing asserts.
A fact in a comment is not a gate, and three sweeps in a row certified themselves complete. So the fix is not a fourth sweep: a required check now parses the kernel's dispatch table the way the compiler does and fails the build on any shipping entry gated on that slot. It is falsified four ways, including against a renamed table — because every other rule in it is vacuous if the parser has quietly stopped matching, and a check that cannot fail is the thing this whole finding is about.
The same week, the same mistake, in a different file — and this time the checker found it. The container format the build writes and the kernel reads was recorded as being written down four times. A checker added to refuse a second copy of it reported eleven on its first run, including two on the boot path that starts the first userspace process. The recorded number had been produced by a person reading the code, and it was short, exactly as the count of ungated syscalls above had been short four days earlier.
Both were closed the same way, and it is the transferable part of all of this: stop counting, and let something enumerate. A number in a document is a claim about the code that nothing re-checks; every time this project has written one down by hand, it has drifted. The format now has a single declaration that the kernel, the userspace side and the host build tool all compile, and a test that boots the system and confirms the bytes on disk really came from it — because the build tool is a separate program built by a separate compiler, and no amount of static checking can bridge that gap.
When the kernel traps in its own code it writes the serial line directly, one byte at a time, because the ordinary logging path is silenced the moment a userspace process takes ownership of the console — and that process writes the same serial line. So an unrelated program’s output can land between two characters of a single kernel report. On 2026-09-02 that is exactly what happened on a pull request that touched none of the code involved: a kernel panic reached the log beginning mid-word, the gate’s pattern did not match, and it announced that the defect it was hunting had not reproduced in eight boots — with the panic printed four lines below that sentence, in the gate’s own evidence dump.
A gate whose evidence can be destroyed by an unrelated program fails open, and there is no lock available: the writer the kernel would have to exclude is a process it does not schedule. The repair is a channel with only one writer, and what makes it one is not a convention but the capability model itself. The kernel now reports on a serial port that no capability names — it is absent from every entry in the device table, so the syscall that hands out port access has nothing to hand out. It is not that userspace does not write there; it is that it cannot, and the test proves that by having a userspace process attempt the write in both configurations. Declaring the port makes the write land. Leaving it undeclared makes the identical instruction fault.
It stays on this list, because only the mechanism is fixed. Around twenty existing gates still read the shared console for kernel output and are exposed exactly as before, and migrating them is the remaining work. The first thing the new channel caught, incidentally, was the test written to measure it: it had been proving the console handover by searching the shared console for a marker, which the same hazard ate on one boot in five.
Horus is maintained by one person, and recent pull requests merged with zero reviews. The assurance it can honestly claim is "thoroughly automatically verified", not "independently reviewed". The IPC finding is the demonstration of what that combination produces: a defect that passed every automated gate, because the suite tested the property the author had in mind rather than the property the documentation claimed. This is the highest-leverage open problem on the list, and it is not a technical one.
Until 2026-08-15, not one of the 22 required status checks was a security
gate, including smoke-captest, the capability conformance
suite that is the named witness for eight of the security properties on this page.
That is exactly how the 2026-07 critical finding survived every automated gate.
Promoting it helped; it did not fix the mechanism that produced the omission.
The required list lived only in a branch ruleset that no commit touches, so every
job added to the workflow landed in the advisory set by default and
nothing asked whether it should have. It cost a security gate twice, once for
smoke-captest, and again on 2026-08-16 when the two journal
durability gates landed advisory in the very commit that fixed the defect they
witness.
Since 2026-08-16 the decision is checked in. Every job in all three workflows must be listed as merge-gating, or exempted with a written reason, and CI fails the build if any is in neither; there is no default, because defaulting was the defect. It caught an unclassified static-analysis job on its first run. The intended set is 120 gating and 3 exempted, and the promotions are backed by measurement rather than optimism: across 18 sampled runs, 64 of 66 jobs had zero failures in 1152 job-executions.
A required check can also be required and unable to fail. One of them was, for as long as it took to notice. A job kept from its advisory days the one line that tells GitHub to report it green whatever its steps did; the change that promoted it edited the decision file and the ruleset and never opened the workflow, and a later change rewrote that job's name one line above to delete the word ADVISORY, and left the line. It was not idle: the job failed twice on the main branch inside runs reported green, and the daily ruleset audit could not see it, because that audit compares the names of checks and a masked job publishes the right name with the wrong verdict. Since 2026-08-22 the classifier refuses the combination outright, so a gate cannot be required and unfailable at the same time.
The ruleset was synced toward that set on 2026-08-16, from 22 required checks, so every security test named above blocks a merge. The first attempt required three checks the main branch could not yet produce, which blocks every pull request on a check that never reports, promotion has to lag the job landing by one merge, and a tool now enforces that.
It is not closed yet, but the last gap now has a mechanism.
Reading a ruleset needs the Administration permission, which is not
among the scopes a workflow token can be granted at all, so CI proved the
classification was complete, never that the ruleset matched it, and the two could
diverge through a single change in the web UI with nothing noticing. A scheduled
job now re-checks that daily, authenticating as a GitHub App scoped to this one
repository with read-only administration access, minted per run. The trade is
written down rather than glossed: a credential that can read repository
administration now sits in CI secrets, to detect drift that requires
administration access to cause. That app went live on 2026-08-19:
the scheduled run that morning read the ruleset and reported it matching, where the
run a day earlier had failed on the missing credentials. It failed loudly rather
than skipping for every day it was unconfigured, an audit that quietly skips when
unconfigured is a check that cannot fail, which is why the day it started working
is visible at all.
What is left of this finding is the other half. Writing the required list back needs an administrator's credentials, so it stays a human step: a change that adds a gating job leaves the list one entry behind until someone runs the sync afterwards. The daily audit does not remove that lag; it makes it visible the next morning instead of indefinitely.
The same class of drift, in the documents themselves, is now gated too. An audit on 2026-08-19 found nine stale numbers across five files in one morning, while two other files carried them correctly. The house rule to re-derive every number had been written down the whole time, a rule only a reader enforces fails silently. Each derivable count and every place stating it is now declared in one file, computed from the source, and compared on every merge. Reword a sentence so a declared claim vanishes and that fails too, because a check deleted along with its claim is the same failure wearing a different hat.
Closed 2026-08-17. For eight days the SMP session soak failed at roughly 2–3% per boot and the origin resisted several investigations. It was this: a scheduler switch path published the outgoing task as claimable by another CPU while the CPU making the switch was still executing interrupt-handler frames on that task's kernel stack. A CPU that took the task inside that window resumed it to ring 3, and its very next trap re-entered the interrupt handler on the same stack, at the same depth, running the same functions , rewriting exactly the words the first CPU had not finished reading.
The exactness is why it hid. Two CPUs running the same code at the same depth put the same return addresses and the same stack canary back into their own slots, so every frame validates and every return goes where it should. Only the data differs, and the first datum out is the resume stack pointer the interrupt epilogue is about to load. That accounts for the whole recorded signature: a plausible word from the wrong context, a canary that passed, and a scheduler invariant that read perfectly consistent.
The invariant was never evidence against it, and that is the correction worth publishing. The project had recorded that the shared-stack hypothesis had "nothing observed supporting it", because the one capture taken at the right moment showed the task claimed by exactly the CPU running it. A deliberately reproduced collision prints that same consistent line, because it is true. The task really is running on one CPU. The other one is merely still leaving, and no amount of that instrument would ever have said so.
The claim is now held until the CPU has physically left the stack, released from the interrupt epilogue's first instruction on the new one. The property is checked on every interrupt rather than argued for, and it is S20 in the property table. Two gates settle it in seconds instead of at one boot in 150; a widened-window build with the fix, which must complete a session, and the same widened window with the old release site, which must reproduce the collision. The soak job gates a merge again.
The second path, closed the same day. When a task died and nothing else was runnable, the fault path resumed that CPU on task 0's kernel stack , and every CPU taking that path landed on the same one. This was first written up here as a lead with no witness. It has one now, and the interesting part is how it was nearly missed: on a healthy session the path is never entered, 0 parks in 3 boots, which reads as "unreachable". On a workload that kills tasks on purpose it is entered 5–8 times per boot, and two CPUs were parked on that one stack 2–3 times per boot. A path a test never enters is not a path that cannot be entered. Each CPU now parks on its own stack.
Closing it turned up something else. The per-CPU idle stacks the kernel parks on had no guard page, so the claim that every kernel stack sits above an unmapped guard was false, and had been false independently of this finding, because the scheduler has always parked idle CPUs there. They are guarded now, using each slot's first page so the stack top does not move and the boot trampoline needs no change. The guard check was confirmed by switching the arming off and watching the self-test fail.
The last component was not a scheduler bug at all. The checker that watches for a leaked claim exempts one while the CPU holding it is mid-handover, and it tracked that exemption in a variable the release path cleared before it took the lock that actually drops the claim. For the width of a lock acquisition the claim was held, unexempt, and already being released. A core auditing in that window saw exactly what a leak looks like. It was reading a torn intermediate state of its own bookkeeping. Second time this checker has done that: in August it read a deliberate impersonation the same way.
The natural event appeared on about one boot in twenty-two, with enough variance that two hundred boots could not tell four percent from six. So the window was widened deliberately and set in both arms: with the fix, ten boots of ten are silent; without it, eight of ten accuse. That pair is the evidence; the clean two hundred boots that followed only bound the rate, they do not prove a zero.
Closed 21 August 2026. Closing G-8 stopped a defect that killed every boot of a task-killing workload, and what it uncovered underneath was a second one that had been hidden behind it: at four CPUs, that workload violated the scheduler's claim invariant on roughly 40% of boots. It had never been run at more than one CPU before, so nothing had ever asked.
Wider than first recorded, 21 August 2026. That 40% was measured against a spawn-and-reap stress workload, and the finding was written as though that workload were the whole of it. It is not: the same leak, a claim left behind by a core that then went idle, turned up in the ordinary boot, with no test workload at all, at about one boot in 120. The mechanism is unchanged and the rate is far lower, but the blast radius is the normal path rather than a stress driver. Its gate stays merge-blocking: a red run there is a reproduction worth keeping, not a flake worth re-running.
The cause of one component was a single shared variable. When a task replaces its own image, the kernel hands the interrupt path a note saying "re-enter this task through the fresh context just built for it". That note was one global, and it was read on the way out of every system call on every CPU, with nothing checking that the exec belonged to the CPU reading it. A core that had nothing to do with the exec would take the note, claim that task, install its address space and resume the trap frame the exec had just fabricated, while the core that actually ran the exec was still executing on that very frame. One race, and it accounts for all three recorded symptoms: a leaked claim, a task running with no claim, and two CPUs on one kernel stack.
The storage is per-CPU now, so the sharing is removed rather than guarded, and a one-comparison assertion keeps it that way. Restoring the shared variable on demand reproduces the theft in 5 boots of 20; the fix shows 0 in 30.
This is a narrowing, not a close, and the difference is the point. The workload still fails 2 boots in 30, a claim leaked before any exec runs, and a bogus stack pointer handed back by the dispatcher, so this was a narrowing and the gate whose red flag started all this stayed advisory rather than being promoted back on a partial fix. Both of those have since moved: that gate was promoted on 22 August 2026 once G-9 closed, and the 2-in-30 residue described here is now filed separately as G-12 above, since attributed and fixed. Three earlier explanations for this defect were published-in-progress and were all wrong; each looked right when read and was killed by an instrument. One measurement of the fix even came back clean, because the diagnostic scaffolding still in the build had perturbed the timing enough to hide the remainder. The arm you measure has to be the arm you ship.
Filed 2 September 2026, attributed and fixed 3 September 2026. The residue G-9's own record predicted was real, and it took two weeks of exclusions to find because it was hiding behind three false positives in the checkers that were looking for it. Measured across 2250 boots it appeared on 0.31% of boots, a few hundred milliseconds after the kernel hands control to its first task. Three of its four signatures were not audit reports but memory corruption: a resume stack pointer that is the number one rather than an address, the kernel's own stack canary tripping, and an instruction fetch into a stack address, which is what executing a clobbered return address looks like.
The mechanism is one line of ordering. The function that enters a brand-new task claimed it unconditionally — it wrote “this core owns this task” without asking whether another core already did. And the one place in the running system that calls it published the task as runnable a call earlier. Between those two statements the task is visible to every other core, satisfies every condition the scheduler's selection loop tests, and is owned by nobody. A second core's timer tick landing in that window picks it up, claims it, and starts running it; the first core then arrives and claims it as well. Two cores, one task, one kernel stack, and every symptom above follows from that.
Fixed in two rules, because it was two failures. The entry path now re-checks under the scheduler lock and refuses: a core will not enter a task another core holds, nor one that has stopped being runnable, and parks itself with a report instead. That second clause is not theoretical — with the window held open for sixty milliseconds, the other core ran the task all the way to a blocking wait and gave it back, and the old code entered a blocked task because it had checked before queueing for the lock and never looked again. Separately, the launch site now publishes the task, claims it and makes it current inside a single lock acquisition, so the window does not exist at all.
The obvious alternative was written and thrown away. Claiming first and publishing second leaves a core holding a claim it is not yet running — a gap the claim auditor deliberately does not excuse. Fixing a launch path by widening an exemption in the checker that catches this entire class is the wrong direction, however tidy the diff.
It reproduces on demand now, which it never did before. An instrument holds the entry open until another core takes the task; it is set in every arm, so the runs differ only in the defect. Restore the old ordering and the theft happens on 3 boots out of 3. Take the guard out as well and the two-core collision reproduces on 6 out of 6, printing the exact signature this investigation had been chasing since it was filed. The instrument polls rather than sleeping a fixed time, and that detail was earned: the first version slept, and reproduced the other defect on the same path. An arm that reproduces the wrong one of two defects is an arm reporting the wrong thing.
What is deliberately not claimed. That this accounts for the 0.31%. The campaign that measured that figure was also counting three checker false positives — which is why the rate had already fallen to zero in 3500 boots before this fix landed, on checker repairs alone. The arms establish that the mechanism was real, reachable from an ordinary boot, and is now impossible. The share of the historical rate it owned is not recoverable, and no number here pretends otherwise.
The gate stays exactly as it is. It permits zero failures over thirty boots, which made it red on about 9% of runs while the defect was open — a fact about the defect, not about the gate. Relaxing it at any point in those two weeks would have converted a detector of real memory corruption into a silence, and there would have been nothing left to attribute.
Filed 2 September 2026, closed 3 September 2026. The installer's integration test went red twice on the main branch, both times a five-minute timeout waiting for the install to report success, with the guest having said “formatting” and then nothing at all. No crash, no error, no output. The same step takes six seconds on a workstation.
It was written off as a slow test runner, and then that was rejected on what looked like solid ground: a runner slow enough to turn six seconds into five minutes would have to be fifty times slower, and the boot step in both captures was perfectly normal. Two explanations — a contended runner, or a genuine hang in the format — and nothing to choose between them. The budget was deliberately not raised, which was the right call and left the finding stuck.
The boot step cannot answer that question, and that is the whole finding. Slowing the machine's processors slows the boot and the format together, in lockstep, leaving their ratio unchanged — so that lever would indeed have shown up in the boot step. Contending the disk does something else entirely: the boot stays at full speed while the format triples. Dial the guest's disk down with the emulator's own limiter and the format's cost is a clean straight line in one over the operation rate, while the boot step sits flat at 1.7 seconds at every single point. It is not a poor probe for a slow disk. It is completely blind to one.
The format turns out to be about 4,700 synchronous device operations and only about 2.3 megabytes of data, which is why throughput is the wrong knob and operation rate is the right one. Solve the line for the five-minute budget and it gives roughly sixteen operations per second — and a guest throttled to twelve reproduces the continuous-integration failure exactly, first try, including the normal boot step that had been the reason for disbelieving it.
The repair is not a bigger budget. No total budget can separate the two candidates at any value: raise it and a real hang takes longer to report, lower it and a slow disk fails. They differ in one thing only — whether the machine is still making progress — so that is what the bound measures now. Thirty seconds with no disk operation at all is a wedge; anything still moving is a slow disk and is not a failure. A genuine hang is now caught in thirty seconds instead of five minutes, and the failure says which of the two it saw.
Three ways to measure progress, two of them wrong, in opposite directions. Watching the disk image change declares a hang the moment the format stops writing and starts reading its own metadata back — a two-hundred-second read phase on a throttled disk, and the first implementation failed exactly there. Counting the emulator's read calls instead keeps climbing even when the guest is wedged, because the emulator is polling its serial port; a detector that cannot go quiet cannot fire. What works is asking the emulator for the guest's own device statistics, which move in both phases and stop dead when the guest does. When that channel is unavailable the gate fails closed rather than quietly falling back to the budget it just replaced.
What is deliberately not claimed. That the runner really was that slow on those two days. It is not recoverable: the gate kept no serial log, and both captures survive only as the six hundred characters the timeout message happened to quote. It keeps one now. What the measurement establishes is narrower and enough: a slow disk produces every symptom that was observed, including the one that had been treated as ruling it out.
Found 2026-08-17, closed 2026-08-18, while narrowing the finding above. Everything spawning or exec'ing a program needs while it is in flight; the buffer the executable is staged in, the argument vector, the standard-I/O wiring, the identity of the spawning task, was a single process-wide variable, and nothing serialised two CPUs through any of it. The exec note above was one instance of that pattern; the rest are dealt with below.
The correctness consequence was visible already: an address space could become reachable before its kernel half had been built, which is what a supervisor write-fault in the interrupt-acknowledge path looks like. The consequence that mattered more was about authority; the spawning task's identity was written at the start of a spawn and read much later, so a child's standard I/O could be wired from the wrong parent's capability space. That is authority inherited from a task that never spawned it, which is precisely what this kernel exists to make impossible.
The sharpest of those singletons is now fixed, and it was a memory-safety hole rather than a tidiness problem. When a task slot was reused, the kernel reclaimed the previous occupant's page tables, justified by a comment reasoning that the caller was on the kernel's own address space, so nobody could be walking the tree. That is true of the core doing the reclaim and false of the others: a CPU parked in the idle loop never reloads its address-space register, and a task killed from another core keeps running in ring 3 until its next timer tick, while the slot allocator asks only whether the task is marked dead. So a spawn could recycle the page tables of a task that was still running on them.
The freed frames went straight back to the pool and were handed out as ordinary pages to other tasks, while the first core carried on reading and writing through tables that had come to describe somebody else's memory. That is a cross-address-space read/write primitive reachable from an unprivileged program; no capability required, only the ability to get itself killed at the right moment. It surfaced as a supervisor write fault on the interrupt-acknowledge register, which lives in each task's own low mapping and vanished when its entry was recycled.
Each core now publishes which address space it has loaded, and the reclaim refuses to free one that anybody else still holds, parking it for a later attempt instead of leaking it. Removing the guard on demand reproduces the free-in-use on 20 boots out of 20; with it, the fault goes from 6 boots in 30 to 0 in 30. Together with the exec fix above, the self-test workload that started this went from failing roughly 45% of boots to 2 in 30.
The rest of it closed the next day, in two different ways. The authority half was deleted: the spawning task's identity and the standard-I/O request are arguments passed down the call chain now, not globals read back later, so a child inheriting standard I/O from the wrong parent's capability space stops being unlikely and becomes unsayable. The staging buffer and argument vector keep one copy, a copy per core is real memory for state that belongs to a spawn, not to a core, and every window from arming an image to consuming it is held under one lock instead.
And the honest part: the race this closes cannot be reached by anything this system can currently boot. Rather than quote a rate that does not exist, the window was instrumented, every entry, and every arrival that finds another core already inside, and then deliberately held open for millions of cycles. Across 16 boots at four cores, the window was entered 214 times and never once by two cores at the same time. The reason is structural: every task that spawns anything today is the init process or one of its children, so the busiest spawner cannot be running while init is mid-spawn. Two concurrent spawners is a property of the operating system this is becoming, not of the one it is. So no test claims a rate here, and the arm that removes the lock is kept for the day a workload has two live spawners, a control arm that cannot fail is not evidence.
Still unchanged: a task can be marked dead and still be executing. The guard makes that memory-safe without making it sensible.
Found and closed 2026-08-18, while serialising the window above;
and it is the more serious of the two. A program image is staged in one shared
buffer, and nothing recorded which task had staged it. One system call turns that
from an oddity into a privilege boundary: sudo re-authenticates the
caller and then spawns whatever image is armed as root, in a different
system call from the arming.
So one task arms its own program; a second task types its own correct password; and
the second task's successful sudo launches the first task's
program with root's identity and capabilities. Neither party fails a permission
check. The authority comes from the pairing; the classic confused deputy, and the
same shape as this kernel's oldest defect: authority a caller is trusted for
having rather than for holding a capability to.
Arming an image now records the task that armed it, and consuming one refuses any other, fail closed, including for an image with no recorded owner, so forgetting to record one breaks the spawn instead of quietly restoring the old behaviour. The refusal is audited rather than logged as a failure: a correct password about to elevate somebody else's program is the event worth keeping. The witness asserts both directions in a single boot, a forged foreign owner must be refused, and the task's own image must still spawn, because a check that refuses everything is not a check. Removing the check on demand spawns the foreign image on every boot, 3 in 3.
Measured 2026-08-20, and checked on every merge since. 89 of 97 system calls have their handler actually executed by the three workloads this project tracks, a scripted end-to-end session, the permission conformance suite, and the boot-modules session. The other 8 are each listed with a written reason.
The technique has now found a defect three times out of three. The most recent, on
2026-09-06, was the raw block pair — SYS_BLOCK_READ and
SYS_BLOCK_WRITE, the medium beneath the filesystem — which no
build in this tree had ever entered. Both returned the storage layer's bare
-1 for a block the device refuses, and -1 is the value of
“you hold no capability for this”. A caller could not tell a bad block
from a refusal, and neither could a test: the defect and the thing that hid it were
the same value.
That was 65 until 2026-08-30, and the thirteen that moved cost no new machinery, only a question nobody had asked of the whole list. Twelve of them are dispatched with no central permission check at all, because the authority they need depends on which object the caller names and so has to be tested inside the call itself. That makes their implementation reachable by a program holding nothing, so a test proving the call says no is a test that ran it. The same argument had already promoted three separate groups of calls; it had simply never been applied to the rest. Two more were left alone on purpose, one blocks waiting for a keystroke, and one would return at its first line because the feature it reports on is not built into these images, which would raise the number without testing anything.
The conformance suite is a refusal suite by design: it checks that a program without permission is turned away, and a refusal is decided before the call's body ever runs. So a call can be named by the suite, counted as tested, and have its implementation never once execute — which is precisely what happened, and why a fault reproducible for every fixed variable in the system survived a hundred passing checks.
This page used to say that nothing on the uncovered list was known to be broken. That has now been wrong twice. In August, three of the calls on it turned out to share a helper that spun forever holding a lock with interrupts off, reachable by any unprivileged program in a single call. On 1 September, writing the program that would finally run the audit calls — a task holding exactly one permission and nothing else — found a fault on its first boot: the record the kernel sends back was described in two places, 256 bytes in the kernel and 72 in the header programs compile against, under the same name. Every field was read from the wrong place, and the kernel wrote 184 bytes past the end of the array it was handed, for every record. It is confined to the program that asked, and it is the same class of fault as the one that started all of this. There is now one description of that record, which both sides compile and both sides check the size of.
The pattern is worth stating plainly, because it is the argument for the whole exercise: both faults were found by the act of running the code, not by reading it, and neither could have been found by widening the conformance suite — both calls are gated on a permission that suite deliberately does not hold.
The build can record the first time each call's body is entered and say so on the wire, and a checked-in file classifies all 97 implemented syscalls, covered or not covered with a reason. The check fails if a call is in neither list, if a covered one stops being exercised, if an uncovered one starts being exercised and its reason has gone stale, or if the recording produced nothing at all. That last case is the one that would otherwise let the whole check pass while measuring nothing.
It deliberately does not demand all 96. That would be a large amount of test-writing wearing the costume of a guarantee. What it demands is that the number be decided rather than drifting, and that every gap be written down; the same bargain this project already makes with which tests are allowed to block a merge. The pipe family used to be the cheap example here — untested only because no scripted session ran a command pipeline, a gap in the script rather than in the kernel. It is covered now. What is left is eight calls, in five groups: three answer to a capability the conformance suite deliberately does not hold, and one of those three formats the attached disk, so no tracked workload can enter it without destroying the volume the run is using; one is reached only on a start-up failure path, which a tracked workload would have to break itself to take; two would SUCCEED, and either duplicate the caller or replace its image; one blocks on a keystroke; and one enters a body that returns at its first line, because the feature it reports on is compiled out of every tracked image.
Found and closed 2026-08-20, while writing the witness for the finding below. Two system calls, reading the kernel log, and fetching the audit digest, took the address of the caller's buffer and threw away its upper half before handing it to the kernel. The registers that carry it are twice that wide, so nothing required the loss; it was a stray cast. The kernel then did exactly what it was told, with an address the program had never named.
It survived because of where things live. Programs are loaded at a random address far above the four-gigabyte line, so every fixed variable in every program was affected, always, while a temporary on the call stack sits low enough to be untouched, and every caller in the system happened to use one. The two conformance checks that name these calls both test that a program without permission is refused, and a refusal is decided before the address is ever looked at. So a fault that was perfectly reproducible for an entire class of buffer was invisible to a hundred-check suite.
It was also not safe-by-default, which is the part worth being plain about. The symptom that exposed it (a refusal) is what happens when nothing occupies the truncated address. When something does, and the low addresses are occupied by the stack and the heap, the kernel writes its data into a page of the program's memory that the program never nominated. It stays inside that one program and reaches no other, so this is corruption rather than a broken permission boundary. But it undoes any claim of the form "we checked the address we were given", because the address checked was not the address given.
The repair is one cast in each call. The part that matters is the check that now refuses to build the system if any such call narrows an address again, decided by reading the source, so it covers every one of them, including calls nothing uses yet, rather than only those some test happens to exercise. The obvious way to defeat a per-call check is to weaken the shared helper they all use, so that is checked separately. And the test that first hit this now deliberately uses a fixed variable rather than a temporary, with an explicit assertion that it really does sit above the line, so the day it stops testing this, it fails instead of quietly passing.
The first diagnosis was wrong, and the correction is on the public issue. The kernel appeared to disagree with the processor about the program's memory map; measurement showed the two agreed exactly, and the kernel was faithfully consulting a different address. The observations were right and the conclusion was not; it pointed at the memory-management code for a defect that lived in a header.
Closed 2026-08-20. Reading the kernel message log has required an
unforgeable token since July, when identity-based authority was retired: a program
runs dmesg only if it holds the capability for it. Writing to that same
log required nothing whatsoever. Every ordinary write to standard output was appended
to the log on its way to the terminal, so any program at all could put lines into
dmesg that a reader cannot tell apart from the kernel's own, and could
push 16 KiB of noise through to evict every real line, since the log is a fixed ring
that overwrites its oldest entries.
That is an anti-forensics tool aimed at exactly the record someone reads after an incident, and it is worth being precise about why it existed: converting "who may read this" into a capability says nothing about who may write it. The sweep that fixed the read side was organised by system call rather than by object, so the write side was never a question anyone asked.
The two destinations are now gated differently, which is the distinction the old code never drew. The bytes still reach the terminal with no permission asked, writing to your own screen is not an authority this system rations. They reach the kernel's log only if the program holds the log capability with the write right. The gate asks the capability graph and nothing else; asking the user id here would have recreated the very defect this project spent July removing.
It closes the finding rather than narrowing it, for a reason that lies outside the check itself: the log capability is minted read-only at the root of the system, and delegation can only ever hand out less than you hold, so no program can obtain the write right at all. The authority remains expressible for the day something legitimately needs it, without being granted to anything today. Removing the append outright would have been fewer lines and would have closed that door permanently.
The witness is a program that is given the log capability and still refused. It holds the read right (so it can read the ring back and check its own work) and is denied the direction it was not given, which is a stronger claim than a program holding nothing being denied everything. It pushes 28800 bytes through standard output, more than the ring holds, and requires both that none of it appears in the log and that a marker placed there beforehand survives. Both are checked before either is reported, so removing the gate on demand reproduces both failures at once, 3 boots in 3, a fix that only rate-limited would keep the marker and still forge.
Endpoints are bounded FIFO queues, reply capabilities are one-shot, and
SYS_IPC_RECV_BLOCK sleeps on an empty queue, a server with no work is
off the run queue rather than spinning. What is still missing is priority
inheritance: the kernel records that a task is waiting on an endpoint, which is the
prerequisite, but nothing propagates priority along that edge, and there are no task
priorities to propagate yet.
Found 2026-08-19, by fixing the step that had been hiding it. The
kernel image is byte-for-byte reproducible and gated on every merge. The ISO; the
thing anyone would actually download, is not, and the cause is not this project's
code: grub-mkrescue stamps a marker named for the wall-clock second
into every image it builds, and embeds that identifier in the three EFI loaders it
generates. Extract two ISOs of one build and diff them and every file this project
authors is identical; only those four grub-generated objects differ.
It went unseen because the step that recorded the build's hashes could not fail. It hashed two artifacts over a build that made only one, discarded the error naming the missing file, discarded the exit status, and announced success, so the record had always held a single line and the ISO had never been compared to anything. That step now refuses an incomplete build and writes nothing when it refuses, with the old behaviour kept as a switch that must reproduce the failure on demand.
The first measurement of this was wrong, in the reassuring direction. Two ISOs built back to back came out identical, which read as proof of reproducibility. They matched because both builds landed inside the same wall-clock second. Repeat the pair across a second boundary and they differ. A measurement fast enough to be convenient was fast enough to be wrong.
ChaCha20, SHA-256, BLAKE2b, Argon2 and the AEAD are all from-scratch
no_std Rust implementations checked against published test vectors.
None has been independently audited and none is verified constant-time. Treat them
as research code.
User copies clamp and return success rather than refusing (C-4). The heap syscalls
do 32-bit arithmetic on 64-bit bounds, latent until the user address space widens
past 4 GiB (I-2). The revocation closure was bounded at 256 entries and
over-approximated on overflow, which an unprivileged task could force as a
denial-of-service against a peer's independent capability to the same object; it
marks in place and iterates to a fixpoint since 2026-08-16, so it is exact at any
subtree size (I-3).
There are no tagged releases, no signed artifacts and no SLSA provenance, so a third
party cannot verify that a horus.iso came from this repository's CI
(I-9). A frame spans at most 64 pages, which is the untyped arena's bound rather
than the design's; that arena is 4 MiB in total and shared with every other kernel
object, so a frame able to span it would be a denial-of-service against every other
object class dressed up as a feature. Formal verification is
narrow: Kani covers revocation and the ELF validator, and there is no TLA+
specification — the two committed in June were removed in September as
unsound rather than merely unchecked.
Horus boots, runs an unprivileged init that supervises an unprivileged
shell, and enforces capability-based access control end to end, including across the
IPC namespace. The infrastructure around it, reproducible builds, measured boot,
adversarial CI, formal proofs, is substantially more mature than the kernel it
verifies.
This is a research and learning kernel, not a shipping operating system. Nothing here should be trusted with anything real.
Ordered by assurance value, not by how well it demos.
Track 0: making the object model true, is complete. IPC is
capability-addressed, ambient uid == 0 authority is retired, and creating
a kernel object is now an exercise of authority the capability graph describes.
Track 1 is the current work: making boot-time interrupt enablement explicit and then landing the per-CPU, interrupt-preserving lock; a blocking receive to finish the IPC primitive; fail-closed user copies; 64-bit-clean heap arithmetic; a durable journal; and an unbounded revocation closure.
Track 2 grows the operating system on top of that: frame capabilities
and shared memory, a monotonic clock and timers, a real process and session model;
fork and the capability space a child inherits are in, a VFS with
several filesystems, dynamic linking, and a network stack as an unprivileged server
holding one network card’s capability, a sentence that only became sayable
on 2026-08-28, when a device capability started naming a device instead of conferring
the console.
The single highest-leverage change is not technical. It is finding a second reviewer for the capability paths, automated verification has already been pushed about as far as it goes without one.