Witnessing Secure Compilation

TL;DR

This paper introduces a translation validation approach for secure compilation that verifies security property preservation during compiler optimizations using automaton-based refinement, avoiding the need to verify compiler correctness itself.

Contribution

It develops a flexible automaton-based refinement scheme to validate security preservation during program transformations, applicable to common compiler optimizations.

Findings

Validation method effectively verifies security preservation.

Can generate and check security witnesses during compilation.

Applicable to real-world compiler optimizations.

Abstract

Compiler optimizations are designed to improve run-time performance while preserving input-output behavior. Correctness in this sense does not necessarily preserve security: it is known that standard optimizations may break or weaken security properties that hold of the source program. This work develops a translation validation method for secure compilation. Security (hyper-)properties are expressed using automata operating over a bundle of program traces. A flexible, automaton-based refinement scheme, generalizing existing refinement methods, guarantees that the associated security property is preserved by a program transformation. In practice, the refinement relations ("security witnesses") can be generated during compilation and validated independently with a refinement checker. This process is illustrated for common optimizations. Crucially, it is not necessary to verify the compiler implementation itself, which is infeasible in practice for production compilers.