An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
Abstract
Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 10, 2021
- Source ID
- 10.1145/3460860
Entities
People
- Adrien Durier
- Carmine Abate
- Cătălin Hriţcu
- Deepak Garg
- Jérémy Thibault
- Marco Patrignani
- Roberto Blanco
- Éric Tanter
- Ştefan Ciobâcă
Organizations
- Alexandru Ioan Cuza University
- Defense Advanced Research Projects Agency
- European Research Council
- Federal Ministry of Research, Technology and Space
- Max Planck Institute for Software Systems
- Office of Naval Research
- Stanford University
- University of Chile