Translation Validation for a Verified OS Kernel

Select |




Print


Sewell, Thomas; Myreen, Magnus; Klein, Gerwin

Sewell, Thomas; Myreen, Magnus; Klein, Gerwin


2013-06-16


Conference Material


ACM-SIGPLAN Conference on Programming Language Design and Implementation (PLDI)


Seattle, Washington, USA


471-481


We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware. More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process. We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2.


ACM


Isabelle, seL4, microkernel, binary verification


http://pldi2013.ucombinator.org


nicta:6449


Sewell, Thomas; Myreen, Magnus; Klein, Gerwin. Translation Validation for a Verified OS Kernel. In: ACM-SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Seattle, Washington, USA. ACM; 2013-06-16. 471-481.



Loading citation data...

Citation counts
(Requires subscription to view)