Microkernel vs. Monolithic Kernel design

In order to understand the need for a secure microkernel as it is provided by the seL4, it makes sense to start with a closer look at kernel design principles in general. Figure 1 therefore depicts the two main kernel design approaches – the monolithic kernel and the microkernel. As can be easily seen, within the former approach, all code required for providing typical OS services (e.g. file storage or networking facilities) is directly implemented in the kernel itself. As the kernel executes in the privileged mode of the hardware (also called kernel or supervisor mode), all code is granted unrestricted access and control of all system resources. Besides being beneficial to the overall system performance, this nevertheless can lead to dangerous situations in case kernel components feature some type of malfunction, which can be exploited by an attacker. The Linux kernel is a prominent example for a monolithic design. Considering its more than 20 million lines of code, a certain number of bugs providing such an attack channel can be expected to exist.

The microkernel design copes with this drawback by drastically reducing the so-called trusted computing base (TCB). It defines the subset of the overall system that must be trusted to operate correctly. Only then the system can be to expect to be secure. Therefore, a microkernel follows the design principle that the kernel itself shall contain only the most fundamental mechanisms (e.g. IPC, scheduling). All further OS functionality is transferred to the unprivileged user mode, running within isolated sandboxes that protect the kernel processes from any interference from the outside except communication that is explicitly allowed. A well-designed microkernel like seL4 can therefore be reduced to the order of ten thousand lines of code, which means drastically shrinking the attack surface. Nevertheless, typical microkernel designs tended to lack performance due to the significant communication overhead induced by additional kernel entries/exits and context switches. However, this general performance problem was solved back in the mid-’90s by Jochen Liedtke, who accelerated the underlying IPC concept and therefore invented the design of the first L4 microkernel (see figure 2).