-
The most widely deployed mobile virtualization solution
Data Sheets
Open Kernel Labs Blog
January 17, 2008
Ask Gernot - Gernot Heiser on his L4.verified presentation
BW from OK: Gernot, I hear you are talking about L4.verified at the Open Group conference in San Francisco. What will your talk cover?
I will report on the work done by my team at NICTA on a formally-verified L4 microkernel as a basis for highly secure systems. This means a kernel that has a mathematically-precise and unambiguous API, and a proof that the implementation (the actual C and assembler code) correctly implements that specification. Which means that we will have a guarantee that any security-relevant properties of the API are present in the implementation. In everyday language: a proof that the kernel implementation is free of bugs.
BW: Is this so special?
Quite. Only a small number of (tiny and highly specialized) operating systems have gone through this level of rigor. No general-purpose system exists to date that has such a proof. Not even EAL7 (the highest level of Common Criteria security certification) demands this — because it's been considered infeasible to date. (And, by the way, to date no OS has even been certified to EAL7.) So this will be a true world's first, and is bound to raise expectations on high-security OSes.
BW: So, what has been achieved to date?
Over the past two years, my team at NICTA has developed a new version of the L4 AIP, called seL4, which aims at meeting the separation and information-flow requirements of highly-secure systems (eg Common Criteria Separation Kernel Protection Profile). The API, semi-formally specified in the Haskell functional programming language, has been converted into a mathematical model in Isabelle/HOL, a theorem-proving tool. A number of basic isolation properties have been proved, and further proofs are in progress.
Concurrently we are working on what is called a refinement proof from the API to the C/assembler code. This is progressing in two steps: First a proof that an intermediate-level model of the kernel is consistent with the API, then that the C/assembler code is consistent with the intermediate model. That model is in fact also a program: it is an implementation of the spec in Haskell (and could, in principle also be used as a kernel running on bare metal, although at somewhat sucking performance). The first refinement is completed, so we can now say that we have a verified Haskell kernel. But that is not the intention: in true L4 spirit, we want something that is as high-performance as it gets.
BW: What remains to be done?
Mostly the second refinement, the proof of the C/ assembler code, which is now in progress. A lot of preliminary work has already been done, such as building extensive proof libraries for low-level machine features, a formal semantics of our dialect of C, an automated tool for formalizing the C code, a formal model of the hardware (to give meaning to the assembler code) etc. The remaining bits are mostly grunt work; most of the technical risk is gone. We are now no longer concerned whether we'll be able to pull it off, but only whether we stay on schedule. So we're convinced we'll have a formally verified high-performance kernel this year!
BW: What then?
The IP will be transferred to OK, with the aim of repeating the feat on the OKL4 production kernel, and get it out as a product. OK is already working on a stepwise evolution of the OKL4 API towards something equivalent toseL4. This will continue, and we will then verify the OKL4 implementation, and also produce the same sort of security proofs I mentioned for seL4. This will happen without compromising the unbeaten performance of OKL4.
BW: What else will your talk cover?
I will talk a bit about our experience in the project, how we approached it, provide statistics about proof sizes etc. I'm quite looking forward to it 
About the Open Group:
The Open Group is a vendor-neutral and technology-neutral consortium, whose vision of Boundaryless Information Flow will enable access to integrated information, within and among enterprises, based on open standards and global interoperability.
Posted by Gernot Heiser on January 17 at 06:42 PM
blog comments powered by Disqus
About Gernot Heiser:
Gernot Heiser, Co-founder and Consulting Scientist, never thought he would be in the business world. Prior to NICTA's creation in 2003, Dr Heiser was a full-time faculty member at the University of New South Wales. However, this die-hard academic couldn’t pass up the opportunity to see the commercialization of this research. Gernot still loves teaching, almost as much as he loves good wine and good food. And anyone will tell you that Gernot knows his wine.