OS News Archive

The Genode project has released the version 16.05 of the operating-system framework. The new version comes with a fundamentally reworked component API, basic support for the Rust programming language, new ACPI infrastructure, and upgraded device drivers for Intel wireless, Intel graphics, audio, and USB.

The Genode API and the programming styles for developing components evolved over the years. Being born out of the L4 community, the sole reliance on synchronous inter-component communication was deeply ingrained in the developer's mindset when the project was started ten years ago. It took the project a few years to overcome this misconception and embrace asynchronous communication primitives. Most modern Genode components use a mix of both synchronous and asynchronous inter-component interactions. At the API level, however, the two forms of communication remained to exist side by side instead of being integrated in one holistic design. With respect to programming styles, the project underwent a similar evolution. Coming from C-programming background, many parts of the original API resembled a C-ish programming style such as the prominent use of pointers, format strings, side effects via global function calls, or integer error codes. Over the years, however, the expressiveness of the C++ language got fully embraced and the programming style evolved towards functional programming.

Today, most modern Genode components are designed as single-threaded state machines, triggered only by signals and RPC requests originating from other components. There are almost no dynamic memory allocations. If so, allocations are not anonymous but accounted to a specific allocator. State is explicitly passed as arguments, not captured in the form of globally accessible objects. Thanks to this style, certain classes of bugs such as race conditions or memory leaks are greatly alleviated by design. Genode 16.05 cultivates the modern style of Genode components in the form of a fundamentally revised API. The new API is less complex, much safer, and easier to reason about. To account for this profound change, the release documentation is accompanied by a new edition of the "Genode Foundations" book (PDF).

The second major focus of the current release is the updated arsenal of device drivers. All drivers ported from Linux were upgraded to the Linux kernel 4.4.3. Specifically, the drivers are the Intel wireless stack, the Intel graphics driver, the USB driver, and the TCP/IP stack. Thereby, Genode users are able to leverage the same drivers as up-to-date Linux distributions but with each driver being encapsulated in a dedicated protection domain. The audio driver, which originates from OpenBSD, received an update to OpenBSD 5.9. The device drivers are complemented with new infrastructure that makes ACPI platform controlling and monitoring features available to Genode users.

Further highlights are the added ability to use the Rust programming language in Genode components and the enhanced support for using the GNU debugger on top of the NOVA microhypervisor. Details about all improvements and API changes are provided by the extensive release documentation of version 16.05.

Bookmark this website, folks.

As Mark Twain famously wrote, "...the reports of my death are greatly exaggerated". So with OpenVMS.

NICTA, Australia's Information and Communications Technology Research Centre, has published a paper on the lessons learned by 20 years of work around the L4 microkernel.

Some of you may remember that NICTA has developped the seL4 microkernel, one of the first - if not the first - microkernel formally verified, an important stepstone in securing computing systems against whole classes of bugs and attacks.

We first reported on Sortix (version 0.9) a year ago.

As a follow-up to Genode's 16.02 release, the project just published an in-depth article describing the experience with the RISC-V architecture and the steps taken to enable Genode on this platform.

The article is targeted at enthusiasts interested in the practical use of RISC-V and can also be used as a guideline on how to bring Genode to a different CPU architecture.

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.