21C3 Schedule Release 1.1.7

21st Chaos Communication Congress
Lectures and workshops

Speakers
Picture of Adam Lackorzynski Adam Lackorzynski
Picture of Michael Peter Michael Peter
Schedule
Day 1
Location Saal 4
Start Time 15:00 h
Duration 01:00
INFO
ID 115
Type Lecture
Track Hacking
Language english
FEEDBACK

The Fiasco ┬ÁKernel

In the talk we will present an overview about the L4 microkernel family as well as systems built on top of it. We will focus on L4Linux and secure systems. The distinguished feature of L4 microkernels is their limitiation to the most primitive abstractions. All other functionality is implemented in user land. The system design allows that system core components can be isolated by address spaces. L4Linux is a port of the Linux kernel to the L4 microkernel. L4Linux runs as a user space application side by side with other L4 programs on the microkernel system. We will present the design and the most interesting implementation details.

Building secure systems on top of microkernels exemplifies how kernel design influences the overall characteristics of the whole system. In the second part of the talk we will outline how such a secure system can be constructed and will show an example on top of L4.

The talk will give an overview of the L4 microkernel family and systems built utilizing a microkernel. We will briefly introduce DROPS the OS project of the TU Dresden group.

L4 microkernels only accomdate functionality that cannot be implemented in user space thereby striving for minimality. The current set of abstractions comprises threads as abstractions of activity, address spaces as protection domain and IPC as a safe communication primitive. Other functionality that is found in monolithic kernels like file systems and process management is implemented in OS personality servers in user space. The provided primitives facilitate a component oriented system design where components are isolated and communicate only through small, well defined interfaces.

One of the systems built on top of an L4 microkernel is L4Linux. L4Linux is a port of the Linux kernel to L4 and runs as a user space application side by side with other L4 programs. L4Linux is binary compatible with the standard Linux, i.e. it runs unmodified off-the-shelve Linux distributions. The first L4Linux version was developed in 1996. The current version of L4Linux is based on Linux 2.6. L4Linux is utilized in scenarios ranging from acting as a driver infrastructure container providing hardware abstractions at driver level to native L4 applications to running multiple instances with different requirements.

The second topic will be secure systems. Building secure systems based on microkernels is attractive as the involved components are relatively small and can be assembled as needed. Keeping the software for the Trusted Computing Base small is one goal of such systems. A small TCB is a key requirement for secure systems as otherwise (high) assurance claims cannot be substantiated. In the talk we will present one example of such a system, involving several of the aforementioned parts of the project.

If circumstances permit, we'll also show a (small) demo.