Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Secure Composition of Robust and Optimising Compilers

Matthis Kruse, Michael Backes, Marco Patrignani

TL;DR

The paper tackles the problem of understanding how security properties are preserved when composing secure compiler passes that may enforce different guarantees. It develops a general framework for secure composition using cross-language trace relations and universal image projections, and proves that composition preserves the intersection of property classes under suitable well-formedness conditions. A concrete case study demonstrates a six-pass pipeline that preserves the target property specms by combining passes for temporal and spatial memory safety, cryptographic constant time, and speculative safety, along with optimisations. The results provide a principled, modular approach to building secure compilers where end-to-end security of multi-pass pipelines derives from the security guarantees of the individual passes, with formal proofs and a Coq formalization accompanying the development.

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.

Secure Composition of Robust and Optimising Compilers

TL;DR

The paper tackles the problem of understanding how security properties are preserved when composing secure compiler passes that may enforce different guarantees. It develops a general framework for secure composition using cross-language trace relations and universal image projections, and proves that composition preserves the intersection of property classes under suitable well-formedness conditions. A concrete case study demonstrates a six-pass pipeline that preserves the target property specms by combining passes for temporal and spatial memory safety, cryptographic constant time, and speculative safety, along with optimisations. The results provide a principled, modular approach to building secure compilers where end-to-end security of multi-pass pipelines derives from the security guarantees of the individual passes, with formal proofs and a Coq formalization accompanying the development.

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.
Paper Structure (43 sections, 22 theorems, 29 equations, 3 figures)

This paper contains 43 sections, 22 theorems, 29 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Background: Properties and Secure Compilers
  3. Properties and (Robust) Satisfaction
  4. Secure Compilers
  5. Secure Composition
  6. Secure Compiler Composition with Same Trace Models
  7. Security Properties Formalisation & Composition
  8. A Trace Model for Memory Safety
  9. Temporal Memory Safety
  10. Spatial Memory Safety
  11. Memory Safety
  12. A Trace Model for Memory Safety with Constant Time
  13. Strict Cryptographic Constant Time
  14. ms, Strict Cryptographic Constant Time
  15. Extending the Trace Model with Speculation
  16. ...and 28 more sections

Key Result

Theorem 3.1

$\;$ If RoyalBlue$\;\vdash_{{\sim_1}}{\gamma{}^{\mathsf{{\color{RoyalBlue}{L}}}}_{\mathbf{{\color{RedOrange}{L}}}}\xspace}:{\tilde{\sigma}_{\sim_2}\left(\mathbf{{\color{RedOrange}{\mathbb{C}_{1}}}}\right)}$, RedOrange$\;\vdash_{{\sim_2}}{\gamma{}^{\mathbf{{\color{RedOrange}{L}}}}_{\mathtt{{\color{Em

Figures (3)

  • Figure 1: Example program where the level of optimisations differ for one pass of applying cf and dce in any order. Every edge is a compilation pass and the label on the edge states what the pass does, i.e., cf or dce. The source code in the nodes is a glorified compiler intermediate representation and the code gets more optimised towards the right hand side of the figure.
  • Figure 2: Traces for \ref{['ex:lscct']}.
  • Figure 3: Visualisation of the optimising compilation pipeline that preserves specms. Vertices in the graph are the programming languages from earlier sections (\ref{['sec:casestud:defs']}). Full edges are secure compilers passes. Dotted edges are composition of passes and use the presented framework (\ref{['sec:sequential']}) to indicate the property they preserve. The dashed lines partition the graph into the sections where the respective theorems are presented.

Theorems & Definitions (42)

  • Example 1.1: strncpy
  • Definition 2.1: Property Satisfaction
  • Definition 2.2: Robust Satisfaction
  • Definition 2.3: Universal Image
  • Definition 2.4: Robust Preservation with $\sigma_\sim$
  • Definition 2.5: Robust Preservation
  • Definition 3.1: Well-formedness of $\sim$ for a Class $\mathbf{{\color{RedOrange}{\mathbb{C}}}}$
  • Theorem 3.1: Composition of Secure Compilers w.r.t. $\sigma$
  • Corollary 3.1: Swapping Secure Compiler Passes
  • Corollary 3.2: Composition of Secure Compilers
  • ...and 32 more