seL4

seL4

Developer(s)	seL4 community; seL4 Foundation
Written in	C (kernel); Isabelle/HOL (proofs)
Engine
Type	Microkernel; capability-based operating system kernel
License	GPL-2.0-only (kernel); mixed licensing in ecosystem
Website	sel4.systems

Search SeL4 on Amazon.

seL4 is an open-source, high-assurance, capability-based microkernel. It inherits the high-performance and design of the L3/L4 microkernel lineage but is implemented using high-assurance methods. seL4 comes with formal mathematical verification to prove the system's confidentiality, integrity, availability (among other properties). The separation between privilege contexts is better than that of VMs in other operating systems. seL4 won the 2019 ACM SIGOPS Hall of Fame Award.

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 (Australia) with industry partners; technology press coverage treated the release as notable within the secure/embedded systems community.

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.

Design

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. seL4 is more akin to a CPU driver than other commercial microkernels like Mach, QNX, or Minix. This is necessary to keep verification tractable and enables the kernel to remain in a CPU's L1 cache .

Capability-based access control

seL4 uses a capability-based model to control all access to memory and kernel resources. 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. System builders explicitly convert untyped memory into typed kernel objects—such as memory frames, page tables, CNodes, or thread control blocks—using 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 represents memory-mapped I/O regions and is subject to additional restrictions to prevent unsafe retyping or reuse.

Inter-process communication (IPC)

seL4 IPC is designed not 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 synchronisation, 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 minimise 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.

Control-plane and data-plane separation

While synchronous IPC is the fundamental communication primitive provided by the kernel, they are intentionally designed to avoid (ab)use as a way to transmit data and its use within seL4 based systems is minimised on performance-critical paths. Systems commonly separate communication into a control plane and a data plane. IPC is used primarily for control operations such as configuration, request–reply interactions, and capability transfer, while bulk or high-frequency data exchange is implemented in user space using shared memory combined with asynchronous notifications.

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

• L4 IPC: seL4’s IPC model is directly descended from earlier L4 microkernels, which also emphasised synchronous, high-performance message passing. seL4 retains rendezvous-style IPC semantics but integrates them more tightly with a formal capability system and a verified kernel design, making authority transfer explicit and amenable to formal reasoning.

• 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.

• 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.

Notifications and event signalling

In addition to endpoints, seL4 provides notification objects for asynchronous event signalling and lightweight synchronisation. 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.

Conceptual IPC structure

A typical seL4 IPC interaction can be represented as follows:

Control plane (IPC):
Client thread            Kernel             Server thread
--------------          --------           --------------
  call(endpoint)  -->   rendezvous    <--   receive(endpoint)
     (blocks)                                   |
         |----------- small message + caps ---->|
         |<-------------- reply ---------------|

Data plane (shared memory + notifications):
Producer writes to shared buffer
Producer signals notification
Consumer reads from shared buffer

This separation of control-plane IPC from data-plane shared memory is a defining characteristic of seL4-based system designs, distinguishing them from traditional message-passing systems that rely on kernel-managed queues for both control and data transfer.

Formal verification

Overview of CIA properties.

Functional correctness

The primary verification result reported for seL4 is functional correctness of the kernel’s C implementation with respect to a formal specification, mechanised in Isabelle/HOL. The ACM SIGOPS Hall of Fame citation highlighted seL4 as the first project to provide a machine-checked proof of correctness and security properties of a high-performance microkernel, and noted its impact on subsequent work in provably correct systems.

Extending verification to additional configurations

Summit presentations have reported ongoing work to broaden verification coverage across additional architectures and configurations, and to address multicore-related challenges. For example, the seL4 Summit 2024 programme included a roadmap talk on a verified “static multikernel” approach for multicore, together with a “status and plans” update on the verification effort.

Worst Case Execution Time Analysis (WCET/RTOS)

Better than "real time".

Absence of side channels

RISC-V extensions.

Binary Proofs

Proofs have been extended to the binary.

Ongoing Verification

Various architectures, configurations, multicore support, and various other features that have been implemented do not yet have formal proofs of correctness. Most are considered stable and verification is not expected to cause breaking API changes but bugs have been found in the unverified implementations. No such bugs have been found in the verified portions of the kernel over the past 15 years.

Ecosystem

seL4 is commonly used as the kernel foundation for componentised embedded systems, and the Foundation supports a set of associated tools and frameworks. The annual seL4 Summit is a primary venue for presenting ecosystem development, research directions, and experience reports.

Microkit

The seL4 Microkit is an operating-system framework built on top of seL4 that provides a small set of abstractions aimed at lowering the barrier to building statically structured systems while preserving performance and memory efficiency goals. It is distributed as an SDK and documented by the seL4 project. Microkit has also been presented at seL4 Summit as part of the ecosystem’s engineering direction.

Device Driver Framework (sDDF)

The seL4 Device Driver Framework (sDDF) is a driver architecture for seL4-based systems discussed in multiple summits; summit materials describe a design emphasising separation of concerns and event-based/asynchronous communication with shared-memory data paths.

Rust-based OS services (Magnetite)

The summit programme has also included work on Rust-based operating system services for seL4, including the Magnetite project presented at seL4 Summit 2023.

Governance and community

The seL4 Foundation coordinates aspects of project governance and promotes a vendor-neutral ecosystem. Its launch (April 2020) was announced by the Linux Foundation and CSIRO’s Data61, and was framed as an effort to support broader adoption and long-term stewardship of seL4 technology.

The seL4 Summit is an annual conference focused on seL4 and related tools, infrastructure, and projects. Recent summits have included both research work (for example, multicore verification roadmaps) and industry-oriented sessions, such as a 2025 panel on building a business case for verified kernels featuring multiple companies using or evaluating seL4-based approaches.

See also

• L4 microkernel family
• Microkernel
• Capability-based security
• Formal verification

External links

• Official website
• Documentation
• seL4 Summit

This article "SeL4" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:SeL4. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.

📰 Article(s) of the same category(ies)

• Civil Service Commission (Isle of Man)
• Agnes, Georgia
• Abdulrahman al-A'ama
• Sandhya Shantaram
• Kamila Krzyzaniak
• Wagner Lake
• Evan Z. Macosko

---