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：小：基于依赖类型的高级语言编程的安全汇编，启用程序验证以及程序开发，从而成为构建完全验证的高保证软件的理想工具。最近允许有关状态和效果推理的近期类型的语言 - 例如Hoare类型理论（HTT）和Microsoft的F*---尤其有希望，并且已用于验证一系列丰富的安全策略，从国家依赖性信息流和访问控制到有条件的解密和信息擦除。但是，尽管这些语言提供了验证高级源程序的安全性和正确性的手段，但最终需要的是保证相同的属性保留了编译的低级目标代码。不幸的是，即使存在此类高级语言的编译器，它们也无法正式保证正确的编译，更不用说任何保证安全编译的保证了，即，在任意低级上下文中执行时，编译的组件将保持与其高级对应物一样安全。该项目旨在演示如何建立现实但安全的编译器。这是一个众所周知的困难问题。一方面，安全的编译器必须确保低级上下文不能在编译的组件上启动任何“攻击”，这是无法以高级语言启动的。另一方面，现实的编译器不能简单地限制低级目标语言的表现力来实现安全目标。该项目的智力优点是开发有力的新证明体系结构，以实现依赖合同的相关语言的现实且安全的编译，以确保目标级别的环境尊重源级别的安全性保证，并以正式模型的方式来确保源和目标代码如何相互键入。更广泛的影响是，这项研究将使您可以将高保证软件组件构成高保证软件系统，而不管组件是用高级编程语言开发还是直接在组装中开发。对于认证系统的高保证系统，构图一直是一个长期的开放问题。因此，这项研究可能会对高保险系统的构建和认证产生巨大影响。该项目的具体目标是开发一个经过验证的多通编译器，从Hoare类型理论到保存，正确和安全的类型的组装。编译器将包括执行封闭转换，堆分配和代码生成的通行证。为了证明组件的正确汇编，不仅是整个程序，这项工作将使用一种方法来定义源组件和目标代码之间互操作性的正式语义。为了确保安全汇编，项目将使用（静态）合同检查，以确保仅在尊重源级安全保证的目标上下文中运行编译的代码。为了执行编译器正确性的证据，该项目将开发出Hoare类型理论的逻辑关系证明方法。

项目成果

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