Security Witnesses for Compiler Transformations

Compiler optimizations can be correct and yet be insecure. Program changes made during optimization may weaken security guarantees -- for instance, by introducing new ways to leak secret data. This work presents a methodology for ensuring that security properties are preserved during compilation. Properties are expressed as automata operating over a bundle of related program traces. A notion of automaton-based program refinement guarantees that the associated security property is preserved. In practice, such refinement relations can be generated by a compiler as it optimizes a source program, and validated with an independent refinement checker. This process formally establishes the security of every source-to-target transformation without, however, requiring a proof of correctness of the compiler implementation itself.