cispa_all_3332.pdf (535.3 kB)

Trace-Relating Compiler Correctness and Secure Compilation

Download (535.3 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly 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 in order 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 secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.


Preferred Citation

Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu and Marco Patrignani. Trace-Relating Compiler Correctness and Secure Compilation. In: European Symposium on Programming (ESOP). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

European Symposium on Programming (ESOP)

Legacy Posted Date


Open Access Type

  • Unknown


@inproceedings{cispa_all_3332, title = "Trace-Relating Compiler Correctness and Secure Compilation", author = "Abate, Carmine and Blanco, Roberto and Ciobaca, Stefan and Durier, Adrien and Garg, Deepak and Hritcu, Catalin and Patrignani, Marco", booktitle="{European Symposium on Programming (ESOP)}", year="2020", }

Usage metrics


    No categories selected


    Ref. manager