OS News Archive

With version 16.02, the Genode OS Framework moves beyond x86 and ARM CPUs and embraces the emerging open-source RISC-V hardware architecture. Furthermore, the release comes with the new ability to securely assign USB devices to virtual machines, and updates the Muen separation kernel and the seL4 microkernel.

Today's x86 and ARM-based commodity platforms have become increasingly opaque and infested with proprietary firmware. With new platforms becoming ever more complex and being equipped with mandatory companion processors like Intel's Management Engine, the trustworthiness of mainstream hardware becomes more and more uncertain. If those parts of the system become compromised, even a perfectly secure OS cannot protect the user's privacy and security. It goes without saying that this development is a strong concern of privacy advocates. The article Intel x86 considered harmful by Joanna Rutkowska substantiates those concerns extremely well.

RISC-V is a possible answer to the call for trustworthy hardware. In contrast to the CPUs of current-generation hardware, RISC-V is an open-source CPU architecture. The idea of open-source CPUs is not new. There exist numerous softcore CPUs like LatticeMico32 or OpenRISC. But in contrast to those projects, which are primarily targeted at FPGA platforms, RISC-V is designed to scale from deeply embedded systems to 64-bit general-purpose platforms. The prospect of a scalable and trustworthy hardware architecture motivated the Genode project to take a closer look. In the just-released version 16.02, RISC-V has been added as a supported architecture to Genode's custom base-hw kernel. Since the hardware is still in flux, the scope of the support is still somewhat limited. But Genode is already able to run on the official Spike simulator as well as on RISC-V as a synthesized FPGA softcore.

Besides the added RISC-V support, the second highlight of the current release is the new ability to securely assign USB devices to VirtualBox instances running on top of the NOVA kernel. With this feature, Genode becomes able to accommodate many typical desktop-OS work flows like transferring data via USB sticks, or obtaining pictures from a digital camera. Under the hood, the implementation is quite interesting as it successfully transplants the xHCI device model of Qemu to VirtualBox.

The third focus of version 16.02 is the update of the Muen and seL4 kernels. The Muen separation kernel has been updated to version 0.7, which greatly improves the interoperability with Genode's tooling. In fact, Muen can now be targeted with the same work flows as employed for all the other kernels. Genode's support for the seL4 kernel is still a rather experimental line of work. In this respect, the update to the kernel version 2.1 posed a number of interesting challenges with respect to the kernel-resource management. This discussion along with details about the many more improvements of the current release is covered in the official release documentation.

I wouldn't exactly call this article "concise", but it's definitely filled with valuable technical information.

Impressive project, and lovely retro '90s website.

In their latest article, the developers of the Genode OS Framework document the long-winded way to their new ARM TrustZone demo on the USB Armory - an open source flash drive sized computer. This undertaking was motivated by the prospect to put Linux, which normally runs on the USB Armory, under the supervision of a significantly less complex Genode hypervisor. This construction enables shielding sensitive information like cryptographic keys from Linux by exposing them to Genode only and thereby drastically reduces the attack surface.

The article illustrates 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. Finally, the article provides you with all tools and information for easily bringing the demo to your own USB Armory.

A very detailed look at this piece of MINIX3 functionality.

GNU Hurd 0.7 and GNU Mach 1.6 have been released.

Since day one of the GNU project, Hurd was supposed to be its kernel - as we all know, of course, it turned out Linux provided a far better kernel with a much faster pace of development, and it's been used as the de-facto GNU kernel ever since. Those with an appreciation for history will love the lingering, mildly dismissive tone of "...such as Linux".

These people are gods.

Impressive.

Where monolithic kernel architectures represent one extreme with respect to kernel complexity, separation kernels mark the opposite end. The code complexity of monolithic OS kernels such as Linux is usually counted in terms of millions of lines of code. In stark contrast, modern microkernels such as NOVA and seL4 are comprised of only ten thousand lines of code. Separation kernels go even a step further by reducing the code complexity to only a few thousand lines of code. How is that possible? The answer lies in the scope of functionality addressed by the different types of kernels. The high complexity of monolithic kernels stems from the fact that all major OS functionalities are considered as being in the scope of the kernel. In particular, device drivers and protocol stacks account for most of the code in such kernels. Microkernels disregard such functionalities from the scope of the kernel by moving them to user-level components. The kernel solely retains the functionality that is fundamentally needed to enable those components to work and collaborate. In order to accommodate a wide range of workloads, microkernels typically provide interfaces to user land that enable the dynamic management of low-level resources such as memory, devices, and processing time. Genode's designated role is to supplement microkernels with a scalable and secure user-level OS architecture. In contrast to microkernels, separation kernels disregard dynamic resource management from their scope. All physical resources are statically assigned to a fixed set of partitions at system-integration time and remain unchanged over the lifetime of the system. The flexibility of microkernels is traded for the benefit of further complexity reduction. Their low complexity of just a few thousand lines of code make separation kernels appealing for high-assurance computing. On the other hand, their static nature imposes limitations on their application areas.

Muen as a representative of separation kernels is special in two ways. First, whereas most separation kernels are proprietary software solutions, Muen is an open-source project. Second, the kernel is implemented in the safe SPARK programming language, which is able to formally verify the absence of implementation bugs such as buffer overflows, integer-range violations, and exceptions. Thanks to the close collaboration between the Muen developers and the Genode community, the assurance of the Muen separation kernel can now be combined with the rich component infrastructure provided by Genode. From Genode's perspective, Muen is another architecture for their custom base-hw kernel. In fact, with Genode on Muen, a microkernel-based system is running within the static boundaries of one Muen partition. This way, the component isolation enforced by the base-hw kernel and the static isolation boundaries enforced by Muen form two lines of defense for protecting security-critical system functions from untrusted code sandboxed within a Genode subsystem.

The second major theme of the current release is the use of Genode as the day-to-day operating system by its developers. Since the beginning of June, one of the core developers is exclusively working with a Genode/NOVA-based system. The key element is VirtualBox with its powerful guest-host integration features. It allows for an evolutionary transition from Linux-centric work flows to the use of native Genode applications. Network connectivity is provided by the Intel wireless stack ported from the Linux kernel. File-system access is based on NetBSD's rump kernels. For using command-line based GNU software directly on Genode, the Noux runtime environment comes in handy. The daily use of Genode as general-purpose OS motivated many recent developments, ranging from the management of kernel memory in NOVA, over new system monitoring facilities, SMP guest support in VirtualBox, to user-facing improvements of the GUI stack. These and many more topics are covered by the comprehensive release documentation.

We've talked about Qubes before, but since it's been a while, here's a quick primer:

This new live USB image should make it a lot easier to give Qubes a go.