Secure Compilation

Secure compilation is an area of programming languages research which focuses on compiling/translating languages in way that preserves the security properties of the source language.

The call for papers of the PriSC 2020 workshop states

Secure compilation aims to protect high-level language abstractions in compiled code, even against adversarial low-level contexts, and to allow sound reasoning about security in the source language. The emerging secure compilation community aims to achieve this by: (1) identifying and formalizing properties that secure compilers must possess; (2) devising efficient enforcement mechanisms; and (3) developing effective formal verification techniques.

In logical terms, secure compilation amounts to defining a translation (-)^+ : \mathcal{L}_1 \to \mathcal{L}_2 from a (probably high-level) language \mathcal{L}_1 to a (probably low-level) language \mathcal{L}_2, in a way which preserves observational equivalence. That is,

	e_0 \simeq_{\mathcal{L}_1} e_1 \quad
  \Longrightarrow \quad
  e_0^+ \simeq_{\mathcal{L}_2} e_1^+

This statement hides a lot of nuance in it. Observational equivalence is usually defined through contexts, i.e. terms of the language with a hole punched out. The antecedent thus says that e_0 and e_1 are indistinguishable in all contexts of the language \mathcal{L}_1. Such contexts strictly follow the structure of \mathcal{L}_1, and thus respect all its good security/safety/noninterference properties. On the other hand, the conclusion states that the translations e_0^+ and e_1^+ must also be equivalent, which is to say that they are indistinguishable in all contexts of the language \mathcal{L}_2. As \mathcal{L}_2 is more low-level (even perhaps untyped), it will have less power in enforcing the security properties that were implicitly present in the source language. This additional expressive power can be used to look into the workings of programs that are used to fill them.

References

• The Principles of Secure Compilation workshop is a dedicated venue for the subject.

• Introductory material on secure compilation can be found in the lectures by Amal Ahmed at OPLSS 2019 1 2 3 4

• There is a recent survey paper on secure compilation: