The seL4 microkernel: Optimized for security and endorsed by the Linux foundation

The seL4 microkernel: Optimized for security and endorsed by the Linux foundation


Linux code

Image: iStockphoto/Spectral-Design

The Linux Foundation is a fundamental organization for the promotion of open source software and has officially endorsed the seL4 microkernel. To further boost seL4, the Linux Foundation will host seL4 Foundation, which is a non-profit organization, established by Data61.

We need to unpack this a bit.

SEE: How smart tech is transforming the transportation industry (TechRepublic Premium)

What is a microkernel?

In order to understand seL4, we must first know what a microkernel is. A microkernel is the bare minimum of components needed to form an operating system. Usually, microkernels are comprised of:

The advantages of the microkernel are:

  • Small and isolated, for improved functionality

  • The minimal amount of components offer a heightened level of security

  • Easily expanded without disturbing the Kernel

  • Modules can be replaced, reloaded, and modified without even touching the Kernel

  • Fewer system crashes

  • Interface helps admins enforce a more modular system structure

  • Features can be added without recompiling

  • Malfunctions are isolated

  • Highly flexible

  • Less code required to run in kernel space

What is seL4?

Now that we have a superficial understanding of what a microkernel is, just what is seL4? The seL4 is an open source L4 microkernel. The L4 microkernel was created by German computer scientist Jochen Liedtke in response to the poor performance of previous microkernel-based operating systems. The L4 microkernel has undergone a number of revisions such as L4, L4Ka::Hazelnut, L4/Fiasco, and L4Ka::Pistachio.

The seL4 microkernel came into being in 2009 and was a scientific breakthrough from the Trustworthy Systems group (TS), who develop trustworthy software systems which come with provable security, safety, and reliability guarantees. The seL4 microkernel provides an unmatched isolation between running applications in the system, which means a compromise in one application can be isolated from all other applications as well as critical system components. In the end, that equates to seriously heightened system security. In fact, seL4 is the only proven operating system which features fine-grained capability-based security as well as high performance. 

The first time seL4 proved itself worthy of real-world deployment was in the form of the DARPA-funded HACMS program, where seL4 was used to protect an autonomous helicopter against cyber attacks.

You can check out the seL4 code from the official Github page.

Linux Foundation formal endorsement

The new seL4 Foundation’s goal is to accelerate the commercial development of seL4 and it’s related technologies. With the help of the Linux Foundation, it will enjoy global, independent, and neutral organization for funding as well as its future evolution. 

The founding members of the seL4 Foundation include:

  • Data61

  • UNSW Sydney

  • HENSOLDT Cyber GmbH

  • Ghost Locomotion, Inc.

  • Cog Systems, Inc.

  • DornerWorks, Ltd.

According to Michael Dolan, VP of strategic programs for the Linux Foundation, “The Linux Foundation will support the seL4 Foundation and community by providing expertise and services to increase community engagement, contributors and adopters, helping to take the OS ecosystem to the next level.” Dolan adds, “The open governance and standards-based model will provide a neutral, mature, and trustworthy framework to help advance an operating system that is readily deployable and optimized for security.”

Implications of seL4

There are numerous ways seL4 will impact the current tech landscape. One is within connected devices (think edge computing). Carl L. Nerup, CEO of Cog Systems, Inc. says, “seL4 has set the new standard for high assurance for embedded solutions on connected devices.” More specifically, Nerup adds, “This enables us to deliver commercial solutions that meet the rigorous demands associated with formal verification to deliver a certified approach that meet the highest standard for safety and security in the market today.”

In other words, seL4 could deliver far more secure IoT and edge computing platforms. Considering such systems are expected to see an exponential increase in deployment, a dependence on a verified secure operating system is key to preventing data theft and downtime. 

Another area where seL4 might excel is autonomous vehicles. Consider Ghost, a self-driving system which integrates into automobiles. Dr. Daniel Potts of Ghost Locomotion, Inc., says of seL4, “Ghost is a self-driving system that integrates seamlessly into your current car. Designed to be safer than a human driver, Ghost will give you the power to fully disengage on the highway and focus on what matters to you. Nowhere is the pursuit of perfection more important than our highways and we are proud to join the seL4 community to make provably-correct, safety-critical systems a reality for millions of daily commuters.”

Yet another area is cybersecurity. Gregg Wildes, innovation leader and partnership manager of DornerWorks, Ltd., said, “The seL4 proof provides a secure foundation to answer the growing need for cyber-security. By joining the seL4 Foundation, DornerWorks can do more to help accelerate customer adoption of seL4 as the trusted software base for their embedded products.”

Even the coronavirus pandemic was mentioned, when former Director of DARPA I2O John Launchbury said, “In system security, seL4 is one-of-a-kind. COVID-19 has taught us all the value of ‘distancing’ in keeping any kind of system healthy and secure. That’s what microkernels like seL4 do for software. What makes seL4 unique is that we know with mathematical certainty that the seL4 code implements its ‘distancing’ specification with zero functionality bugs. That it does so without a performance hit is doubly astonishing. I am eagerly anticipating seeing more and more system builders incorporate it to increase their digital security, and I’m confident that the seL4 foundation has been well structured to be effective in curating the ongoing open source development of seL4.”

Needless to say, we’re only just now scratching the surface of seL4. The possibility this microkernel has to offer will absolutely reset the bar on security for connected systems.

Also see

Source of Article