Secure Interoperability, Languages, and Compilers

Despite considerable progress in compiler verification in recent years, verified compilers are still proved correct under unreasonable assumptions about what the compiled code will be linked with. These assumptions range from no linking at all—i.e., that compilation units are whole programs—to linking only with code compiled by the same compiler or from the same source language. Such assumptions contradict the reality of how we use compilers in today’s world of multi-language software where most software systems are comprised of components written in different languages compiled by different compilers to a common target, as well as runtime-library routines handwritten in the target language.

The SILC group is investigating techniques for principled compilation and secure interoperability in a world of multi-language software. Our recent research on compositional compiler correctness (or correct compilation of components) has led us to the conclusion that compositional compiler correctness is fundamentally a multi-language problem: solutions to this problem demand both novel language design, in the form of principled FFIs for languages, as well as compilers that preserve type specifications and correctness of refactoring to ensure safe linking with code compiled from other languages.

Our long-term vision is to have verified compilers from languages as different as C, ML, Rust, and Gallina—the specification language of the Coq proof assistant—to a common low-level, richly (and gradually) typed WebAssembly-like target language that enforces safe interoperability between components compiled from more precisely typed, less precisely typed, and untyped source languages.
In pursuit of this vision, we have made progress on challenging problems in a number of areas relevant to correct and secure compilation in the setting of multi-language software.

Research funding

  • NSF: Principled Compiling and Linking for Multi-Language Software (CCF-1816837, 10/2018-9/2021)
  • NSF Graduate Research Fellowship for Aaron Weiss (2017-2022)
  • NSF: Foundations of Just-in-Time Compilation (CCF-1618732, 9/2016-8/2018)
  • NSF CAREER: Verified Compilers for a Multi-Language World (CCF-1453796, 5/2015-4/2020)
  • NSF: Secure Compilation of Advanced Languages (CCF-1422133, 8/2014-7/2017)
  • Google Faculty Research Award: Verified Compilers for a Multi-Language World, (2014)
  • NSF: Effectful Software Contracts (CCF-1203008, 8/2011-7/2014)
SILC is part of the Programming Research Laboratory at Northeastern University.