Translation validation for a verified OS kernel
Thomas Arthur Leck Sewell, Magnus O. Myreen, Gerwin Klein · 2013
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.