seL4: Present and future
Authors
NICTA
UNSW
Abstract
seL4, a member of the L4 family of microkernels, and the world’s highest-assured operating system kernel, has recently joined the FLOSS community. This talk will provide an overview of what seL4 is, what it can and cannot do, and where we see it heading in the future.
I will start of briefly summarising the concept of a microkernel, and the core principles which characterise the L4 microkernel family. I will then introduce the core concepts of seL4, and what distinguishes it functionally from other L4 kernels.
What makes seL4 really special is its formal verification. I will explain what this is, and what exactly we have proved about seL4, and discuss what this means in practice, especially as far as security, safety and reliability are concerned. I will also indicate where we are planning to take seL4, i.e. a high-level summary of our on-going research and development projects.
Having covered the technical aspects, I will discuss the development process of the seL4 ecosystem, both past and present. I will specifically discuss the licensing status of various bits of this ecosystem, and how it is likely to develop. In particular I will indicate suggest the best way for the community to contribute to this ecosystem, and help develop it to the benefit of us all.
BibTeX Entry
@misc{Heiser_15_2,
address = {Brussels, BE},
author = {Heiser, Gernot},
booktitle = {FOSDEM'15},
keywords = {sel4 microkernels security verification safety},
month = feb,
note = {invited talk at FOSDEM'15},
slides = {https://trustworthy.systems/publications/nicta_slides/8551.pdf},
title = {{seL4}: Present and Future},
year = {2015}
}
Slides
BibTeX