|
|
|
High Integrity Language Technology
ACM SIGAda’s Annual International Conference
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.