Genode 16.08 brings interactive and dynamic workloads to seL4

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.