Sat 13 Jan 2018 17:00 - 17:30 at Hershey - Session 3 Chair(s): Lars Birkedal

Fully abstract compilation has long been understood to be useful for building secure compilers, but most verified compilers are not fully abstract. In particular, much recent work in the verified compilers community has gone into building compilers that are able to link with code that may not be produced from the same compiler. This is an important area of progress, because real software is made up of components written in different languages compiled by different compilers. But a key challenge is how to formally state the compiler correctness theorem so it supports linking with target code of arbitrary provenance. Recent results state their correct-component-compilation theorems in remarkably different ways, yielding pros and cons that aren’t well understood. Worse, to check if these theorems are sensible, reviewers must understand a massive amount of formalism. Further complicating things, compilers have multiple passes, which means that results from single passes need to be lifted to multi-pass compilers which often requires non-trivial work.

In this talk, we will survey recent results and present a generic compositional compiler correctness (CCC) theorem that we argue is the desired theorem for any compositionally correct compiler. Specific compiler-verification efforts can use their choice of formalism ``under the hood'' and then show that their theorems imply CCC. Using this theorem, we will show how fully abstract compilation relates to compositional compiler correctness, and argue that even researchers uninterested in secure compilation would still benefit from building fully abstract compilers, as they lead to easier composition of multi-pass compilers.

Slides (ccc-prisc.pdf)1.88MiB
extended abstract (prisc18-paper6.pdf)415KiB

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

16:00 - 18:00: Session 3PriSC at Hershey
Chair(s): Lars BirkedalAarhus University
16:00 - 16:30
Talk
Constant-time WebAssembly
PriSC
John RennerUCSD, Sunjay CauligiUCSD, Deian StefanUniversity of California, San Diego
Pre-print File Attached
16:30 - 17:00
Talk
Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
PriSC
Robert SisonData61, CSIRO and UNSW
File Attached
17:00 - 17:30
Talk
On Compositional Compiler Correctness and Fully Abstract Compilation
PriSC
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
File Attached
17:30 - 18:00
Talk
Foundations of Dependent Interoperability
PriSC
Pierre-Evariste DagandLIP6/CNRS , Nicolas TabareauInria, France, Éric TanterUniversity of Chile
Link to publication File Attached