一句话：提出超性质模拟框架，统一刻画编译过程中 k-超性质的保持，并给出可复用的非干扰保持代码变换。
安全编译器必须在编译过程中保持安全策略（如非干扰），而经典编译正确性只要求源程序语义被保持，因此许多标准优化可能破坏非干扰等策略。现有安全编译方法在概念框架上受限，对可用的编译器优化或可支持的安全策略限制过强。本文提出「超性质模拟」（hyperproperty simulations），一种新的安全编译框架，能够建模任意 k-超性质在编译过程中的保持，在表达力与灵活性上超越已有方法。基于该框架，作者设计并证明了一个通用的非干扰保持代码变换，可实例化到不同的优化与泄漏模型上，从而把每个优化所需的证明负担降到最低。该变换在多种泄漏模型与若干标准编译器优化上得到实例化，而这些优化在既有方法中至多只能以受限且缺乏模块化的方式处理。所有结果均在 Rocq 证明助手中形式化验证。
To protect security-critical applications, secure compilers have to preserve security policies, such as noninterference, during compilation. The preservation of security policies goes beyond the classical notion of compiler correctness which only enforces the preservation of the semantics of the source program. Therefore, several standard compiler optimisations are prone to break standard security policies like non-interference. Existing approaches to secure compilation are very restrictive with respect to the compiler optimisations that they permit or to the security policies they support because of conceptual limitations in their formal setup. In this paper, we present hyperproperty simulations , a novel framework to secure compilation that models the preservation of arbitrary k -hyperproperties during compilation and overcomes several limitations of existing approaches, in particular it is more expressive and more flexible. We demonstrate this by designing and proving a generic non-interference preserving code transformation that can be applied on different optimisations and leakage models. This approach reduces the proof burden per optimisation to a minimum.We instantiate this code transformation on different leakage models with various standard compiler optimisations that could be handled in a very limited and less modular way (if at all) by existing approaches. Our results are formally verified in the Rocq theorem prover.
@article{paperbot2919,
title = {Non-interference Preserving Optimising Compilation},
author = {Julian Rosemann and Sebastian Hack and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763101}
}