Linked by Norman Feske on Wed 31st Aug 2016 22:35 UTC
OSNews, Generic OSes

With the just released version 16.08, Genode makes the entirety of the framework's drivers, protocol stacks, and libraries available on the seL4 kernel. Thereby, the vision of a real general-purpose OS built upon a formally verified kernel suddenly becomes a tangible mission. Further highlights of the new version are the use of the framework to run VirtualBox 4 on the Muen separation kernel, an experimental version of VirtualBox 5 on top of the NOVA kernel, the added support for virtual networking and TOR, profound Zynq board support, and new tools for statistical profiling.

The seL4 kernel is universally regarded as the world's most advanced open-source microkernel - not by technical merits alone but by the fact that the kernel is accompanied by formal proofs of its correctness. However, to achieve this high level of assurance, the kernel's responsibilities had to be reduced to an extreme that goes even beyond traditional microkernels. In particular, the kernel leaves the problem of managing kernel memory to be solved at the user level. The problem still exists but it isn't considered the kernel's problem anymore. Consequently, this kernel design makes the creation of a scalable user land extremely challenging. For this reason, most use cases of seL4 remain solely static in nature, or combine static components with virtualization. The real potential of seL4 to scale towards dynamic systems remained untapped so far. Here is where Genode comes into play. Genode is designed as a dynamic user land for microkernels, which addresses the management of memory at the user-level via a unique resource-trading concept. It turns out that this concept is a suitable answer to the kernel-management problem posed by seL4. By completing the implementation of the framework's base mechanisms for this kernel, literally hundreds of existing Genode components become readily available to the seL4 community.

The Muen separation kernel is another take on the use of formal methods for assuring the absence of bugs in an OS kernel. In contrast to seL4, Muen applies different technologies (Ada/SPARK) and addresses static partitioned systems. A natural use case is the co-hosting of virtual machines. In a multi-level scenario, each virtual machine hosts a guest OS for editing documents at one security level. The separation kernel enforces the information-flow policy between the virtual machines. In such scenarios, the predominant guest OS is MS Windows. Consequently, Muen had to support the virtualization of such commodity OSes. Genode already solved this problem for another microkernel by making VirtualBox available on top of NOVA. So the idea was born to leverage Genode's version of VirtualBox on top of Muen - essentially using Genode as a runtime environment for VirtualBox. As crazy as it sounds - it works! The release documentation has a dedicated section that tells the full story. Speaking of VirtualBox, the ability to run VirtualBox directly on a microkernel is certainly a key feature of Genode. With Genode 16.08, a first version of VirtualBox 5 becomes available on the NOVA kernel.

The anecdotes above highlight the benefits of Genode's cross-kernel portability. The new version pushes this idea even further by attaining binary compatibility across all the supported kernels for a given CPU architecture. In fact, compiled once, an ELF binary of a regular component can be natively executed on kernels as different as seL4 and Linux as long as the component does not rely on a special feature of a particular kernel.

At a higher level, the current release extends the framework's library of ready-to-use building blocks in several areas. Most prominently, there are new network-related components for routing traffic, using TOR, and for distributing Genode over the network. Other added components are concerned with improving the use of Genode as a general-purpose OS, or to aid the optimization of components by the means of statistical profiling. Version 16.08 is further complemented with added board support for devices based on Xilinx Zynq, including drivers for GPIO, video DMA, SD cards, and I2C.

These and many more topics are covered in detail by the release documentation of version 16.08.

Permalink for comment 633811
To read all comments associated with this story, please click here.
RE[5]: Comment by ddc_
by nfeske on Fri 2nd Sep 2016 10:43 UTC in reply to "RE[4]: Comment by ddc_"
Member since:

Intuitively it sounds odd but it is actually perfectly reasonable. Let me try to explain:

Each kernel needs some memory for internal data structures, e.g., for remembering the states of threads and address spaces, or for the page tables supplied to the MMU. Where does this memory come from?

The traditional answer is that the kernel maintains a private memory pool to allocate such objects from. Usually, a fixed portion the available physical memory is reserved for the internal memory pool at boot time. All remaining memory is handed over to the user land. This raises two questions:

1. What happens in the catastrophic event that the kernel memory exhausts? Most microkernels will simply panic! In contrast to a monolithic kernel that can somehow intelligently respond to memory pressure by swapping memory to disk, flushing the block cache, or sacrificing a process, a microkernel has no reasonable way to respond to such a condition. It has no notion of a block cache, no disk driver, and doesn't have any interpretation of the role of processes on top. For this reason, most microkernels (such as traditional L4) just stop the machine.

2. Who can trigger the consumption of kernel memory? The frightening answer is: any user-mode program running on top of the kernel! For example, on traditional L4 kernels, any normal program can install new memory mappings from its own memory into its virtual address space. Inside the kernel, this operation may trigger the allocation of a new page table, and the need to store metadata about the mapping. In L4, this meta data is called "mapping database". For each memory mapping, its keeps a record how the memory mapping was established in order to revoke mappings if their origin disappears.

Isn't this scary? Unfortunately, there is no easy solution for this problem. Hence, the academic research community swapped it under the carpet for more than a decade. Even NOVA as a very recent member of the L4 family left this problem un-addressed. Other kernels provided band-aid solutions in the form of kernel-resource quotas, which work reasonably well in practice but don't scale. The seL4 kernel is the first kernel that at least allows the userland to fix the problem instead of letting it suffer from the kernel's limitation. Sure, it does not magically solve the problem but it enables Genode to solve it.

Therefore, even though seL4's concept to manage kernel memory in user space is inconvenient compared to the more abstract interfaces of prior kernels, I regard it as its killer feature compared to all other kernels I have encountered in the past.

Is the seL4 way the only way? Certainly not. E.g., Genode's custom base-hw kernel successfully addresses the problem in a very different way. But in contrast to seL4, which is agnostic with respect to the user land on top, base-hw's design it inherently tied to Genode.

Reply Parent Score: 1