In a microkernel-based system, device drivers operate as regular processes in user mode, each within its own address space. This separation is enforced using hardware mechanisms such as the memory-management unit (MMU) and the IOMMU, which handle devices performing direct memory access (DMA) via memory-mapped input/output (MMIO).
Processes that provide services are commonly referred to as servers, adhering to the client-server communication model. Services are functions that clients can access through inter-process communication (IPC), which can be either blocking or nonblocking. This IPC mechanism is similar to a remote procedure call (RPC) in network environments but functions within the system’s protection domains.
A protection domain in a microkernel-based system is akin to a “process” in traditional UNIX systems and runs code represented by the kernel object “thread”. The service invoked within a protection domain is known as a capability, providing IPC endpoints.
Kernel objects in a microkernel-based system include:
- Threads
- Address spaces
- IPC endpoints
- Capability spaces (lists of capabilities)
- Frames (block on physical memory, usually in size of a page)
- Interrupt objects
- Untyped memory
Kernel objects communicate via IPCs, which are typically termed system calls. In seL4, there are three defined system calls (IPCs): Send, Wait, and Yield.
Access control is fundamental to all kernel services; an application must use a capability it holds to perform an operation, ensuring it has the necessary access rights. Capabilities can be copied, moved within capability spaces, and transmitted through IPC. This mechanism enables the creation of applications with specific access rights, delegation of authority to other applications, and the transfer of authority for new or specific kernel services.
Devices are invoked through memory kernel objects that are linked via bidirectional queues where the server sends data to the driver and the driver data to the server. For SeL4 the sDDF framework abstracts the driver development in this AsyncIO/ VirtIO manner.
In a common operating system setup on the kernel serves various servers. To describe this assembly of components SeL4 offers a framework called “CAMKES”. For different scheduling strategies between the components (aka server) support can be found here. CAMKES is also used to implement “virtual machine” (VM) via the “libsel4vm”.
Further notes:
- Musllibc provides the POSIX interfaces which will be linked by each server to abstract the kernel specifics.
- Microkit offers an SDK to develop OS on top of SeL4.
- A couple of open SeL4 based OS do exist e.g.