seL4® – Why a microkernel system?

Sebastian Eckl, Senior Software Engineer at HENSOLDT Cyber

This blog post marks the start of a series of articles which will explain the idea of TRENTOS®, a novel secure embedded operating system (OS) on top of the proven seL4® ecosystem. For a better understanding of the design decisions behind this OS idea, the principles and the exceptionalism of the underlying seL4 microkernel shall be discussed within this first blog post.

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). 

 

Figure 1: Monolithic vs. Microkernel Kernel design (Source: https://github.com/seL4/whitepaper/blob/master/imgs/kernel.pdf)

The seL4 microkernel – what makes it unique?

Released in 2009, made available as open source software in 2014 and maintained by the seL4 Foundation since 2020, the seL4 microkernel joins the family of L4 microkernels. However, the kernel implemented the L4 design completely from scratch, getting rid of any inheritance (e.g. API and code), benefiting from all the positive and negative experiences of almost 20 years of L4 based kernel design. Apart from this, seL4’s outstanding feature can be found in its inherent and unique focus on the development of highly secure systems without compromising performance. It introduced two main security design concepts: the utilization of capabilities and the application of formal verification techniques. Capabilities hereby represent a form of access token that allows for a very fine-grained control over system resources and therefore supports the kernel’s isolation properties. In addition, due to being formally verified, the absence of bugs inside the kernel implementation is proven with respect to its specification. This leaves seL4 as the world’s most advanced and most highly assured OS kernel.

Figure 2: L4 microkernel history (Source: https://github.com/seL4/whitepaper/blob/master/imgs/l4family.pdf)

seL4 and TRENTOS – laying the foundation for a secure OS

With TRENTOS, HENSOLDT Cyber takes the next logical step – developing a novel secure embedded OS on top of the proven seL4 ecosystem. It alleviates the entry to the quite complex area of developing secure embedded systems by abstraction. Hereby, developers can fully focus on creating secure applications without having to worry about lower-level details and the underlying architecture.

So, stay tuned for the upcoming blog posts, which will provide more insights on the TRENTOS architecture, its utilization of the CAmkES component framework as well as the content of the TRENTOS SDK. If you are interested in more details regarding the seL4 microkernel, have a look at the seL4 Whitepaper (https://sel4.systems/About/seL4-whitepaper.pdf). For now, let’s conclude with a statement of Dr. Gernot Heiser, inventor of the seL4 and Professor at the John Lions Chair of Operating Systems at the University of New South Wales (UNSW), who is supporting HENSOLDT Cyber as a Chief Scientist:

 “TRENTOS leverages seL4’s mathematically proved security enforcement while presenting a higher-level interface that is easier to understand and use than seL4’s low-level mechanisms. TRENTOS provides the basic functionality required by security-critical systems with a minimal trusted computing base, protected by seL4.”

READ MORE

Be the first to hear about our products and innovations!

Share on facebook
Share on linkedin
Share on email

Leave a Reply

Your email address will not be published. Required fields are marked *