HILT 2012             ACM logo - Advancing Computing as a Science & Profession

High Integrity Language Technology
ACM SIGAda’s Annual International Conference

Formal Verification of the seL4 microkernel

Michael Norrish

Abstract

Michael Norrish will discuss the various languages used in the course of the source-level verification of the seL4 micro-kernel. With the exception of the logical "language" used within the Isabelle theorem-prover, none of these were languages that one would feel completely comfortable labeling "high-integrity".

The kernel itself is written in C, but the project also made extensive use of SML, Haskell, and even Python.

Michael will describe how these languages were knitted together into a convincing verification. Most of this "knitting" technology was formal proof, but the proofs did not always follow the traditional approach of verifying source code with respect to a complete specification. Instead, the logical approach chosen allowed side-stepping questions of correctness entirely in some cases.

Michael will also describe some of the current thinking about moving beyond the micro-kernel. For example, they hope to support programs that are built on top of the kernel and that exploit its guarantees.


Created on 30 November 2012;  website comments and corrections to ClydeRoby at ACM.Org