The Genode project announced the version 15.08 of their OS framework. The most prominent topics of the current release are the use of Genode as day-to-day operating system by their developers and the added ability to run Genode-based systems on top of the Muen separation kernel.
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.
That is a wall of text we have there, but its a very nice wall of text that informs and delights the senses. Unlike the previous nextbsd one…
Finally some great positive less than mainstream Os News on OSnews! I’mma going to rejoice by trying to figure geode out.
This is a great story but it should really be condensed to a paragraph on the homepage like every other story.
Acutally, I think it would have been ok if the 2nd paragraph had been axed…
It’s interesting to see an open source kernel in Ada/Spark
Edited 2015-09-01 04:23 UTC
Makes sense. Readability of code even without inline comments is important after all.
Nice! Going to “eat your own dogfood” is an important indication of maturity…
Great to see Ada and SPARK being used in this way in an open source / free software project.
Yes, when SPARK was mentioned in the previous report, it “sparked” me to look into SPARK and Ada a little bit. I’d never heard of SPARK before, and I hadn’t thought about Ada for a long time. There have been several versions of the Ada standard since I last checked, and the changes seem positive.
I may not have much practical use for it, but it’s nice to stretch the mind in different directions.
I wish there was an easy way to try the latest version with Muen kernel on a virtual machine.
I agree with this. It would be nice to have some pre-build VM images, to make it easier to get started playing around with it.
If there are any, please let us know!
This is exactly the kind of architecture mobile devices should be using, but for whatever reasons aren’t. We may flatter ourselves for being involved in a forward thinking industry, but at heart it’s painfully conservative.
So what are the actual tradeoffs when compared to a monolithic kernel? Reliability vs Security vs Memory vs Performance? Because the only arguments I’ve ever gotten for Android not using a microkernel like Neutrino or L4 were that it’s unfamiliar to users.
But would such a kernel have made updating Android easier? Would it have been more memory conservative than Linux (the Android devs were completely obsessed with memory back in the day)? Would it improve battery life or security?
I think the predominance of traditional OS architectures has primarily non-technical reasons. On technical grounds, Blackberry has demonstrated that a microkernel can very well be used for building a good-performing smartphone OS.
The decision for or against a given OS foundation is the result of judging business risks. The Linux kernel is proven technology. It enjoys an enormous mind share, which includes chip vendors. As long as its architecture does not fundamentally contradict with selling products (like a smart phone), it is just reasonable to use it. In contrast, investing in a largely unproven alternative technology would have a much higher risk with no tangible benefit for the vendor. Even with the recently growing awareness regarding privacy and security, smart phones based on traditional OS technology still sell. So from the vendor’s perspective, there is no need to replace the existing OS foundation by something different.
Consequently, outside the application areas where high security or robustness are mandated, microkernel-based OS architectures still remain a curiosity. With Genode, we hope to significantly reduce the business risk of basing products on microkernel technology so that more and more application areas can benefit from it.