seL4 Level-1 Tutorials – seL4 Introduction
What is seL4?
seL4 is the first verifiable microkernel in the public domain. This means:
- In the public domain means that you can use it without paying a fee, provided you abide by the GPL license. seL4 facilitates adoption, since GPL applies to Kernel components only.
- Micro-kernel means that most functionalities of the operating systems have been removed from the kernel, reducing its attack and error-prone development.
- Finally, and most importantly, verifiable means that the kernel has been proven correct. In other words, the mechanisms provided by the kernel have been formally proven to execute just as they are described, and nothing else!
Microkernels
A microkernel is the near-minimum amount of software that can provide mechanisms needed for an operating system. This includes:
- Low level address space management
- Thread management
- Interprocess communication
- Interrupt management and routing
Generally the kernel is the most privileged--everything else contained in userspace.
seL4 Microkernel - Concepts and Principles
The kernel provides objects for threads, address spaces, interprocess communication, notifications, device primitives, and capability spaces. It also uses threads to group executing contexts together. Threads are contained by Thread Control Block tcb_t structures (as of kernel 8.0 and higher, those can be seen in kernel/include/object/structures.h).
The root thread is the thread seL4 branches to after it has initialized the kernel and structures for user space. It receives all of the capabilities and memory that the kernel knows about, and it is responsible for managing those resources in the userspace (e.g., creating threads and assigning them certain capabilities with certain privileges).
Processes are not seL4 constructs. But they are supported by the seL4 libraries. A process contains a thread and can inherit and pass capabilities with the root thread. Processes are generally loaded from binary images (e.g. ELF).
seL4 relies heavily on endpoints for interprocess communication (IPC). They allow small amounts of data and capabilities to be transferred between threads. Endpoint communication is extremely fast. The most common communication system calls are:
- seL4_Send
- seL4_Call
- seL4_Recv
- seL4_ReplyRecv
Endpoints, however, are not the only method for IPC since messages can be sent to other kernel objects. The seL4 IPC model consists of the thread having the capability to access the kernel object of interest and then loading the thread’s message register. IPC message registers have three descriptive registers that are backed by CPU registers and anywhere from 1-4 “Message Registers” that are backed by the thread’s IPC buffer (thread_t.tcbIPCBuffer).
seL4 Capabilities
Capabilities are stored in capability spaces (CSpace) which are kernel objects made up of capability nodes (CNode). Each CNode has an array of capability slots. A slot contains a capability pointer (CPtr/capPtr). The kernel objects are inaccessible to the userspace, but they can be controlled through capability pointers which are stored in the CSpace.
Capabilities have four specific privileges:
- Read
- Write
- Execute
- Grant
Capabilities can be transferred following the principle of least privilege. That is, the transferred capability can never have more privileges after the transfer, but it can have fewer. The main operations on capabilities are:
- Invoke: Perform action/operation on an object pointed to by the capability. Operations vary depending on the underlying object type.
- Copy/Mint/Grant: Create a copy of the capability with the same or lesser privileges.
- Move/Mutate: Transfer to a different address with the same or lesser privileges.
- Delete: Invalidate a capability pointer. If the underlying object is only referred to by this capability, it will also be cleaned up.
- Revoke: Delete any derived (copied or minted) capability. The capability we call revoke on will not be destroyed.
For more background on seL4 microkernel, refer to the seL4 Whitepaper and seL4 Reference Manual.