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.

翻译：为确保安全应用不泄露其机密，它们需要维护多项安全属性，例如空间和时间的存储安全性以及密码学常数时间执行。现有工作展示了如何以与架构无关的方式，通过分别关注单项属性的安全编译器遍次来逐一强制执行这些属性。然而，当面对两个分别可能维护不同安全属性的安全编译器遍次时，尚不清楚这些安全编译器遍次的组合会维护何种安全属性。本文首次研究了不同安全编译器遍次组合后可维护的安全属性。从安全相关属性（如上述属性）的属性组合一般理论出发，本文形式化了一套安全编译器组合理论。随后，通过一个维护前述安全相关属性的安全多遍编译器实例，对该理论进行了论证。关键之处在于，本文从单个遍次（包括安全保持与优化遍次）所维护的安全属性组合中，推导出了该多遍编译器的安全性。从工程角度来看，这是构建安全编译器的理想方法。