Translation validation for verified, efficient and timely operating systems

Computer software is typically written in one language and then translatedout of that language into the native binary languages of the machines thesoftware will run on. Most operating systems, for instance, are written in thelow-level language C and translated by a C compiler. Translationvalidation is the act of checking that this translation is correct. Thisdissertation presents an approach and framework for validating the translationof C programs, and three experiments which test the approach. Our validation approach consists of three components, a frontend, a backend anda core, which broadly mirrors the design of the C compiler. The threeexperiments in this dissertation exercise these three components. Each of thesecomponents produces a formal proof of refinement, and theserefinement proofs compose to produce a proof that the binary is a refinement ofthe source semantics. This notion of refinement can then compose withcorrectness proofs for a C program, resulting in a verified binary.Throughout this work, our case study of interest will be the seL4 verifiedoperating system kernel, compiled for the ARM instruction-set architecture, forwhich we will produce a verified efficient binary.The thesis of this work is that our translation validation approachoffers us great flexibility. We can quickly produce verified binariesproduced via many complex transformations without specifically addressing eachsuch transformation. We can adapt our frontend to handle low-level source codewhich does not strictly respect the rules of the C language it is written in.We can also retarget our backend to address important timing concerns as wellas correctness ones