保持非干扰性的优化编译

《Proceedings of the ACM on Programming Languages》：Non-interference Preserving Optimising Compilation

提出hyperproperty simulations框架，支持任意k-超属性保护，解决现有方法在优化和策略支持上的限制，设计通用非干扰代码转换，减少证明负担，并在Rocq中形式化验证。

　　

摘要

为了保护安全关键型应用程序，安全编译器必须在编译过程中维护诸如“不干扰”之类的安全策略。维护安全策略超出了传统编译器正确性的概念范畴，后者仅要求保留源程序的语义。因此，一些标准的编译器优化操作可能会破坏这些安全策略。现有的安全编译方法在允许的编译器优化类型或支持的安全策略方面存在诸多限制，这主要是由于其形式化框架的概念性局限。

在本文中，我们提出了“超属性模拟”（hyperproperty simulations）这一新颖的安全编译框架，该框架能够模拟编译过程中任意“k-超属性”（k-hyperproperties）的保持机制，并克服了现有方法的诸多局限性，特别是在表达能力和灵活性方面表现更为出色。我们通过设计并证明了一种通用的、能够保持代码不干扰特性的转换方法来验证这一点，该方法可应用于不同的优化策略和数据泄露模型。这种方法将每种优化策略的证明工作量降至最低。我们将这种代码转换应用于多种数据泄露模型，并结合了现有的标准编译器优化技术；而现有的方法在这些场景下的处理能力非常有限，甚至可能根本无法有效应对。我们的研究成果已在Rocq定理证明器中得到了形式化的验证。