Submitted by 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.
That is still waiting for a medical grade open OS.
Great release! And thanks you for that detailed documentation: very nice!
The new effort taken in porting audio drivers makes me wonder:
Wouldn’t it be better to extend the existing rump-kernel support (now used for filesystems) to support audio as well?
Also networking could be realized via rumpkernels. That would give Genode a flexible but universal way of providing drivers: rump-kernels for almost any piece of hardware.
With a broad support for rump-kernel hypercalls, porting new drivers could be done by users by building a dedicated rk.
Edited 2015-05-26 21:37 UTC
Thanks for all the nice feedback!
Regarding the question about using Rump kernels vs. porting individual drivers: This is decided on a case-by-case basis. For file systems, we used Rump kernels because of the high amount of code to port. So the overhead (in terms of complexity, memory consumption, build-system mechanics) of using Rump kernels is ok. For situations where individual drivers are to be ported and the drivers use a well designed interface to the kernel (as is the case for the OpenBSD audio drivers), it is quite easy to just port the driver. In such cases, we prefer this lean approach to avoid the overhead that comes with a large runtime as a Rump kernel.
So it’s an OS framework? I’m curious if there are any actual OS’s out there (real or hobbyist) that uses this. Anyone?
Sure:
it runs e.g. a paravirtualized version of linux as a user prozess of genode. It provides its own userland with a port of qt5 and e.g. a web-browser. It providedes a environment to run posix command line tools.
It slso can run android as a guest on arm. Or via virtualbox anything that runs on that.
Impressive!
I am always impressed with the progress from the Genode team, and this time is certainly no exception. The functionality (and documentation!) is maturing quickly.
I am still reading the release notes, but just wanted to say “keep up the good work”!