The seL4 microkernel is the world's first OS kernel that is formally verified to contain no bugs. After several years of development as a proprietary technology, the kernel was eventually released as open source in summer 2014. This prompted me to explore the use of seL4 as base platform for the Genode OS framework. The talk will introduce seL4, explain the interplay of Genode with the kernel, and present the current state of development.
The Genode OS framework is a tool kit for building component-based operating systems. It combines microkernel technology, capability-based security, and virtualization with a unique component architecture that allows it to scale from static embedded systems to highly dynamic general-purpose workloads.
Since its inception in 2008, Genode was designated as user land for the L4 family of microkernels. In that spirit, it supports most members of the family including L4ka::Pistachio, L4/Fiasco, OKL4, NOVA, and Fiasco.OC. Each of those kernels has different pros and cons. Genode enables software developers to target all of them at once, and allows system integrators to pick the kernel that fits best.
The seL4 kernel is the latest and supposedly greatest member of the L4 family. What sets it apart from all the others is the premise, under which it was designed and developed: The formal verification of the kernel's correctness while achieving high performance. Similarly to NOVA and Fiasco.OC, it employs capability-based security as the fundamental mechanism for guarding the access to kernel objects. But in contrast to the existing kernels, it also attacks the fundamental problem of managing kernel memory from the user land - a problem that used to be conveniently ignored by all prior L4 kernels.
After several years of development behind the closed doors of NICTA, seL4 was finally set free under the GPL license in 2014. From Genode's perspective, this sounded almost too good to be true: An open-source microkernel that is formally verified to be correct, well documented, backed by an enthusiastic community, and equipped with all the basic functionality required by Genode!
It goes without saying that - as a Genode developer - I was thrilled to bring both projects together. After conducting a series of experiments exercising the kernel interface, I started adapting Genode to seL4 as a personal side project. Even though the seL4 kernel and the Genode user land should intuitively fit perfectly together on paper, the devil lies in the details. In the talk, I'd like to share those details, the challenges that had to be overcome, and the solutions I came up with. It provides insights into both the seL4 kernel interface and Genode's underpinnings, and gives a glimpse of the future direction.
Speakers: Norman Feske