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.

翻译：为确保安全应用不泄露其秘密，它们需要满足多项安全属性，如空间与时间内存安全性以及密码学常数时间性。现有研究展示了如何通过专注于单个属性的安全编译器过程，以架构无关的方式分别强制执行这些属性。然而，给定两个各自保持可能不同安全属性的安全编译器过程，目前尚不清楚这些安全编译器过程的组合会保持何种安全属性。本文首次研究了不同安全编译器过程组合后保持的安全属性。从安全相关属性（如前述属性）的通用组合理论出发，本文形式化了安全编译器的组合理论。随后，通过一个保持前述安全相关属性的安全多过程编译器展示了该理论。关键的是，本文从各独立过程（包括安全保持过程与优化过程）所保持安全属性的组合中推导出多过程编译器的安全性。从工程视角看，这是构建安全编译器的理想途径。