New book "Genode Foundations" May 29, 2015

The book "Genode Foundations" is available as a free download.

We are proud to announce a milestone in our history: A book that describes the Genode OS Framework in a holistic and comprehensive way. It 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.

The book "Genode Foundations" is ready to be downloaded at http://genode.org.

Combining Genode with the seL4 microkernel May 29, 2015

At the end of May, Genode reached a point that allows us to run simple Genode scenarios on the seL4 kernel.

Back in the newsletter of November 2014, we first mentioned the seL4 kernel. Now, we are excited to follow up on this topic.

The seL4 microkernel is the world's first operating-systems kernel that is formally verified to contain no implementation bugs. As its name suggests, it is a member of the L4 family of kernels. With the other family members it shares the fundamental construction principle to provide mechanisms but no policy. But it is the first kernel that applies this principle to the management of its own memory resources. It thereby solves a long-standing robustness and security concern of traditional L4 kernels. At the same time, seL4 is designed to scale well towards dynamic workloads.

Both the proven absence of implementation bugs and the sound concept of its kernel resource management make this kernel extremely valuable in application areas that ultimately depend on the correctness of the kernel under all circumstances.

In summer last year, after being proprietary technology for several years, seL4 was published as an open-source project.

Even though seL4 is designed to accommodate dynamic workloads, its existing user-level infrastructure is limited to static systems. This is where Genode comes into play. By enabling Genode to run on top of seL4, seL4 will eventually become able to execute all the dynamic application workloads that Genode provides.

At the end of May, we reached a point that allows us to run simple Genode scenarios on this kernel. While pursuing this line of work, we took the opportunity to thoroughly document our steps. The result are following three articles:

Building a simple root task from scratch

IPC and virtual memory

Porting the core component

The current state of development has already been incorporated into the main development of Genode and is featured in the official version 15.05.

postal address:

  Genode Labs GmbH
  Dammweg 2
  D-01097 Dresden

visiting address:

  Genode Labs GmbH
  Friedrichstr. 26
  D-01067 Dresden

phone:

  +49 351 3282613

email:

  info@genode-labs.com