In previous work [Sewell, Myreen and Klein, 2013] we have implemented atranslation validation mechanism for checking that a C compiler is adheringto the expected semantics of a verified program. We used this apparatus tocheck the compilation of the seL4 verified operating systemkernel [Klein et.al. 2009] by GCC 4.5.1. To get this result, wecarefully chose a problem representation that worked well with certain highlyoptimised SMT solvers. This raises a question of correctness. While we areconfident the result is correct, we still aim to replay this result with themost dependable tools available.In this work we present a formalisation of the proof rules needed to replaythe translation check within the theorem prover Isabelle/HOL. This is part ofan ongoing effort to bring the entire translation validation result within asingle trusted proof engine and derive a single correctness theorem, thusreaching the gold standard level of trustworthiness for program verification.We had hoped to present the formal rule set in action through a worked example.Unfortunately while we have all the theory we need, the mechanisms forselecting and applying the rules and discharging certain side conditions remaina work in progress, and our example proof is incomplete.
Formal Replay of Translation Validation for Highly Optimised C
