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.

Thread beginning with comment 633828
To view parent comment, click here.
To read all comments associated with this story, please click here.
RE[7]: Comment by ddc_
by nfeske on Fri 2nd Sep 2016 15:10 UTC in reply to "RE[6]: Comment by ddc_"
Member since:

Thanks to the link to your previous discussion!

I question this. I see no reason the kernel and userspace can't simply share the same memory pool. To the best of my knowledge, this is what operating systems generally do at the page level (with possible quotas, dma reservations, and whatnot).

Sorry, I should have been more clear that I referred specifically to L4 kernels. You are right that other microkernels indeed provide memory objects at the kernel interface and thereby can use a single memory pool. The out-of-kernel memory problem exists regardless, doesn't it?

Here's the bit I'm stuck with, to me it doesn't seem like the problem is solved, it's just moved into a new scope. I'm I right about this or am I missing something?

seL4 pushes the problem from the kernel to the user land. Here, it is actually solved by Genode!

How does it perform?

I am unable to answer this question because it is overy generic. It ultimately depends on the workload.

There are plenty opportunities for performance improvements in several areas, in the scopes of both the kernel and Genode. It is too early to draw any conclusions at this point. Anyway, you can give it a spin right now. ;-)

Reply Parent Score: 1

RE[8]: Comment by ddc_
by Alfman on Fri 2nd Sep 2016 16:48 in reply to "RE[7]: Comment by ddc_"
Alfman Member since:


You are right that other microkernels indeed provide memory objects at the kernel interface and thereby can use a single memory pool. The out-of-kernel memory problem exists regardless, doesn't it?

Yes absolutely. In principal a kernel could bubble out an exception for every operation that could potentially lack memory and in theory such a kernel could be formally verified. The problem is that this is easier said then done, at least until we have transactional operating systems. I kind of have trouble sticking on topic ;)

seL4 pushes the problem from the kernel to the user land. Here, it is actually solved by Genode!

That's what I thought, but it isn't clear to me that the net complexity or failure modes have improved at all relative to handling it in the kernel. Ultimately though I think it's great that you are trying something different. It's good to question everything. We get so enamored with the mainstream approaches that the field becomes stale.

Reply Parent Score: 2