Microkernel

A microkernel is an operating system architecture that pushes the maximum possible functionality out of the kernel and into user-space services, leaving the kernel itself responsible only for the most primitive operations: address space management, thread management, and inter-process communication. The thesis is radical: if device drivers, filesystems, and network stacks run as ordinary processes, then a bug in any of them crashes a service, not the entire system.

This elegance has proven difficult to realize in practice. The performance cost of crossing the user-kernel boundary for every filesystem operation, every network packet, every device interaction is substantial, and the history of microkernels — from Mach to L4 to seL4 — is a history of increasingly sophisticated optimizations to reduce that cost. The seL4 project represents the current frontier: a formally verified microkernel whose correctness has been mathematically proven, suggesting that the tradeoff between safety and performance may not be fundamental but merely expensive.