Session
Schedule FOSDEM 2020
Microkernels and Component-based OS

seL4 Microkernel Status Update

K.4.601
Gernot Heiser
I will give an overview of where seL4 stands today in terms of functionality, verification, ecosystem, deployment and community. The focus will be on what has happened in seL4 land over the past 12 months, which is a lot: seL4 Foundation, RISC-V support and introducing time protection.

The biggest news of the year is that we are in the process of setting up the seL4 Foundation, as an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. I will report on the state of this.

The other big development is that we are closing in on completing verified seL4 on the open RISC-V architecture. This includes the functional correctness proof (that guarantees that the kernel is free of implementation bugs), the binary correctness proof (which guarantees that the compiler did not introduce bugs) and the tranition to the new mixed-criticality scheduling model, which supports the safe co-location of critical real-time software with untrusted components, even if the latter can preempt the former.

Finally, on the research side we have introduced the new concept of time protection (the temporal equivalent of the established memory protection) that allows us to systematically prevent information leakage through timing channels.

Additional information

Type devroom

More sessions

2/2/20
Microkernels and Component-based OS
Nils Asmussen
K.4.601
Current microkernels have shown to provide advantages in terms of security, robustness, and flexibility of systems. However, in recent years, the hardware added new challenges that need to be addressed as well, demanding approaches that include the hardware into the picture. First, hardware is getting more and more heterogeneous and consists not only of general-purpose cores, but contains also various accelerators. Second, system designers need to integrate untrusted third-party components ...
2/2/20
Microkernels and Component-based OS
Jakub Jermář
K.4.601
This is going to be an all-encompassing update talk for HelenOS developments that happened in the Year of the Pig (since the last FOSDEM).
2/2/20
Microkernels and Component-based OS
Hajime Tazaki
K.4.601
LKL (Linux Kernel Library) is aiming to allow reusing the Linux kernel code as extensively as possible with minimal effort and reduced maintenance overhead. It allows us to link the library with any programs (which wish to call as a function call) containing Linux kernel code. There are many use cases: reading/writing files without general system calls, putting experimental protocol implementation without neither of host kernel update nor kernel module installation, using customized kernel in ...
2/2/20
Microkernels and Component-based OS
Dmitry Zavalishin
K.4.601
Phantom OS is an Operating system based on the orthogonal persistence. Application does not feel OS shutdown and restart. Even abrupt restart. It is guaranteed that application will be restarted in consistent state.
2/2/20
Microkernels and Component-based OS
Johannes Kliemann
K.4.601
Gneiss is an abstraction layer for component based environments that aims to provide a foundation for formally provable components. It enables the creation of platform independent, asynchronous components in SPARK and provides function contracts that allow to prove the correct interaction with the underlying platform.
2/2/20
Microkernels and Component-based OS
Alexander Senier
K.4.601
With 2.5 billions of active users Android is the most widely deployed mobile operating system in the world. Its vast complexity paired with a monolithic architecture regularly result in severe security issues like the infamous Stagefright bug. In this presentation we talk about an ongoing research project which aims at running Android applications on top of the component-based Genode OS framework and secure them using formally verified components. We discuss how Android applications interact, ...
2/2/20
Microkernels and Component-based OS
Norman Feske
K.4.601
Sculpt OS is a novel general-purpose operating system designed from the ground up and implemented using the building blocks of the Genode OS framework. It started with the vision of a truly trustworthy OS that combines a completely new system structure with microkernels, capability-based security, sandboxed device drivers, and virtual machines. The talk is a live demonstration of the current incarnation of Sculpt.