SHF: Small: Secure Compilation of Advanced Languages

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

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.