Interactive and dynamic workloads on top of the seL4 kernel Sep 20, 2016

SeL4 promises to be a firm foundation for trustworthy systems because it is widely regarded as the world's most advanced open-source microkernel. The kernel applies the lessons learned in twenty years of L4 microkernel research and commercial deployment. In addition, seL4 underwent a complete formal verification and is accompanied by a functional correctness proof of its implementation as well as a complete proof chain of high-level security properties down to the executable binary. SeL4 was designed to accommodate dynamic operating systems with high assurance requirements but up to now, its current use cases remain static in nature or combine static components with virtualization.

Here Genode comes into play with the ambition to provide an operating system framework for today's dynamic workloads and security demands. We are proud to announce that Genode 16.08 makes the entirety of the framework's drivers, protocol stacks, libraries, and applications available on top of the seL4 kernel. This enables users of seL4 to compose dynamic and interactive scenarios from a plethora of ready-to-use Genode components. For illustrating the potential, we assembled a live scenario that can be tested in a virtual machine or directly on PC hardware. download the live scenario...