Above and beyond: seL4 noninterference and binary verification
Authors
NICTA
UNSW
Abstract
In 2009, the L4.verified project completed the world’s first verification of functional correctness for a general-purpose OS kernel, seL4. Functional correctness here was embodied by a formal theorem of refinement, which stated that the behaviour of the C code that implemented the kernel accorded with an abstract specification of how the kernel was meant to function.
A cynic would say that this result proves only that the kernel has no bugs that are not present in its abstract specification or the C compiler. Specifically, while seL4 was designed for security, the functional correctness proof did not rule out the abstract specification specifying insecure behaviour. Further, there was no guarantee that the compiler used to compile the kernel’s C code would produce a binary whose behaviour matched its formal C semantics from the functional correctness proof: the proof did nothing to rule out compiler bugs.
Therefore, two obvious questions remained. Firstly, how do we know that the abstract specification correctly specifies the kernel we want? Secondly, how do we know that the compiler will honour the formal C semantics of seL4?
We present new results on both of these fronts. First, we discuss the recent proof of the classical security property of noninterference for seL4 over its abstract specification. By virtue of the functional correctness proof, we obtain this result automatically for the kernel’s implementation— a world first for a general purpose kernel. Coupled with an earlier proof of integrity for seL4, we now know that it is secure: seL4 provably enforces confidentiality and integrity.
Second, we discuss recent work on applying translation validation to seL4, to formally verify that the binary produced by the compiler adheres to the formal C semantics used in the functional correctness proof. Here, we interpret the binary against a formal model of the ARM ISA developed by Fox et al. to give it a formal semantics, which is then matched-up against the formal semantics of the kernel’s C code, and the match automatically proved by SMT solving.
Combined, these results give us security theorems that apply to the kernel binary; neither the abstract specification nor the compiler need be trusted anymore. seL4 has now become the world’s most deeply verified general-purpose kernel, and so serves as an ideal base for the construction of trustworthy systems. Importantly, system builders can make use of the high level security theorems to obtain system-wide guarantees without needing to trust their kernel or compiler. No other system provides this level of assurance.
BibTeX Entry
@misc{Murray_Sewell_13,
address = {Annapolis, MD},
author = {Murray, Toby and Sewell, Thomas},
booktitle = {2013 High Confidence Software and Systems Conference},
editor = {{34-35}},
month = may,
paperurl = {https://trustworthy.systems/publications/nicta_full_text/7076.pdf},
title = {Above and Beyond: {seL4} Noninterference and Binary Verification},
year = {2013}
}
Full text
BibTeX