Sat 13 Jan 2018 14:00 - 14:30 at Hershey - Session 2 Chair(s): David Naumann

We map the space of soundness criteria for secure compilation based on the preservation of hyperproperties in arbitrary adversarial contexts, which we call robust hyperproperty preservation. For this, we study the preservation of several classes of hyperproperties and for each class we propose an equivalent “property-free” characterization of secure compilation that is generally better tailored for proofs. Even the strongest of our soundness criteria, the robust preservation of all hyperproperties, seems achievable for simple transformations and provable using context back-translation techniques previously developed for showing fully abstract compilation. While proving the robust preservation of hyperproperties that are not safety requires such powerful context back-translation techniques, for preserving safety hyperproperties robustly, translating each finite trace prefix back to a source context seems to suffice.

slides (2018-01-prisc.pdf)1.35MiB

Sat 13 Jan

prisc-2018
13:30 - 15:30: PriSC 2018 - Session 2 at Hershey
Chair(s): David NaumannStevens Institute of Technology
prisc-2018151584660000013:30 - 14:00
Talk
File Attached
prisc-2018151584840000014:00 - 14:30
Talk
Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniSaarland University, CISPA, Marco Stronati, David SwaseyMPI-SWS
Pre-print File Attached
prisc-2018151585020000014:30 - 15:00
Talk
Guglielmo FachiniInria Paris, Cătălin HriţcuInria Paris, Marco Stronati, Ana Nora EvansUniversity of Virginia, USA, Théo Laurent, Arthur Azevedo de AmorimCarnegie Mellon University, USA, Benjamin C. PierceUniversity of Pennsylvania, Andrew TolmachPortland State University
Pre-print File Attached
prisc-2018151585200000015:00 - 15:30
Talk
File Attached