A microkernel is the minimal core of an operating system (OS). It presents a very small subset of what is generally considered an operating system today. The definition of what makes up a microkernel is given by Liedtke [SOSP’95]: A concept is tolerated inside the microkernel only if moving it outside the kernel, i.e., permitting competing implementations, would prevent the implementation of the system’s required functionality.

 

A microkernel therefore does not provide high-level abstractions over the hardware (files, processes, sockets etc) as most modern operating systems such as Linux or Windows do. Instead, it provides minimal mechanisms for controlling access to physical address space, interrupts, and processor time. Any higher-level constructs are built on top of the microkernel, using those mechanisms. Such higher-level services inevitably encapsulate policy. Policy-freedom is an important characteristic of a well-designed microkernel.

 

In the model used by L4 microkernels (and seL4 is no exception), an initial user-level task (the root task) is given full rights to all resources left over once the kernel has booted up (this typically includes physical memory, IO ports on x86, and interrupts). It is up to this root task to set up other tasks, and to grant rights to those other tasks in order to build a complete system. In seL4, like other third-generation microkernels, such access rights are conferred by capabilities (unforgeable tokens representing privileges) and are fully delegatable.

 

Presently seL4 runs on Arm v6, v7 (32-bit) and v8 (64-bit) cores, on PC99 (x86) cores (32- and 64-bit mode), and RISC-V RV64 (64-bit) cores. See the up-to-date list of supported platforms.

 

You can get sel4 here