SHF: Small: Secure Compilation of Advanced Languages

SHF：小型：高级语言的安全编译

• 批准号: 1422133
• 负责人: Amal Ahmed
• 金额: $ 49.98万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-08-01 至 2017-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422133&HistoricalAwards=false
• 关键词: SHF; Small; Secure; Compilation; Advanced

Title: SHF: Small: Secure Compilation of Advanced LanguagesAdvanced programming languages, based on dependent types, enable program verification alongside program development, thus making them an ideal tool for building fully verified, high assurance software. Recent dependently typed languages that permit reasoning about state and effects---such as Hoare Type Theory (HTT) and Microsoft's F*---are particularly promising and have been used to verify a range of rich security policies, from state-dependent information flow and access control to conditional declassification and information erasure. But while these languages provide the means to verify security and correctness of high-level source programs, what is ultimately needed is a guarantee that the same properties hold of compiled low-level target code. Unfortunately, even when compilers for such advanced languages exist, they come with no formal guarantee of correct compilation, let alone any guarantee of secure compilation---i.e., that compiled components will remain as secure as their high-level counterparts when executed within arbitrary low-level contexts. This project seeks to demonstrate how to build realistic yet secure compilers. This is a notoriously difficult problem. On one hand, a secure compiler must ensure that low-level contexts cannot launch any "attacks" on the compiled component that would have been impossible to launch in the high-level language. On the other hand, a realistic compiler cannot simply limit the expressiveness of the low-level target language to achieve the security goal. The intellectual merit of this project is the development of a powerful new proof architecture for realistic yet secure compilation of dependently typed languages that relies on contracts to ensure that target-level contexts respect source-level security guarantees and leverages these contracts in a formal model of how source and target code may interoperate. The broader impact is that this research will make it possible to compose high-assurance software components into high-assurance software systems, regardless of whether the components are developed in a high-level programming language or directly in assembly. Compositionality has been a long-standing open problem for certifying systems for high-assurance. Hence, this research has potential for enormous impact on how high-assurance systems are built and certified. The specific goal of the project is to develop a verified multi-pass compiler from Hoare Type Theory to assembly that is type preserving, correct, and secure. The compiler will include passes that perform closure conversion, heap allocation, and code generation. To prove correct compilation of components, not just whole programs, this work will use an approach based on defining a formal semantics of interoperability between source components and target code. To guarantee secure compilation, the project will use (static) contract checking to ensure that compiled code is only run in target contexts that respect source-level security guarantees. To carry out proofs of compiler correctness, the project will develop a logical relations proof method for Hoare Type Theory.

标题：SHF：小型：高级语言的安全编译基于依赖类型的高级编程语言可以在程序开发的同时进行程序验证，从而使其成为构建经过充分验证的高保证软件的理想工具。最近允许对状态和效果进行推理的依赖类型语言（例如霍尔类型理论 (HTT) 和 Microsoft 的 F*）特别有前途，并且已用于根据状态相关信息验证一系列丰富的安全策略有条件解密和信息删除的流程和访问控制。但是，虽然这些语言提供了验证高级源程序的安全性和正确性的方法，但最终需要的是保证编译后的低级目标代码具有相同的属性。不幸的是，即使存在这种高级语言的编译器，它们也没有正确编译的正式保证，更不用说安全编译的任何保证——即，在任意环境中执行时，已编译的组件将保持与其高级对应物一样的安全。低级上下文。该项目旨在演示如何构建现实且安全的编译器。这是一个众所周知的难题。一方面，安全编译器必须确保低级上下文无法对已编译组件发起任何在高级语言中不可能发起的“攻击”。另一方面，现实的编译器不能简单地限制低级目标语言的表达能力来实现安全目标。该项目的智力优点是开发了一个强大的新证明架构，用于现实而安全地编译依赖类型语言，该语言依赖于合约来确保目标级上下文尊重源级安全保证，并在正式模型中利用这些合约。源代码和目标代码如何互操作。更广泛的影响是，这项研究将使将高保证软件组件组合成高保证软件系统成为可能，无论这些组件是用高级编程语言还是直接用汇编语言开发的。组合性一直是高可信度系统认证的一个长期悬而未决的问题。因此，这项研究可能会对高保证系统的构建和认证方式产生巨大影响。该项目的具体目标是开发一个经过验证的多遍编译器，从霍尔类型理论到类型保留、正确且安全的汇编。编译器将包含执行闭包转换、堆分配和代码生成的过程。为了证明组件的正确编译，而不仅仅是整个程序的正确编译，这项工作将使用一种基于定义源组件和目标代码之间互操作性的形式语义的方法。为了保证安全编译，该项目将使用（静态）契约检查来确保编译后的代码仅在尊重源级安全保证的目标上下文中运行。为了证明编译器的正确性，该项目将为霍尔类型理论开发一种逻辑关系证明方法。

项目成果

The next 700 compiler correctness theorems (functional pearl)

• DOI: 10.1145/3341689
• 发表时间: 2019-07
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Daniel Patterson;Amal J. Ahmed