Microkernel

A microkernel is an operating-system kernel that runs in privileged hardware mode only the parts that absolutely must be privileged: thread switching, address-space protection, traps and interrupts, and inter-process communication. Everything else (file systems, device drivers, network stacks) lives in ordinary user-mode processes and talks to the rest of the system through IPC. The argument was made concrete by Jochen Liedtke’s 1995 paper “On µ-Kernel Construction” and his 1996 CACM paper “Toward Real Microkernels,” which showed that the slow first-generation microkernels (Mach, Chorus) had been slow because of poor implementation, not because of the microkernel idea (Liedtke, “Toward Real Microkernels,” CACM Sept 1996). The seL4 microkernel later carried the idea to formal verification, proving correctness of a ~10,000-line C kernel against its specification (Heiser, The seL4 Microkernel: An Introduction, 2025).

Resolved 2026-08-08

The primary paper is now in hand and the minimality principle is quoted verbatim below, in the section on Liedtke’s L3, L4, and the second generation. The 1995 SOSP paper PDF fetched at HTTP 200 from the Karlsruhe Institute of Technology operating-systems group mirror, os.itec.kit.edu/downloads/publ_1995_liedtke_ukernel-construction.pdf, and independently at HTTP 200 from the UNSW cs9242 course mirror; the two extractions agree word for word. Bibliographic record: 15th ACM Symposium on Operating Systems Principles (SOSP ‘95), Copper Mountain Resort, Colorado, 3–6 December 1995, pp. 237–250, DOI 10.1145/224056.224075 (note the correct DOI prefix is 224056, not the 224057 recorded in an earlier draft of this note). The wording is corroborated by Elphinstone and Heiser, who reproduce the same sentence verbatim in “From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels?”, SOSP 2013, §3.1.

One transcription caveat: the 1995 PDF is a 1994-era dvips/Distiller artefact whose Greek µ glyph is a bitmap font that text extraction drops, so every µ-kernel comes out of pdftotext as -kernel. The µ characters in the quotations below are restored from the paper’s own title and from Elphinstone and Heiser’s independent verbatim rendering; no other character has been altered. Where a sentence in the original contains a glyph that cannot be recovered with confidence, the quotation starts after it rather than guessing.

Why Anyone Would Build One

In a monolithic kernel like Linux, every file system, every device driver, every network protocol runs in supervisor mode with full access to memory and hardware. The kernel is one address space, and a bug in any one of those components (a USB driver, an NFS client, the TCP stack) can scribble on any other and corrupt or crash the whole system. The Linux kernel comprises “of the order of 20 million lines of source code (20 MSLOC); we can estimate that it contains literally tens of thousands of bugs” (Heiser, seL4 whitepaper, section 2.1). The set of code that must be correct for system security is called the trusted computing base (TCB), and on Linux the TCB is the whole kernel.

The microkernel design is the opposite extreme. Push every service into a user-mode process. Now a bug in the file-system server can corrupt only the file-system server’s address space; the kernel keeps running, the network stack keeps running, the other processes keep running. The TCB shrinks from twenty million lines to roughly ten thousand. Of the known critical Linux compromises, “29% would be fully eliminated by a microkernel design, and another 55% would be mitigated enough to no longer qualify as critical” (Biggs et al., 2018, cited in the seL4 whitepaper section 2.1).

The trade is performance. Where a Linux file read is one syscall (a single kernel entry), a microkernel file read is at minimum two IPCs (application → FS server → application). If IPC is slow, the whole system is slow, and that is precisely what killed the first-generation microkernels. Mach 3 on a 486DX-50 needed “about 115 µs per IPC, compared with about 20 µs for a conventional Unix system call” on the same hardware: roughly an order of magnitude penalty per call (Liedtke 1996 CACM).

Mental Model

flowchart TB
  subgraph MONO["Monolithic kernel (Linux-style, ~20 MSLOC in privileged mode)"]
    APP_M["App"]
    VFS["VFS, FS, net, drivers, scheduler, paging<br/>(everything in kernel mode)"]
    HW_M["Hardware"]
    APP_M -- "syscall" --> VFS
    VFS --> HW_M
  end
  subgraph MICRO["Microkernel (L4 / seL4, ~10 kSLOC in privileged mode)"]
    APP_U["App"]
    FS["FS server"]
    NET["Net stack"]
    DRV["Disk driver"]
    KERN["Microkernel:<br/>traps, threads, IPC, address spaces"]
    HW_U["Hardware"]
    APP_U -- "IPC" --> FS
    FS -- "IPC" --> DRV
    APP_U -- "IPC" --> NET
    NET -- "IPC" --> DRV
    APP_U --> KERN
    FS --> KERN
    NET --> KERN
    DRV --> KERN
    KERN --> HW_U
  end

Monolithic vs microkernel architecture, redrawn from the seL4 whitepaper Figure 2.1. What it shows: on the left, every OS service runs in kernel mode and a bug anywhere compromises the system. On the right, the kernel is reduced to a small core (traps, threads, IPC, address spaces); file systems, network stacks, and drivers are normal user processes that the kernel only multiplexes. The insight to take: the microkernel’s job is not to provide services. It is to make user-mode processes the right substrate for providing services, by giving them protected memory, fast IPC, and direct access to specific hardware via the trap and interrupt machinery.

A Brief History

The first generation: Mach and Chorus (1985-1995)

Mach grew out of Richard Rashid’s group at Carnegie Mellon, with development running 1985-1994 (Wikipedia, “Mach (kernel)”). Its four abstractions, task (an address space and its resources), thread, port (a protected message queue), and message, all-but defined what a microkernel was. It replaced Unix syscalls with messages to ports, letting servers outside the kernel implement what the kernel used to. Mach 3.0 was the pure-microkernel revision; everything except the kernel itself was meant to run as a user-mode server.

The problem was performance. “Mach 3.0-based UNIX single-server implementations were about 50% slower than native UNIX” on contemporary hardware (Wikipedia, “Mach (kernel)”). Chorus, the parallel French effort, fared similarly. The disappointment was severe enough that “both Chorus and Mach reintegrated the most critical servers and drivers into the kernel” (Liedtke 1996 CACM). The pure microkernel was, in practice, an academic curiosity. The XNU kernel underneath macOS and iOS uses a Mach core but is “a heavily modified hybrid Open Software Foundation Mach Kernel” with the file systems, networking and VM living inside the kernel: not really a microkernel any more (Wikipedia, “Mach”).

Liedtke’s L3, L4, and the second generation (1988-1996)

Jochen Liedtke, working first at GMD (the German national IT research lab) and later at IBM Research, built L3 from 1988 as the pragmatic counter-example to Mach. L3 took roughly 10 microseconds for an RPC round-trip where Mach took 115 (Liedtke 1996 CACM; Liedtke 1995 SOSP, as summarised in the MIT review notes). His 1993 SOSP paper “Improving IPC by Kernel Design” laid out the implementation techniques (lazy scheduling, virtual registers, careful cache-line packing); his 1995 SOSP paper “On µ-Kernel Construction” argued the design principle that justified them.

The 1995 paper introduced L4, a clean-slate redesign with only three abstractions: address spaces, threads, and IPC. L4 implemented “only seven system calls, and needs only 12 Kbytes of code. Across-address-space IPC on a 486-DX50 takes 5 µs for an 8-byte argument and 18 µs for 512 bytes,” compared to Mach’s 115 µs and 172 µs respectively (Liedtke 1996 CACM). The L4 RPC was about twice as fast as a conventional Unix syscall on the same hardware. Liedtke’s argument was that microkernel slowness “was due to poor implementation choices rather than architectural limitations” (Seltzer course notes on Liedtke 1995).

The 1995 paper also articulated two principles that the field still cites. The first is the minimality principle, and because it is quoted (and misquoted) so often, here it is verbatim, in full, from section 2 “Some µ-Kernel Concepts”, page 2 of the paper:

In this section, we reason about the minimal concepts or “primitives” that a µ-kernel should implement.¹ The determining criterion used is functionality, not performance. More precisely, a concept is tolerated inside the µ-kernel only if moving it outside the kernel, i.e. permitting competing implementations, would prevent the implementation of the system’s required functionality.

— Jochen Liedtke, “On µ-Kernel Construction”, SOSP ‘95, §2

Three details in that sentence do real work and are usually lost in paraphrase. “Tolerated”, not “included”: the default is exclusion, and anything inside the kernel is there under sufferance and must justify itself. “i.e. permitting competing implementations” is the operational test — the question is not “is this code small?” but “could two different user-level implementations of this concept coexist?”; if they could, the concept does not belong in the kernel. And “the system’s required functionality” makes the criterion relative to a stated requirement rather than absolute, which is why an L4 for a real-time system and an L4 for a general-purpose system can legitimately draw the line in different places. Elphinstone and Heiser call this “a more pointed formulation of ‘only minimal mechanisms and no policy in the kernel’” and note that it “has continued to be the foundation of the design of L4 microkernels” (Elphinstone & Heiser 2013, §3.1).

The second is the non-portability principle. Section 5 of the same paper, titled simply “Non-Portability,” places the microkernel at the boundary between a minimal set of abstractions and the bare processor, and concludes: “The performance demands are comparable to those of earlier microprogramming. As a consequence, µ-kernels are inherently not portable. Instead, they are the processor dependent basis for portable operating systems” (Liedtke 1995, §5). The paper’s own conclusions repeat it in imperative form: “Similar to optimizing code generators, µ-kernels must be constructed per processor and are inherently not portable. Basic implementation decisions, most algorithms and data structures inside a µ-kernel are processor dependent.” The microkernel should be carefully tuned for each architecture it targets; the portability lives one level up, in the servers.

L4 grew into a family: L4Ka::Hazelnut (1999, the first C++ implementation), L4/Fiasco (TU Dresden, 1998-, pre-emptible for real-time work), L4Ka::Pistachio (2001, portable across architectures), OKL4 (shipped on “billions of Qualcomm cellular modem chips” and the iOS secure enclave) (Heiser, seL4 whitepaper, section 2.2; Wikipedia, “L4 microkernel family”).

Third generation: seL4 (2009 onward)

seL4 was the line’s culmination. Developed at NICTA in Sydney from roughly 2006, it pushed beyond performance into formal correctness. In 2009 the team published “the world’s first OS kernel with a machine-checked functional correctness proof at the source-code level” (Heiser, seL4 whitepaper, section 3; [Klein et al., SOSP 2009]). The kernel is roughly 10,000 lines of C plus a small amount of assembly; the proof is roughly half a million lines of Isabelle/HOL script, a 50:1 proof-to-code ratio (Wikipedia, “seL4”). The proofs have since been extended to integrity, confidentiality, and bounded worst-case execution time. seL4 was open-sourced by NICTA in 2014 and now lives under the seL4 Foundation at UNSW; it won the 2023 ACM Software System Award.

seL4 is also the only widely-deployed microkernel built on capabilities: every kernel object is named by an unforgeable token, and the kernel’s access checks are reduced to “does the caller hold the right capability for this object.” There is no global namespace of “file /etc/passwd” for the kernel to interpret. A user-mode server can grant a capability to another process, but only if it holds it itself, which makes the principle of least authority enforceable rather than aspirational.

The other living microkernels: QNX and MINIX 3

QNX Neutrino, designed by Gordon Bell and Dan Dodge of Quantum Software Systems (Waterloo, 1980, renamed QNX in 1984), is the longest-running commercial microkernel. Its kernel (named procnto) “contains only CPU scheduling, interprocess communication, interrupt redirection and timers” with all other services as user-mode processes (Wikipedia, “QNX”). After BlackBerry’s 2010 acquisition, QNX shipped in roughly 275 million vehicles globally; it is the dominant car-infotainment, telematics, and ADAS operating system. QNX’s IPC is a synchronous MsgSend: “the message is copied, by the kernel, from the address space of the sending process to that of the receiving process” with no kernel involvement in marshalling or buffering.

MINIX 3 is Andrew Tanenbaum’s microkernel-revival project from 2005. Roughly “4,000 lines of C code” in the kernel itself, with drivers and servers as user processes (Wikipedia, “MINIX 3”). Its distinctive feature is the reincarnation server, a userspace process that monitors all drivers and “automatically terminates and restarts” any one that fails or hangs, giving the system a self-healing property monolithic kernels cannot offer. MINIX 3 became, by some accident of history, the most-deployed microkernel: it is the OS that runs on Intel’s Management Engine inside every Skylake-or-later Intel CPU, “potentially making it the most widely deployed OS on x86/AMD64 systems” (Wikipedia, “MINIX 3”).

Mechanical Walk-through: What the Microkernel Actually Does

A microkernel’s responsibilities collapse to four categories.

1. Trap and interrupt entry. When a hardware trap (page fault, illegal instruction, syscall, external interrupt) fires, the CPU jumps to the kernel’s vector. The kernel saves registers, identifies the cause, and either handles it directly (if it concerns scheduling or IPC) or forwards it as a message to a registered user-mode handler. In L4, an external interrupt is delivered as an IPC message to the driver task that owns the device (Liedtke 1996 CACM).
2. Thread scheduling. Picking which thread to run next when one blocks or a timer fires. The simplest viable scheduler is Round-Robin Scheduling; production microkernels typically run a small priority queue with explicit yield. seL4 famously uses a mixed-criticality model that supports both round-robin and preemptive priority scheduling in the same kernel (Heiser, seL4 whitepaper, section 5).
3. Address-space management. The kernel programs the CPU’s memory protection (MMU page tables on a full processor; PMP on a small RISC-V chip without an MMU) so each user process can see only its own memory. L4 expressed this as three primitives: grant (transfer a page from one address space to another), map (share a page across address spaces), and demap (revoke a shared page) (Liedtke 1996 CACM). seL4 generalises this with capabilities that name memory regions.
4. IPC. A synchronous rendezvous (sender blocks until receiver is ready, no buffering) is the simplest and the L4/seL4 default; see Synchronous IPC. The kernel’s IPC fast path is, by far, the most performance-sensitive code in the system; L4’s whole performance argument is “make this path 5 microseconds instead of 100.”

Everything else, opening a file, sending a packet, reading a sensor, is implemented as one or more user-mode servers that talk to each other and to driver processes over IPC. The kernel is involved only to route the messages and to switch the address space when the message crosses a process boundary.

Configuration / Code

A skeleton system call dispatcher for a very small RISC-V microkernel in Rust, illustrating the “everything is IPC” structure. The kernel itself implements only thread switch, IPC, and address-space update:

// In M-mode trap handler, after registers are saved.
pub fn trap_dispatch(cause: usize, mepc: usize, regs: &mut TrapFrame) {
    match Cause::from(cause) {
        // Software interrupt: scheduler tick or cross-hart wakeup.
        Cause::SoftwareIrq => scheduler::tick(),
        // Timer interrupt: from CLINT, drive scheduler.
        Cause::TimerIrq    => scheduler::on_timer(),
        // External interrupt: claim from PLIC, post message to driver task.
        Cause::ExternalIrq => {
            let src = plic::claim();
            if let Some(handler) = drivers::lookup(src) {
                ipc::post_message(handler, Message::Irq { src });
            }
            plic::complete(src);
        }
        // ecall from user mode: dispatch the syscall.
        Cause::UserEcall => match regs.a7 {
            SYS_IPC_SEND => ipc::send(regs.a0, regs.a1 as *const _, regs.a2),
            SYS_IPC_RECV => ipc::recv(regs.a0 as *mut _),
            SYS_YIELD    => scheduler::yield_now(),
            SYS_GRANT    => vm::grant(regs.a0, regs.a1, regs.a2),
            _            => Err::BadCall,
        },
        Cause::PageFault => {
            // Forward to the faulting task's pager via IPC.
            let pager = current_task().pager;
            ipc::post_message(pager, Message::PageFault { addr: regs.badaddr, mepc });
        }
        _ => panic!("unhandled trap {:?}", cause),
    }
}

Line-by-line: software, timer, and external interrupts are all dispatched as IPCs to the right userspace handler; the kernel does not itself decide how to handle a UART RX byte, it just posts a message to whoever owns the UART. Syscalls are a small fixed set: send, receive, yield, grant. Page faults are forwarded as messages to a userspace pager rather than handled in the kernel. This dispatcher fits in a few dozen lines; the size of the whole privileged-mode kernel comes from a careful implementation of ipc::send and scheduler::tick, not from policy code.

Failure Modes and Common Misunderstandings

• “Microkernels are slow” is true only of the first generation. L4 IPC at 5 microseconds is faster than a Linux syscall in absolute terms (Liedtke 1996). seL4 IPC on modern hardware is around 100 cycles. The latency penalty for a syscall-equivalent operation in a well-designed microkernel is one extra address-space switch, not orders of magnitude.
• “Microkernels prevent system-wide bugs” is true only with discipline. A microkernel can still be brought down by an erroneous server if the server holds a privilege the kernel cannot protect against (e.g. a disk driver issues a wild DMA write). Hardware IOMMUs and capability discipline are required to actually realize the isolation.
• “Drivers in user-mode are necessarily slower” is false. Liedtke notes: “user-level drivers perform as well as integrated drivers” once IPC is below 10 µs (Liedtke 1996 sidebar). The cost of a driver crossing privilege levels is dominated by the IPC, not by hardware mode switching, which “are only 3%–7% of the measured costs.”
• Capabilities are not POSIX file descriptors. A POSIX fd is a small integer that the kernel looks up in a per-process table. A capability in seL4 is an unforgeable token; the kernel does not look up a name, it checks that the bits the caller presents are valid. This is the difference between “I have a file descriptor named 7, please ask the kernel what it points to” and “I am holding the capability that lets me read this object.” It eliminates a whole class of confused-deputy bugs.
• Microkernels are not necessarily smaller than monolithic kernels’ source. seL4 the kernel is 10 kSLOC, but the total useful system includes the file-system server, network server, drivers, etc., which together can dwarf a Linux kernel’s “interesting” subset. What microkernels minimize is the privileged TCB, not total LOC.

Alternatives and When to Choose Them

• Monolithic kernel (Linux, BSDs, Windows NT). Choose when you need an enormous device-driver ecosystem and the entire Unix userland working out of the box. Pay the cost in TCB size.
• Hybrid kernel (XNU under macOS/iOS, Windows NT in practice). A Mach-style core with the file systems and drivers integrated. You get Mach’s IPC primitives and threading but Linux’s monolithic performance characteristics; you also get neither the verification story of a true microkernel nor the simplicity of a monolithic one.
• Exokernel (MIT, 1995). A different reaction to Mach’s slowness: don’t have abstractions at all; expose hardware primitives and let library OSes in userspace build whatever model they want. Excellent performance, very few real-world deployments.
• Unikernel (Mirage, IncludeOS). Fuse application and OS into one address space and run the whole thing on a hypervisor for isolation. Faster than microkernels for single-purpose systems, useless for general-purpose multi-tenant systems.

For a small from-scratch hobby SoC the choice is between a tiny monolithic kernel and a microkernel. A microkernel is the better fit for the definitely-not-esp32 project for three reasons. First, the codebase is small enough that the kernel proper fits comfortably in roughly 5,000 lines of Rust; the L4-class abstractions match the chip’s hardware almost one-to-one. Second, the microkernel’s structure makes it natural to bring up servers incrementally: the kernel can come up first, then a UART driver server, then a scheduler, then a filesystem, each independently testable. Third, the educational payoff is higher: a microkernel forces you to be honest about every privileged-mode operation rather than letting them accumulate inside a giant kernel blob.

Production Notes

• seL4 deployments: secure cross-domain solutions in defence, certified avionics, the DARPA HACMS program (which embedded seL4 “in a range of autonomous vehicles, ranging from trucks, a land robot, and a quadcopter to Boeing’s Unmanned Little Bird helicopter”), and a growing number of embedded automotive use cases. The SMACCM sub-project under HACMS ran 4.5 years across Rockwell Collins, Data61/NICTA, Galois, Boeing, and the University of Minnesota; in the end-of-project demonstration “the HACMS Red Team… was unsuccessful at compromising the security of the helicopter, in flight” even when given the keys to the in-VM camera task (Trustworthy Systems, SMACCM project page; seL4 in use). The seL4 Foundation tracks ports across ARM, x86-64, and RISC-V 64.
• QNX: in roughly 275 million vehicles, in industrial control, in medical devices. Famously, the Cisco IOS XR carrier-grade router operating system is QNX-based. Hard-real-time guarantees are its main selling point.
• MINIX 3: runs on Intel ME inside the majority of x86 hardware shipped since 2015. Tanenbaum learned of this deployment from the press, not from Intel.
• OKL4 / Trustworthy Systems: on every Qualcomm Snapdragon’s secure baseband processor and Apple’s Secure Enclave (descended from the L4-embedded kernel). The numerical estimate is “billions of devices” (Heiser, seL4 whitepaper section 2.2).
• In definitely-not-esp32 v1.0, the microkernel runs in M-mode (no S-mode in the v1.0 SoC), uses Round-Robin Scheduling across at most four user tasks, Synchronous IPC as the only message-passing primitive, PMP-based address-space isolation, and routes UART input and timer ticks through the kernel to whichever task is registered as the handler. The total privileged-mode code budget is ~10 kSLOC of Rust; the project’s avowed influence is the L4 design ethic (“only what cannot be moved out”).

See Also

• Round-Robin Scheduling
• Synchronous IPC
• RISC-V Privilege Modes
• RISC-V Trap Handling
• Physical Memory Protection
• ecall Instruction
• Supervisor Binary Interface
• Wishbone Bus
• Core Local Interruptor
• Platform-Level Interrupt Controller
• Computer Architecture MOC

Footnotes

1. Liedtke hangs footnote 3 off this sentence, and it is worth reading because it pre-empts the obvious objection: “Proving minimality, necessarity and completeness would be nice but is impossible, since there is no agreed-upon metric and all is Turing-equivalent.” The principle is a design heuristic he is asking the reader to accept on argument, not a theorem. ↩