Programming languages with advanced type systems facilitate the development of reliable software by giving programmers the ability to express numerous safety and security properties of their programs via types.  Violations of these properties can be caught via type checking at compile time, rather than at run time. Languages like OCaml and F# have types that provide memory safety and information hiding guarantees, while dependently typed languages such as that of the Coq proof assistant have richer types that enable verification of full functional correctness during program development.  In recent years, numerous projects have used Coq to build fully verified software fromOS kernels to compilers to cryptographic protocols.

While advanced typed languages are a powerful tool for verifying safety, security, and correctness of source programs, what is ultimately needed is a guarantee that the same properties hold of compiled low-level code.  Unfortunately, compilers for such advanced languages come with no formal guarantee of correct compilation in the presence of linking with other code, let alone any guarantee of secure compilation---i.e., that compiled components will remain as secure as their source-level counterparts when linked with arbitrary target-level code.  This is a concern because compiled code is routinely linked with libraries implemented directly in the target language or compiled from other source languages. Formally, a correct compiler is one that preserves the semantics of all source code it compiles, while a secure compiler is one that is fully abstract: it guarantees that two compiled components can be distinguished by some target-level code if and only if their source-level counterparts can be distinguished by some source-level code. Thus, secure compilers have the added benefit of allowing programmers to reason about their programs (such as correctness of refactoring) by *thinking* only in their source language.  

This project has developed methods for building realistic yet secure (fully abstract) compilers for advanced typed languages, a notoriously difficult problem. Fully abstract compilation has historically been achieved by either making the source language more expressive or making the target language less expressive. Both approaches are infeasible in the context of real compilers whose target languages are usually more expressive than the source, allowing target-level attackers to make observations about compiled components that source-level attackers cannot make about the original source component---e.g., via disruptions of control flow, or inspection of information private to a module.

A central goal was to demonstrate that source-language types can be translated/compiled to target-language types (static contracts) that can be used to ensure that target-level contexts respect source-level security guarantees.  The use of static rather than dynamic contracts for ensuring security is critical as it allows us to avoid the significant performance overheads that accompany dynamic enforcement of security guarantees.

The first major result of our project is the development of correct and *typed* compiler passes for the core language of the Coq proof assistant. These include typed CPS translation, which since 2002 was conjectured to be impossible, and typed closure conversion that is compatible with critical features of Coq.  These results are key to building a practical verified compiler for Coq which would ensure that fully verified source code cannot be compromised via compiler bugs or unsafe linking.

The second major outcome are proof techniques for verifying that acompiler is fully abstract.  The project devised "backtranslation" techniques that demonstrate that target-level attackers can be modeled at source level, even when the target language contains features that are absent from the source.  Different classes of proof techniques were developed for terminating languages (back-translation by partial evaluation) and for Turing-complete languages (back-translation via universal embedding).  

The third major result is development of interoperability semantics between high-level (direct-style) languages and a low-level assembly, that supports embedding assembly in high-level programs, and vice versa, while ensuring safety of the mixed program.  The key challenge was developing a notion of "components" in assembly such that components can be made up of different number of basic blocks and can be nested. This should inform design of other high/low multi-languages, e.g., for verification of C code mixed with assembly and just-in-time (JIT) compilers.

Finally, the project noted the tension between secure compilation--which must disallow linking with code whose behavior cannot be expressed in the compiler's source language--and the building of useful multi-language software--which frequently demands such linking.  The project advocated that language designs be extended to facilitate development of compilers and toolchains that support building multi-language software.  Specifically, every language should come with *linking types* extensions that provide programmers with the means to annotate their source code to express the points where they wish to link with code behaviors that cannot be expressed in their language.  Giving programmers high-level means to control low-level linking seems essential for building practical secure compilers and toolchains that report cross-language type errors to aid in the development of multi-language software.

Last Modified: 04/19/2018
Modified by: Amal Ahmed