seL4 is
extremely minimal, even compared to prior L4 kernels: it only handles memory management/process isolation and process scheduling - everything else is handled outside of kernel mode. At boot time, the seL4 kernel statically allocates enough memory for itself and then hands over all remaining memory and capabilities to an initial user space process. seL4 is more akin to a CPU driver than other commercial microkernels like
Mach,
QNX, or
Minix. The primary motivation was to enable policy and architectural freedom for system builders, but it also helps make verification easier and minimizes cache misses.
Capability-based access control seL4 uses a
capability-based model to control all access to memory and kernel resources. This enables resources and information flow to be reasoned about and managed in a programmatic manner (as opposed to a one-size-fits all security and architecture policies). In this model, a
capability is an unforgeable token that both names a kernel object and encodes the operations that may be performed on it. Capabilities are stored in kernel-managed tables called
capability nodes (CNodes), which form a hierarchical namespace analogous to a file-system directory structure. A CNode contains capability slots and is itself a kernel object accessed only through a capability, allowing authority over resources to be explicitly delegated, subdivided, or revoked. Physical memory in seL4 is initially represented as
untyped memory capabilities, which grant authority over raw regions of RAM but do not correspond to usable objects. Untyped memory is converted into typed kernel objects via a
retype operation. The kernel records the relationships between untyped memory and derived objects in a
capability derivation tree (CDT), which allows the system to enforce safe memory reuse: all capabilities derived from an untyped region must be removed before that region can be reallocated. This mechanism replaces implicit kernel allocators with an explicit, auditable memory lifecycle under application control.
Inter-Process Communication (IPC) seL4 IPC is
not intended as a general-purpose message-passing mechanism, but as a way to implement cross-domain invocation of functions or services across protection boundaries. seL4's designers frame it as a
Protected Procedure Call (PPC), which carries only small argument and return values (similar to a function call across protection domains) rather than a buffering transport for arbitrary data. seL4's designers explicitly recommend against using IPC for shipping bulk data or for synchronization, instead using IPC primarily for
request–reply invocation of services and
capability transfer. Inter-process communication in seL4 is based on capability-governed kernel objects and is designed to minimize kernel state while making authority explicit. The primary IPC object is the
endpoint, which represents both the right to communicate and the rendezvous point for communication: a thread may send to or receive from an endpoint only if it holds an appropriate capability. IPC via endpoints is synchronous and blocking (with other conventions layered on top). A send operation waits until a receiver is ready, and a receive operation waits until a sender arrives. Unlike many traditional message-passing systems, seL4 endpoints do not provide kernel-managed message queues or mailboxes. The kernel maintains only queues of waiting threads, and message data is transferred directly between the communicating threads using a small, fixed-size payload. This avoids implicit kernel memory allocation during communication and is consistent with seL4's explicit resource-management model. Shared memory regions are explicitly created from untyped memory and mapped into multiple address spaces, and notifications are used to signal availability of data or completion of work. This pattern enables the implementation of lock-free or wait-free data structures such as ring buffers without involving the kernel in the data path. By keeping the kernel out of bulk data transfer, seL4 systems reduce copying overhead, avoid unnecessary blocking, and preserve the simplicity required for formal verification. This design approach is promoted by higher-level frameworks in the seL4 ecosystem, including CAmkES, the seL4 Device Driver Framework (sDDF), and the seL4 Microkit.
Comparison with other IPC models •
POSIX message queues: POSIX message queues expose named, kernel-resident queues that support asynchronous message passing. They rely on implicit kernel memory allocation and a global namespace, and separate message passing from access-control mechanisms. By contrast, seL4 has no global IPC namespace and no kernel-managed message queues; all communication requires possession of an explicit endpoint capability, and buffering policies are implemented in user space if required. •
Mach ports: Mach ports combine naming and authority for IPC and are typically associated with kernel-managed message queues and asynchronous buffered communication. In contrast, seL4 endpoints avoid kernel message buffering and instead provide synchronous rendezvous semantics, reducing kernel complexity and hidden resource usage compared with Mach's more flexible but slower IPC mechanisms. •
L4 IPC: seL4's IPC model is directly descended from earlier L4 microkernels, which also emphasized synchronous, high-performance message passing. seL4 retains rendezvous-style IPC semantics, however, it decouples message passing from synchronization. This enables optimizing the former for PPC (server invocations) and integrates them more tightly with a formal capability system and a verified kernel design, making authority transfer explicit and amenable to formal reasoning.
Notifications and event signalling In addition to endpoints, seL4 provides
notification objects:
semaphore like objects for asynchronous event signalling and lightweight synchronization. Notifications are commonly used to deliver hardware interrupt events to user-space device drivers or to signal state changes between components, supporting a microkernel architecture in which interrupt handling and drivers execute outside the kernel. == Formal Verification ==