Advanced 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.
