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 seL4
speaker:Gerwin Klein and Thomas Sewell, NICTA
time: Friday, 14 June 2013, 11:00am
location:
Galois Inc.
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.