OS News Archive

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.

With the just released version 15.11, the Genode OS framework takes a big step towards desktop computing. On that account, its GUI and audio stacks have become much more modular, dynamic, and flexible. Moreover, the release features the port of Intel KMS from Linux, extends the support for the USB Armory and Xilinx Zynq-7000, and introduces new file-system infrastructure such as a VFS server.

In their release documentation, the Genode developers dedicate an entire section (including screenshots) to the ambition to use Genode as desktop OS. It turns out that the framework's existing component architecture solves a number of difficult problems in new and elegant ways. For example, the configuration of all types of components - be it low-level device drivers or high-level GUI components - can be edited live with a plain text editor. The changes become effective by merely saving a file. This works even for components that have no means or permissions to access a file system at all. Another interesting twist on classical GUI-integration features is Genode's new copy-and-paste mechanism that prevents the clipboard to be misused by malicious applications as a covert information channel while retaining the convenience of traditional clipboard mechanisms.

At a lower level, the desktop theme of the release is supported by the new Intel KMS driver ported from the Linux kernel. It allows the use of multiple displays, and screen resolutions can be switched on the fly. With nearly 70,000 SLOC of Linux kernel code, the porting was a major feat. This work continues the pattern of reusing Linux kernel code, which already enabled Genode to use the Intel wireless stack, the Linux USB stack, and the Linux TCP/IP stack as user-level components. The Intel KMS driver is interesting also in another respect: Since it is tightly coupled with the Intel GEM and DRM infrastructure of the Linux kernel, those subsystems had to be ported as well. So the driver may become a suitable starting point for the development of a future GPU multiplexer.

Thanks to the developer's continuous focus on making the framework fit for day-to-day computing, Genode is now used by a hand full of die-hard Genode enthusiasts as their primary OS. Still, many tasks are carried out via a guest OS in VirtualBox. But all of the circa 40 underlying components such as the kernel, device drivers, protocol stacks, and a growing number of applications are working nicely together and are stable and fast enough to get productive work done.

Besides the main focus on desktop computing, the release is not short of other areas of improvement. Xilinx Zynq-7000 has been added to the supported platforms, TrustZone on the USB Armory received a lot of attention, and a new VFS server makes Genode's file-system infrastructure much more flexible. Those and many more topics are covered by the detailed release documentation.

A very detailed look at this piece of MINIX3 functionality.

We've already talked about OOSMOS before, but the project's just gone open source.

These people are gods.

OZ V4.6, a continuation of the actual operating system of the Z88, has been released.

Incredibly impressive project.

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.

The just released version 15.05 of the Genode OS Framework is the most comprehensive release in the project's history. Among its highlights are a brand-new documentation in the form of a book, principal support for the seL4 microkernel, new infrastructure for user-level device drivers, and the feature completion of the framework's custom kernel.

For many years, the Genode OS project was primarily geared towards microkernel enthusiasts and the domain of high-security computing. With version 15.05, the project likes to widen its audience by complementing the release with the downloadable book "Genode Foundations" (PDF). The book equips the reader with a thorough understanding of the architecture, assists developers with the explanation of the development environment and system configuration, and provides a look under the hood of the framework. Furthermore, it contains the specification of the framework's programming interface. If you ever wondered what Genode is all about, the book may hopefully lift the clouds.

Besides the added documentation, the second focus of the new version is the project's custom kernel platform called base-hw. This kernel allows the execution of Genode on raw hardware without the need of a 3rd-party microkernel. This line of work originally started as a research vehicle for ARM platforms. But with the addition of kernel-protected capabilities, it has reached feature completeness. Furthermore, thanks to the developers of the Muen isolation kernel, base-hw has become available on the 64-bit x86 architecture. This represents an intermediate step towards running Genode on top of the Muen kernel.

Speaking of kernels, the current release introduces the principle ability to run Genode-based systems on top of the seL4 microkernel. As the name suggests, seL4 belongs to the L4-family of microkernels. But there are two things that set this kernel apart from all the other family members. First, with the removal of the kernel memory management from the kernel, it solves a fundamental robustness and security issue that plagues all other L4 kernels so far. This alone would be reason enough to embrace seL4. Second, seL4 is the world's first OS kernel that is formally proven to be correct. That means, it is void of implementation bugs. This makes the kernel extremely valuable in application areas that highly depend on the correctness of the kernel.

At the architectural level, the framework thoroughly revised its infrastructure for user-level device drivers, which subjects device drivers to a rigid access-control scheme with respect to hardware resources. The architectural changes come along with added support for message-signaled interrupts and a variety of new device drivers. For example, there is a new AHCI driver, new audio drivers ported from OpenBSD, new SD-card drivers, and added board support for i.MX6.

Further noteworthy improvements are the update of the tool chain to GCC 4.9.2, support for GPT partitions, and the ability to pass USB devices to VirtualBox when running on NOVA. These and the many more topics of the version 15.05 are covered in great detail in the release documentation.

The code's on github.