Martin Stein

The Genode OS framework is an open-source tool kit for building highly secure component-based operating systems scaling from embedded devices to dynamic desktop systems. It runs on a variety of microkernels like SeL4, NOVA, and Fiasco OC as well as on Linux and the Muen SK. But the project also features its own microkernel named "base-hw" written in C++ like most of the Genode framework.

Spunky is a pet project of mine. Simply put it's an approach to re-implement the design of the "base-hw" kernel first in Ada and later in SPARK with the ultimate goal to prove its correctness. It is also an opportunity to learn how Genode can benefit from Ada and SPARK in general and promote the use of safety-oriented languages in the project.

Networking became a prominent aspect in Genode over the years. As common for microkernel-based systems the whole networking infrastructure, down from the drivers up to the socket implementation resides in the userland and comes in cleanly separated building bricks. Today, the framework provides various such building bricks to be combined into an individual solution for each use case. This includes components like an L2/L3-router component with NAT and DHCP functionality, a network-bridge component, a socket-filesystem server using VFS, NIC and Wifi-drivers, as well as libraries like the Lightweight IP and the Linux IP stack. The talk shall give an overview about the design of this ecosystem, how it can be used, how it evolved, and, last but not least, discuss its future.

A fundamental aspect of the Genode OS project always was the support for various kernels as back-end. It remarkably raised testing versatility and provided a high flexibility to users and developers. But supporting the Genode API on self-contained third-party kernels is sometimes also accompanied with deficiencies, redundancies, or work-arounds. To also have the option of a basic kernel without such compromises, the custom Genode kernel was developed. Its main distinguishing mark may be that it not only trusts the Genode Core-component but even more is a mere library to it. The implications of this new design and other characteristics of the custom Genode kernel, such as scheduling, capabilities, and ARM virtualization, are discussed in this lecture.

The USB Armory is an open source computer in the form of a USB stick. It normally runs Linux. But thanks to the ARM TrustZone capabilities of the device, it is possible to run the Genode OS Framework as microhypervisor behind the back of Linux. This is useful for shielding sensitive information like cryptographic keys from Linux by exposing it to Genode only and thereby drastically reducing the attack surface. Even in the event Linux gets compromised, e.g., by a vulnerability in the USB stack, the secrets remain protected.

In the talk, I'll first give a short introduction into the USB Armory project and its motivation. After that, I'll tell the development story of Genode's microhypervisor scenario. I'll also illustrate how the TrustZone technology is used to isolate Genode from Linux without compromising the rich feature set of Linux, and how both worlds can safely communicate with each other. Last but not least, I'll demonstrate the scenario itself and how it can be reproduced.