Languages (High-Integrity and Otherwise) in seL4 and Beyond

Friday, November 30, 2012

Abstract: The formal verification of the functional correctness of the seL4 micro-kernel’s 8-9k lines of C code was built on top of an elaborate tower of languages and techniques. With the exception of the logical “language” used within the Isabelle theorem-prover, none of these were languages that one would necessarily feel comfortable about labelling “high-integrity”. The kernel itself is written in C, but the project also made extensive use of SML, Haskell, and even Python.

After giving some background on the basic structure of the kernel verification, I will describe how we knitted together these languages into what we believe is 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, our logical approach occasionally allowed us to side-step questions of correctness entirely. I will also describe some of our current thinking about moving beyond the micro-kernel. For example, we want to support programs that are built on top of the kernel and can exploit its guarantees.

Bio: Dr. Michael Norrish is a Principal Researcher at the Canberra Research Laboratory of National Information and Communications Technology Australia Limited (NICTA). He is a well-known researcher in the areas of Formal Methods and Interactive Theorem Proving. He is especially known for his work in developing the HOL4 theorem-proving system and for his role in the recent, high-profile verification effort related to the seL4 micro-kernel. More information about his work and research interests can be found on his web site at http://www.nicta.com.au/people/norrishm.

Related Links

• U of M Research centers and institutes
• Undergraduate Research Opportunities Program
• Experts@Minnesota
• Office of Graduate School Outreach
• CSE Research
• CS&E Driven to Discover
• Colloquia
• Talks