seL4 (security enhanced L4) is an open-source, high-assurance, capability-based microkernel. It inherits the performance and design characteristics of the L4 microkernel lineage but is implemented using high-assurance methods. seL4 uses formal mathematical verification to prove the system's confidentiality, integrity, availability among other properties. The initial paper outlining seL4's verification was inducted into the 2019 ACM SIGOPS Hall of Fame.
History seL4 was developed as a from-scratch microkernel design influenced by the L4 microkernel family, with an explicit goal of enabling comprehensive formal verification while maintaining high performance. In 2009, the seL4 project reported a machine-checked proof of functional correctness spanning from formal specification to C implementation. In July 2014, the seL4 kernel sources and verification artifacts were released as open source by NICTA with industry partners. On 7 April 2020, the seL4 Foundation was launched to support governance, ecosystem development and long-term stewardship; it was initially hosted as a project of the Linux Foundation.
Architecture 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 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. Virtual memory management is also capability-governed. A capability to a memory frame confers the authority to map that frame into an address space, subject to the access rights encoded in the capability. Address spaces themselves are constructed from page table objects that are likewise created from untyped memory and referenced via capabilities. In addition to general-purpose memory, seL4 distinguishes device untyped memory, which is subject to additional restrictions to prevent unsafe retyping or reuse.
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. Messages may include both data and selected capabilities, allowing IPC to serve not only as a communication mechanism but also as a means of explicitly delegating authority. Transferring a capability during IPC directly transfers the right to access a kernel object, tightly integrating communication and access control.
… excerpt ends here. Continue reading the full article.
