Greetings. Microkernels rarely appear on Habré, but this week there was a topic about the GNU / Hurd , where they remembered various microkernels and known projects. Many inaccuracies were said, so I decided to talk about how things are going in the industry from our point of view. The fact is that we are actively involved in the development of Fiasco.OC and Genode projects and are developing on their basis, so we have a lot to say.

A bit of history

I think Mach’s core is fairly well known, so I’ll touch it very briefly. It was developed at Carnegie Mellon University in the late 80s - early 90s, after the project was closed at CMU, it developed at Utah University and then, in my opinion, it was already called GNU / Mach. GNU / Mach is part of the GNU / Hurd OS. This is a rather slow microkernel, it only supports x86.
At the end of the 90s, Jochen Liedtke ( Jochen Liedtke ) proposed a new, optimized architecture of the microkernel, first L3, then L4. Unfortunately, in 2001 he had an accident and died. L4 is an ideology and it is documented in the L4 eXperimental reference manual. Now the latest version of X.2 rev.7 Anyone can read this document and program "their" microkernel architecture L4. As a result, quite a few different micronuclear projects appeared in the 00s.

The most famous projects.

There have been many projects, not all have survived to the present, I will tell you about the most famous of the currently existing
1. L4Ka :: Pistachio, Karlsruhe Institute of Technology
This is the team of Jochen Liedtke, they developed a microkernel and environment. Currently this team is not developing the L4Ka project, but this project has spawned many others.
2. Projects of the NICTA Group
NICTA Group - Information and Communications Technology (ICT) Research Center of Excellence. This organization is engaged in projects in the field of system programming, pattern recognition, artificial intelligence, some nano. In general, the most popular areas of CS, which are very popular in the 00th and in the future. At the same time, this organization not only invests in reseche-projects, it conducts them from the idea and searching at the university right up to the products and sales of the company.
The history of the L4Ka microkernel development is very indicative in this respect. First there was the research project NICTA :: Pistachio-embedded (created on the basis of the L4Ka :: Pistachio microkernel from KIT), then inside NICTA the OKL company (Open Kernel Lab) was created, which was engaged in the development of products based on the Pistachio microkernel. Then they made their product - the OKL4 microkernel and in the region of 2007 they signed a contract with Qualcomm, since then the microkernel is present in smartphones on Qualcomm chips. In the recently leaked Qualcomm datasheets, for example, there is a description of the Api L4 (although I'm not sure, I caught a glimpse). More recently, OKL4 was sold to General Dynamics.
L4.verified - formally verified kernel on the L4 architecture. This is a scientific development of the NICTA Group, we can assume that the track of this project will be like OKL4. The main idea of ​​this project is to mathematically prove the correctness of the kernel implementation. The fact is that microkernels, unlike monolithic modular monsters like GNU / Linux, are small, and they can be formally verified, that is, a theorem is written for each line of code, and proving all the theorems, something is proved to be consistent. The L4.verified micronucleus proves compliance with the model implementation, the absence of perpetual loops, and some more things. The cost of this study was about $ 6 million, the project lasted 7 years. The amount of work is 25 man-years. This is a colossal and very interesting work. Its obvious use is war, security.
seL4 is a security-oriented operating system, I don’t know with a verified kernel or not. On the NICTA website you can download binaries.
3. MINIX3
This is a project of the Andrew Tanenbaum team. The main focus in the MINIX3 microkernel is fault tolerance and desktop application. I know little about this project, but some of the developers were present at FOSDEM in the past, and there is a small community of enthusiasts in Russia.
4. HelenOS
This is a development of students at Faculty of Mathematics and Physics at Charles University in Prague. This project has been developing for quite a long time, the kernel supports modern hardware platforms. And in 2012 they participated in the GSoC. In the core, there were initially architectural flaws, for example, the core was not fully micro - part of the device driver was still in the core. Now, as far as I know, this architectural flaw has been eliminated. I personally do not like the fact that being positioned as a general purpose OS, they do not support normal drivers.
5. TU Dresden Projects
At Dresden Technical University there is a research group of Professor Hermann Härtig . He published and worked together with Jochen Liedtke, and the students under his management developed many interesting projects in the field of operating systems. Older kernels - L4 / Fiasco (first L4 core in TUD), VFiasco (attempt to verify Fiasco, 2005)
Modern kernels:
Fiasco.OC is a microkernel written in C ++, built on the concept of Everything Is Object. Supports ARM, x86, ppc, sparc v8. Starts on modern platforms like panda. We are actively involved in the development of this project. The authors of the kernel (Adam Lackorzynski and Alexander Warg), as far as I know, left TUD a couple of months ago and organized their own startup to support and develop microkernels.
NOVA is a micro-hypervisor. It was developed by Udo Steinberg, now it continues to develop this hypervisor in Intel.
As you understand, microkernels themselves are not functional, so TUD has developed an environment for microkernels: L4Re - L4 Runtime Environment. This is a set of libraries and application software that can be run on top of the Fiasco and Fiasco.OC micronuclei. It consists of a para-virtualized L4Linux, a wrapper for using Linux drivers DDEKit (by the way, there is such a DDEKit in GNU / Hurd). This makes it easy to use existing software and use the microkernel in commercial projects. This is a very fast “entry” into microkernels, which seems to me very important. The negative point is that TU Dresden rarely puts updates and there is almost no work of the community. So for example, we keep the groundwork and our version of l4Linux in github.
Genode framwork - Project Norman Feske and Christian Helmuth. They graduated from TU Dresden and have previously worked on the development of a safe graphics subsystem and the development of microkernels. Now they have their own startup, they are developing a framework for various microkernel (not only) operating systems. In Genode, in contrast to TUD, regular releases and roadmap, the sources are in github and everyone can take part in its development. We are also developing this project, and the Fiasco.OC + Genode framework is interesting for us.
In other words, micronuclear projects from TUD are now moving from the state of “experimental student projects” to a real product on which to build their products. So the growth of the community and the involvement is just what is needed now.

6. Singularity

About this project have already been written , I will not touch

FOSDEM

This year we took part in FOSDEM and I talked about our experience in using microkernel OSs. I did not attend the remaining sessions, because on the first day I attended our devroom, and the next day we had a demo section for half a day, where we showed the firmware for a trusted phone on the microkernel, l4linux and Genode. In the devroom there were projects:
GNU / Hurd, told about him Samuel Thibault, the most active I think the developer of this project. He spoke first, and was present at the panel discussion.
Genode labs, talked about their work over the past year. They ported the Genode framework to pandaboard in 2012. I think this is very significant, and extremely useful for the development of the framework and micronuclei, as it adds popularity. We did not take part in the port on the pandaboard, although we were the first to launch Genode on real ARM based hardware.
Also present were HelenOS, they told about their plans for the next year, about what is already supported in HelenOS.
There was Udo and talked about NOVA, about the fact that the performance loss of this hypervisor is lower than that of Xen and eSXI, besides this hypervisor is supported in Genode, that is, virtual machines can be run in parallel with the application software on top of the microkernel.
There were also some new guys who talked about DSL, but this has little to do with microkernels.
From TUD, there was Bjoern Doebel , he talked about his Open Source framework for replication. This is his research project.
One young man from TU Berlin attended the demo section. TU Berlin has a T Lab department that deals with RnD in the field of information security. In particular, they are developing a trusted phone on a para-virtualized L4Android for Deutsche Telecom.
I liked the presentations, and, by the way, next year we will organize Microkernels and Component-based OS devroom.
')
P / S / And yet, last year we spent the summer school of system programming, and now we are looking for students who want to find themselves in the field of Computer Science and system programming. In order to get to our team, you need to see the first three lectures ( 1 , 2 , 3 ) and complete the tasks from them. The solution needs to be put on github and send me a link to sartakov@ksyslabs.org.

P / P / S / If it is interesting, I can tell you about the main trends and trends in the system programming of recent years.

P / P / P / S This year we are preparing a new school, but more on that later