seL4 2.0.0 released

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce seL4 release 2.0.0. The new release cleans up a large backlog of improvements we have been working on for the last 18 months. It also marks the transition to more frequent and regular releases, to minimise the lag between internal and public versions. We have also switched our release process to semantic versioning, so it’s easy to tell which seL4 releases are binary-compatible, source-compatible, or will require updates to user-level code. Specific changes are performance improvements to the IPC fastpath and scheduling, making seL4 even faster overall. All changes are formally verified for ARMv6 to full seL4 standard. There are also changes to terminology to eliminate confusion introduced by some object and system call naming in the past. For details please see the Release Notes posted on the developer mailing list.

More information:

seL4 Developer Day, October, Malibu

Two things to announce for seL4:

They’ve released a roadmap for development and verification.

And they’ve a Developer Day event happening next month. I missed the information about their first Developer Day last month. They’ve just announced a second Developer day, October 8-9, organized in conjunction with DARPA, hosted at HRL Labs, in Malibu, California.

Genode OS v15.05

Found on Joanna’s Twitter feed:

Genode is new to me. Genode Labs makes the “Genode OS Framework”. Genode is a new OS, not a new Linux distribution. It is “a GPLv2-licensed construction kit for building specialized operating systems out of small building blocks including different kernels, device drivers, protocol stacks, and applications”. This current release is a major release for Genode. The new documentation is a large 472 page PDF. The current release adds “rudimentary GPT” support. GPT aside, I don’t see any other UEFI-related technology support, only “BIOS” references to firmware.

Version 15.05 represents the most substantial release in the history of Genode. It is packed with profound architectural improvements, new device drivers, the extension of the supported base platforms, and a brand new documentation.

We understand the complexity of code and policy as the most fundamental security problem shared by modern general-purpose operating systems. Because of high functional demands and dynamic workloads, however, this complexity cannot be avoided. But it can be organized. Genode is a novel OS architecture that is able to master complexity by applying a strict organizational structure to all software components including device drivers, system services, and applications.”

“The current implementation can be compiled for 8 different kernels: Linux, L4ka::Pistachio, L4/Fiasco, OKL4, NOVA, Fiasco.OC, Codezero, and a custom kernel for running Genode directly on ARM-based hardware. Whereas the Linux version serves us as development vehicle and enables us to rapidly develop the generic parts of the system, the actual target platforms of the framework are microkernels. There is no ‘perfect’ microkernel – and neither should there be one. If a microkernel pretended to be fit for all use cases, it wouldn’t be ‘micro’. Hence, all microkernels differ in terms of their respective features, complexity, and supported hardware architectures.

Genode allows the use of each of the kernels listed above with a rich set of device drivers, protocol stacks, libraries, and applications in a uniform way. For developers, the framework provides an easy way to target multiple different kernels instead of tying the development to a particular kernel technology. For kernel developers, Genode contributes advanced workloads, stress-testing their kernel, and enabling a variety of application use cases that would not be possible otherwise. For users and system integrators, it enables the choice of the kernel that fits best with the requirements at hand for the particular usage scenario.

Inverse Path’s USB Armoury supports Genode as of 15.02:  “The Genode OS Framework supports the USB armory since version 15.02 implementing a TrustZone Secure virtual-machine monitor (VMM) supervising Linux running in the Normal world. Support is in the very early stages. The Linux kernel requires minimal patching to be executed in the Normal world, at the moment Martin Stein from Genode Labs provides a repository with a patched kernel.