Download files
Abstract
Computer software is typically written in one language and then translated
out of that language into the native binary languages of the machines the
software will run on. Most operating systems, for instance, are written in the
low-level language C and translated by a C compiler. Translation
validation is the act of checking that this translation is correct. This
dissertation presents an approach and framework for validating the translation
of C programs, and three experiments which test the approach.
Our validation approach consists of three components, a frontend, a backend and
a core, which broadly mirrors the design of the C compiler. The three
experiments in this dissertation exercise these three components. Each of these
components produces a formal proof of refinement, and these
refinement proofs compose to produce a proof that the binary is a refinement of
the source semantics. This notion of refinement can then compose with
correctness proofs for a C program, resulting in a verified binary.
Throughout this work, our case study of interest will be the seL4 verified
operating system kernel, compiled for the ARM instruction-set architecture, for
which we will produce a verified efficient binary.
The thesis of this work is that our translation validation approach
offers us great flexibility. We can quickly produce verified binaries
produced via many complex transformations without specifically addressing each
such transformation. We can adapt our frontend to handle low-level source code
which 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 well
as correctness ones.