Galois is pleased to host the following tech talk. These talks are open to the interested public--please join us! (There is no need to pre-register for the talk.)
Please note that this talk is on Friday, at 11am
title:Non-interference and Binary Correctness of seL4speaker:Gerwin Klein and Thomas Sewell, NICTA
time: Friday, 14 June 2013, 11:00am
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract: This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.
The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.
The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.
bio: Thomas Sewell has worked in the verification group at NICTA for seven years as a staff engineer and Isabelle/HOL proof specialist. Thomas was part of the seL4 proof effort from the beginning, working on the functional correctness proof and later proofs of security properties. He has recently begun joint work with Magnus Myreen (Cambridge University) to work on binary verification for the compiled kernel, and has also recently enrolled at UNSW as a PhD student on this project.
Gerwin Klein is Principal Researcher at NICTA, Australia's National Centre of Excellence for ICT Research, and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is leading NICTA's Formal Methods research discipline and was the leader of the L4.verified project that created the first formal, machine-checked proof of functional correctness of a general-purpose microkernel implementation in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München,Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL.
Gerwin has won a number of awards together with his team, among them the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, and NICTA's Richard E. Newton impact award for the kernel verification work.