Witnessing Secure Compilation
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.
Cite
@article{arxiv.1911.05866,
title = {Witnessing Secure Compilation},
author = {Kedar S. Namjoshi and Lucas M. Tabajara},
journal= {arXiv preprint arXiv:1911.05866},
year = {2019}
}