Write a Blog >>
Sat 25 Jan 2020 10:54 - 11:18 at Rosalie - Foundations and timing channels Chair(s): Marco Vassena

Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that the same generalization also applies to a large class of secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.

slides (slides.pdf)367KiB

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 12:30
Foundations and timing channelsPriSC at Rosalie
Chair(s): Marco Vassena CISPA Helmholtz Center for Information Security
10:30
24m
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco Patrignani Stanford University & CISPA , Marco Guarnieri IMDEA Software Institute
Media Attached File Attached
10:54
24m
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine Abate Inria Paris, Roberto Blanco Inria, Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Deepak Garg Max Planck Institute for Software Systems, Cătălin Hriţcu Inria Paris, Marco Patrignani Stanford University & CISPA , Éric Tanter University of Chile, Jérémy Thibault Inria Paris
Media Attached File Attached
11:18
24m
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan Bay Aarhus University, Aslan Askarov Aarhus University
Media Attached File Attached
11:42
24m
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis Larsen DIKU, University of Copenhagen, Torben Mogensen DIKU, University of Copenhagen, Michael Kirkedal Thomsen DIKU, University of Copenhagen
File Attached
12:06
24m
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine Blazy Univ Rennes- IRISA, Rémi Hutin IRISA / ENS Rennes, David Pichardie Univ Rennes, ENS Rennes, IRISA
Media Attached