一句话：用任意源—目标轨迹关系泛化编译正确性，刻画源与目标轨迹性质的双向保证，统一涵盖未定义行为、侧信道与安全编译。
编译正确性最简形式要求编译后程序的轨迹集合包含于源程序轨迹集合，从而保持所有轨迹性质；但这预设源与目标语言的轨迹集合相同，当语言相距甚远或观察粒度很细时不成立。本文研究一种泛化定义：源与目标轨迹取自可能不同的集合，并由任意关系连接。作者分析当该轨迹关系非恒等时，泛化定义能提供何种保证：源程序的轨迹性质不再被原样保持，因此他们给出通用刻画——正确编译一个满足给定源性质的程序后，目标端被确保的轨迹性质是什么；并给出对偶刻画——为让编译代码获得某目标性质，需要证明的源性质是什么。文章展示该视角可自然容纳未定义行为、资源耗尽、源与目标值差异、侧信道以及各种抽象不匹配，并说明同一泛化也适用于多种安全编译定义，即刻画编译程序与对抗性代码链接时所受的保护。
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.
@article{paperbot1208,
title = {An Extended Account of Trace-relating Compiler Correctness and Secure Compilation},
author = {Carmine Abate and Roberto Blanco and Ştefan Ciobâcă and Adrien Durier and Deepak Garg and Cătălin Hriţcu and Marco Patrignani and Éric Tanter and Jérémy Thibault},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {4},
year = {2021},
doi = {10.1145/3460860}
}