seL4 Is Free – What Does This Mean For You?

Gernot Heiser introduces the open-source seL4 microkernel, explaining its mathematical proof of security and how it guarantees the absence of common software bugs.

Gernot Heiser lca2015.linux.org.au/schedule/30011/view_talk seL4 is the world's most secure OS kernel, in a very strong sense: It has a mathematical proof of security that connects high-level security and safety properties with the binary code that is running on the processor, there is no other system that can make such clams. And it is 100% Australian-made. seL4 runs on ARM and x86 processors and combines the properties of a general-purpose microkernel, a military-style separation kernel, a hypervisor able to run Linux, a protected-mode real-time OS and more. However, until recently it was locked up and basically inaccessible. But, as of 29 July 2014 it is open source. In this talk I will briefly explain what seL4 is (and isn't), what it can do and where it can be deployed, and what its formal verification is all about, i.e. what it can and cannot guarantee. Then I will focus on discussing what this means for the community. As seL4 defines the state of the art in trustworthy systems, I will make the point that it is the right platform for new designs of safety- or security-critical systems, where failure can lead to loss of life or may have massive financial impact. I will encourage the community to contribute to building the seL4 ecosystem, and use it to make everyday computer systems more dependable.