Trustworthy Systems

Formal replay of translation validation for highly optimised c: Work in progress

Authors

Thomas Sewell

NICTA

UNSW

Abstract

In previous work we have implemented a translation validation mechanism for checking that a C compiler is adhering to the expected semantics of a verified program. We used this apparatus to check the compilation of the seL4 verified operating system kernel by GCC 4.5.1. To get this result, we carefully chose a problem representation that worked well with certain highly optimised SMT solvers. This raises a question of correctness. While we are confident the result is correct, we still aim to replay this result with the most dependable tools available.

In this work we present a formalisation of the proof rules needed to replay the translation check within the theorem prover Isabelle/HOL. This is part of an ongoing effort to bring the entire translation validation result within a single trusted proof engine and derive a single correctness theorem, thus reaching 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 for selecting and applying the rules and discharging certain side conditions remain a work in progress, and our example proof is incomplete.

BibTeX Entry

  @inproceedings{Sewell_14,
    address          = {Vienna, Austria},
    author           = {Sewell, Thomas},
    booktitle        = {Verification and Program Transformation},
    keywords         = {translation validation, isabelle/hol, verification},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8102.pdf},
    title            = {Formal Replay of Translation Validation for Highly Optimised C: Work in Progress},
    year             = {2014}
  }

Download