seL4 Is Free – What Does This Mean For You?
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.
Gernot is the microkernel dude, he and his team have been building the world's fastest microkernels for almost 20 years, and his OKL4 microkernel is deployed in billions of mobile devices. He's also the John Lions Chair of Operating Systems at UNSW (that chair was established with the help of funds raised at LCA'06). Many of his students are well known in the Linux community. And he leads the Software Systems research group at NICTA, Australia's ICT Centre of Excellence.