Semantic Intermediate Representations for Sound Language Interoperability

Abstract

Designers of typed programming languages commonly prove meta-theoretic properties such as type soundness and, if applicable, security properties such as noninterference, for at least a core of their language. But any practical language implementation must provide some way of interoperating with code written in other languages – usually via a foreign-function interface (FFI) – which opens the door to new, potentially unsafe and insecure, behaviors that aren’t accounted for in the original type soundness or security proofs. Despite the prevalence of interoperability in practical software, principled foundations for the end-to-end design, implementation, and verification of interoperability mechanisms have been largely neglected.

In this talk, I’ll advocate a proof technique for ensuring soundness or security properties of practical languages, which implement interoperability using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). This proof technique involves building a semantic intermediate representation: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. More interestingly, semantic IRs provide a basis for numerous avenues of future work on the principled design of language interoperability: how to support the inclusion of libraries whose behavior is foreign to the original language, how to prove soundness and security properties that are robust to behaviors (attackers) outside of the semantic IR, and how to develop a compiler IRs and backends that makes it easier to implement and verify sound interoperability for a wide array of source languages.