Modeling interoperability between programs in different languages is a key problem when modeling compositional and secure compilation, which has been successfully addressed using multi-language semantics. Unfortunately, existing models of compilation using multi-language semantics define two variants of each compiler pass are defined: a syntactic translation on open terms, and a run-time translation of closed terms at multi-language boundaries
We introduce a novel work-in-progress approach to uniformly model a compiler entirely as a reduction system on open term in a multi-language semantics, rather than as a syntactic translation. This simultaneously defines the compiler and the interoperability semantics, reducing duplication. It also provides interesting semantic insights. Normalization of the cross-language redexes performs ahead-of-time (AOT) compilation. Evaluation in the multi-language models just-in-time (JIT) compilation. Confluence of multi-language reduction implies compiler correctness. Subject reduction of the multi-language reduction implies type-preservation of the compiler. This model provides a strong attacker model through contextual equivalence, retaining its usefulness for modeling secure compilation as full abstraction.
William J. Bowman is an assistant professor of computer science at the University of British Columbia in Vancouver. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, and meta-programming. His recent work examines type-preserving compilation of dependently typed programming language like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.
Sun 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30: Secure compilers & cryptographyPriSC at PriSC Chair(s): Fraser BrownStanford University, USA, Aastha MehtaMPI-SWS, Germany and University of British Columbia, Canada | |||
16:00 - 16:18 Talk | High-level high-speed high-assurance crypto PriSC Jonathan CoganStanford, Fraser BrownStanford University, USA, Alex OzdemirStanford, Riad S. WahbyStanford University, USA Media Attached | ||
16:18 - 16:36 Talk | Cross-Architecture Testing for Compiler-Introduced Security Bugs PriSC Media Attached File Attached | ||
16:36 - 16:54 Talk | High-Assurance Cryptography in the Spectre Era PriSC Gilles BartheMPI-SP, Germany / IMDEA Software Institute, Spain, Sunjay CauligiUniversity of California at San Diego, USA, Benjamin GregoireINRIA, Adrien KoutsosINRIA Paris, Kevin LiaoMax Planck Institute for Security and Privacy, Tiago OliveiraUniversity of Porto (FCUP) and INESC TEC, Swarn PriyaPurdue University, Tamara RezkInria, France, Peter SchwabeMax Planck Institute for Security and Privacy Media Attached | ||
16:54 - 17:12 Talk | Compilation as Multi-Language Semantics PriSC William J. BowmanUniversity of British Columbia Pre-print Media Attached | ||
17:12 - 17:30 Talk | Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs PriSC Coşku AcayCornell University, Rolph Recto, Joshua GancherCornell University, Andrew C. MyersCornell University, Elaine ShiCornell University Media Attached |