OS News Archive

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.

MenuetOS 1.0 has been released.

Congratulations to the MenuetOS team for sticking with it - this is a great achievement. ComputerWorld Australia has an interview with Ville Turjanmaa, its creator.

It's built on top of Gecko, so you can use Firefox OS APIs. Interesting.

The just released version 14.11 of the Genode OS framework complements the framework's arsenal of device drivers with the Intel wireless stack. This way, Genode enables the realization of microkernel-based systems on modern laptops without relying on any kind of "device-driver OS" or "Dom0". Other highlights of the release are a new dynamic linker, VirtualBox 4.3.16 on the NOVA hypervisor, a new scheduler for the HW kernel, and networking for the Raspberry Pi.

WiFi stacks are known to be extremely complex. In the Linux kernel, it is certainly one of the most sophisticated driver subsystems besides GPU drivers. From the perspective of an alternative OS, it is quite frightening. On the other hand, WiFi is an universally required feature for a general-purpose OS by today's standards. Therefore, the Genode project had to face the issue to enable a full WiFi stack on top of the framework sooner or later. In spring this year, the Genode team finally took on the engineering feat to transplant the Intel wireless stack from Linux to a user-level component on Genode. This line of work was more demanding than originally anticipated. The biggest hurdle was to get a grasp on the interactions between the various involved protocols and mechanisms such as mac80211, cfg80211, nl80211, the netlink API, AF_NETLINK, and the WPA supplicant. The actual porting work followed the approach of prior porting efforts like the Linux USB and TCP/IP subsystems. All Linux kernel threads are executed by a single user-level thread that cooperatively schedules each kernel thread as a light-weight execution context. Compared to the prior porting efforts, the driver environment for the WiFi stack is far more complex. About 8,500 lines of environment code had to be provided to bring the 215,000 lines of WiFi stack to life. However, almost no original code had to be changed, which will make future updates relatively easy.

From its very beginning, Genode was designed to manage resources via a trading mechanism. For example, when a client component connects to a server component, it can provide a part of its own memory budget to the server. This way, the server does not need to perform allocations from its own resources on behalf of its client, which mitigates the risk for denial-of-service attacks driven by malicious clients. This scheme works well for memory but it had not been employed for CPU time, yet. The reason was the lack of the scheduling facilities offered by the kernels supported by Genode. However, with their custom kernel called "base-hw", the Genode developers were finally able to pursue this idea. The outcome of this line of work is featured in the new release.

Besides the WiFi stack and the new scheduler, Genode 14.11 comes with an upgrade of VirtualBox to version 4.3.16 that can be executed directly on the NOVA microhypervisor, a new dynamic linker, added GUI components, and networking support for the Raspberry Pi. The full story behind all those topics is covered by the release documentation.