Secure Composition of Robust and Optimising Compilers

TL;DR

This paper develops a formal theory for understanding how security properties are preserved when composing multiple secure compiler passes, enabling the construction of secure multi-pass compilers that combine security and optimization.

Contribution

It introduces the first formal framework for analyzing security property preservation across composed compiler passes, including both security and optimization transformations.

Findings

Formalized a theory of security property composition for compilers.

Demonstrated a secure multi-pass compiler that preserves key security properties.

Proved security of the multi-pass compiler based on individual pass properties.

Abstract

To ensure that secure applications do not leak their secrets, they are required to uphold several security properties such as spatial and temporal memory safety as well as cryptographic constant time. Existing work shows how to enforce these properties individually, in an architecture-independent way, by using secure compiler passes that each focus on an individual property. Unfortunately, given two secure compiler passes that each preserve a possibly different security property, it is unclear what kind of security property is preserved by the composition of those secure compiler passes. This paper is the first to study what security properties are preserved across the composition of different secure compiler passes. Starting from a general theory of property composition for security-relevant properties (such as the aforementioned ones), this paper formalises a theory of composition of secure compilers. Then, it showcases this theory a secure multi-pass compiler that preserves the aforementioned security-relevant properties. Crucially, this paper derives the security of the multi-pass compiler from the composition of the security properties preserved by its individual passes, which include security-preserving as well as optimisation passes. From an engineering perspective, this is the desirable approach to building secure compilers.