seL4 Reference Manual

• The seL4 microkernel is an operating-system kernel designed to be a secure, safe, and reliable foundation for systems in a wide variety of application domains.
• As a microkernel, it provides a small number of services to applications, such as abstractions to create and manage virtual address spaces, threads, and inter-process communication (IPC).
• A limited number of service primitives are provided by the microkernel; more complex services may be implemented as applications on top of these primitives.
• Threads are an abstraction of CPU execution that supports running software.
• Address spaces are virtual memory spaces that each contain an application. Applications are limited to accessing memory in their address space.
• Inter-process communication (IPC) via endpoints allows threads to communicate using message passing.
• Notifications provide a non-blocking signalling mechanism similar to binary semaphores.
• Device primitives allows device drivers to be implemented as unprivileged applications. The kernel exports hardware device interrupts  via IPC messages.
• Capability spaces store capabilities (i.e. access rights) to kernel services along with their book-keeping information.
• The seL4 microkernel provides a capability-based access-control model. Access control governs all kernel services; in order to perform an operation, an application must invoke a capability in its possession that has sufficient access rights for the requested service.
• A capability is an unforgeable token that references a specific kernel object (such as a thread control block) and carries rights that control what methods may be invoked.
• Conceptually, a capability resides in an application's capability space; an address in this space refers to a slot which may or may not contain a capability.
• Capability spaces are implemented as a directed graph of kernel-managed capability nodes.
• Capabilities can also be revoked to withdraw authority. Revocation recursively removes any capabilities that have been derived from the original capability being revoked.
• The seL4 kernel provides a message-passing service for communication between threads. This mechanism is also used for communication with kernel-provided services.
• Logically, the kernel provides three system calls: send, receive, and yield. However, there are also combinations and variants of the basic send and receive calls.
• seL4_Send() delivers a message through the named capability and the application to continue.
• seL4_Recv() is used by a thread to receive messages through endpoints or notifications.
• seL4_Yield() is the only system call that does not require a capability to be used. It forfeits the remainder of the calling thread's time slice and causes invocation of the kernel's scheduler.
• CNodes store capabilities, giving a thread permission to invoke methods on particular objects.
• Thread Control Blocks represent a thread of execution in seL4.
• Endpoints facilitate message-passing communication between threads.
• IPC is synchronous: A thread trying to send or receive on an endpoint blocks until the message can be delivered.
• Notification Objects provide a simple signalling mechanism. A notification is a word-sized array of flags, each of which behaves like a binary semaphore.
• Virtual Address Space Objects are used to construct a virtual address space for one or more threads.
• Interrupt Objects give applications the ability to receive and acknowledge interrupts from hardware devices.
• Untyped Memory is the foundation of memory allocation in the seL4 kernel.
• The seL4  microkernel does not dynamically allocate memory for kernel objects. Instead, objects must be explicitly created from application-controlled memory regions via Untyped Memory capabilities.
• There are no arbitrary resource limits in the kernel apart from those dictated by the hardware, and so many denial-of-service attacks via resource exhaustion are avoided.
• At boot time, seL4 pre-allocates the memory required for the kernel itself, including the code, data, and stack sections (seL4 is a single kernel-stack operating system). It then creates an initial user thread (with an appropriate address and capability space). The kernel then hands all remaining memory to the initial thread in the form of capabilities to Untyped Memory, and some additional capabilities to kernel objects that were required to bootstrap the initial thread.
• Each user-space thread has an associated capability space (CSpace) that contains the capabilities that the thread possesses, thereby governing which resources the thread can access.
• A CNode is a table of slots, each of which may contain a capability. This may include capabilities to further CNodes, forming a directed graph.
• seL4 requires the programmer to manage all in-kernel data structures, including CSpaces, from user-space. This means that the user-space programmer is responsible for constructing CSpaces as well as addressing capabilities within them.
• Capabilities are managed largely through invoking CNode methods.
• Some capability types have access rights associated with them. The access rights associated with a capability determine the methods that can be invoked.
• seL4 supports three orthogonal access rights, which are Read, Write, and Grant.
• Like a virtual memory address, a capability address is simply an integer. Rather than referring to a location of physical memory (as does a virtual memory address), a capability address refers to a capability slot.
• The seL4 microkernel provides a message-passing IPC mechanism for communication between threads. The same mechanism is also used for communication with kernel provided services.
• Messages are sent by invoking a capability to a kernel object.
• Endpoint capabilities may be minted to create a new endpoint capability with a badge attached to it, a data word chosen by the invoker of the mint operation.
• Notifications are a simple, non-blocking signalling mechanism that logically represents a set of binary semaphores.
• A Notification object contains a single data word, called the notification word.
• seL4 provides threads to represent an execution context and manage processor time. A thread is represented in seL4 by its thread control block object (TCB). Each TCB has an associated CSpace and VSpace which may be shared with other threads.
• In multi-core machines, threads run on the same CPU which originally created the TCB.
• seL4 uses a preemptive round-robin scheduler with 256 priority levels. All threads have a maximum controlled priority (MCP) and a priority, the latter being the effective priority of the thread.
• Each thread has an associated exception-handler endpoint. If the thread causes an exception, the kernel creates an IPC message with the relevant details and sends this to the endpoint. This thread can then take appropriate action.
• A thread's actions may result in a fault. Faults are delivered to the thread's exception handler so that it can take the appropriate action. The fault type is specified in the message label.
• User exceptions are used to deliver architecture-defined exceptions.
• Debug exceptions are used to deliver trace and debug related events to threads.
• Domains are used to isolate independent subsystems, so as to limit information flow between them. The kernel switches between domains according to a fixed, time-triggered schedule.
• A thread belongs to exactly one domain, and will only run when that domain is active.
• A virtual address space in seL4 is called a VSpace.
• Common to every architecture is the Page, representing a frame of physical memory.
• A Page object corresponds to a frame of physical memory that is used to implement virtual memory pages in a virtual address space.
• Page faults are reported to the exception handler of the executed thread.
• Interrupts are delivered as notifications. A thread may configure the kernel to signal a particular Notification object each time a certain interrupt triggers.
• IRQHandler capabilities represent the ability of a thread to configure a certain interrupt.
• Access to I/O ports is controlled by IO Port capabilities. Each IO Port capability identifies a range of ports that can be accessed with it.
• I/O devices capable of DMA present a security risk because the CPU's MMU is bypassed when the device accesses memory.
• The seL4 kernel creates a minimal boot environment for the initial thread. This environment consists of the initial thread's TCB, CSpace and VSpace, consisting of frames that contain the user-land image and the IPC buffer.