There's a dirty secret about writing a kernel in Rust.
Rust's memory safety — the whole reason you'd choose it over C — is conditional. It holds everywhere you don't write unsafe. The moment you do, the compiler steps back and trusts you completely. You're back to being on your own.
In a traditional kernel, unsafe is everywhere. Page tables. Interrupts. CPU registers. Memory-mapped I/O. Context switches. If you write a kernel in Rust and scatter unsafe across 500 files the way Linux scatters void *, you've bought yourself a kernel that's written in Rust. You haven't bought yourself a kernel that's memory-safe. Those are different things.
So when we started the Cyphera Kernel, the first real architectural question wasn't the scheduler or the VFS. It was: where does unsafe live, and how do we keep it contained?
Three options on the table
We thought through three approaches.
Option 1: just write a monolithic kernel and put unsafe where you need it. This is what most Rust kernel projects do in practice. It's reasonable — you're writing a kernel, unsafe is unavoidable, so you use it. But the audit problem is the same shape as Linux. If unsafe is in your scheduler, your filesystem, your network stack, your ELF loader — anything in any of those layers can corrupt memory and you have to audit all of it.
Option 2: microkernel. Hardware-enforced isolation. Each component runs in its own protection domain and communicates over IPC. The unsafe surface for each component is small by construction. seL4 takes this furthest: formally verified, tiny TCB.
We rejected this one. The reason is the workloads we're targeting: databases, web servers, anything syscall-heavy. Microkernels lost the cloud market because IPC is expensive. A read() on a microkernel goes: userland → kernel → IPC to the FS server → IPC reply → kernel → userland. On a monolithic kernel it's: userland → kernel → FS code → userland. For a database doing millions of I/O operations, that overhead compounds. We wanted PostgreSQL to actually run well, not just run.
Option 3: framekernel. Rust's type system as the privilege boundary, instead of hardware isolation.
What the framekernel pattern is
I found this in a published paper: Peng et al., "Asterinas: A Linux ABI-Compatible, Rust-Based Framekernel OS with a Small and Sound TCB," USENIX ATC '25. There's an earlier version from APSys '24 too. Genuine credit due — I read the paper and thought: that's exactly the right answer. The Cyphera Kernel is independently designed and built (clean-room — we read the paper, not the source), but the concept of using Rust's type system to enforce a privilege boundary comes from their published research. Worth reading if you're doing anything in this space.
The idea:
- One crate — in Cyphera's case,
frame/— is the only placeunsafelives. All of it. Everyunsafeblock in the entire kernel workspace is in there, each one with a// SAFETY:comment explaining why it's correct. - Every other crate —
kernel/, the scheduler, the VFS, the network stack, the ELF loader — carries#![forbid(unsafe_code)]at the crate root. Notdeny. Forbid. The compiler will refuse to build if you add an unsafe block. This isn't a convention. It's a compile-time guarantee. - A CI step (
check-unsafe-boundary.sh) runs on every PR and confirms the attributes are present. You can't quietly remove them.
There's no IPC. kernel/ calls frame/ functions as ordinary Rust function calls — they're in the same address space, linked together. The performance matches a monolithic kernel. The isolation is enforced by the type system and the compiler, not by message-passing across protection rings.
frame/ exposes typed capabilities, not generic interfaces. Not void *, not raw page numbers. Frame, PhysAddr, VirtAddr, PageTable, MmioRegion<T>, IrqHandle. You can't accidentally use a physical address where a virtual one is expected. The type system makes the categories distinct.
What this means in practice
Right now, frame/ is 3,693 lines of Rust and 454 lines of hand-written x86_64 assembly at time of writing — the entire unsafe surface of the kernel, 6.7% of the codebase. Every page table operation, every interrupt handler, every MMU operation — in one place, all auditable.
The complete set of hardware-touching operations: port I/O, MSR reads and writes, page-table manipulation, IDT vector setup, the syscall trampoline. That's the list. Each one is exposed to kernel/ as a typed, safe interface — not a raw pointer, not a void *, not a prayer.
kernel/ is the other ~80% of the kernel. The scheduler. The VFS. ext4. Signals. Futex. ptrace. The ELF loader. All of it is #![forbid(unsafe_code)].
That means: given a sound frame/, a bug in the scheduler cannot corrupt memory. The type system prevents it, not the programmer's vigilance. A bug in the ELF loader cannot dereference an invalid pointer. A bug in the ext4 implementation cannot write to arbitrary memory through the safe API. The compiler enforces this at build time — and the burden of correctness sits squarely on frame/, which is exactly where we want it.
The bug classes that cannot exist in kernel/: use-after-free, double-free, data races on shared state, uninitialized reads, type confusion. Not reduced. Eliminated.
Is frame/ itself bug-free? No. We use Kani — more on that in the next post — to formally prove invariants on the allocator and the lock hierarchy, but Kani has bounded verification — it proves things for bounded input sizes, not all possible states. frame/ is where the hard problems live. It's where you'd look first if something went wrong.
But it's ~4,100 lines at time of writing. Not 30 million.
The honest tradeoffs
The framekernel pattern has a cost. frame/ has to expose a safe API that covers everything kernel/ needs — otherwise kernel/ would have to reach around it, which defeats the point. Designing those safe abstractions is real work. When we added a new subsystem and kernel/ needed a primitive frame/ didn't expose yet, someone had to design the right typed interface and add it.
The other cost: this is a newer pattern. Less battle-tested than monolithic kernels, fewer examples to learn from. We're finding edge cases the approach doesn't have established answers for yet.
Whether the tradeoff is worth it: I think so. Having a formally bounded unsafe surface that the compiler enforces is a fundamentally different security posture than "we tried really hard not to make mistakes." For the confidential computing use case we're building toward — where the whole point is a small, auditable TCB — this is the right foundation.