Write a Blog >>
Sat 25 Jan 2020 12:06 - 12:30 at Rosalie - Foundations and timing channels Chair(s): Marco Vassena

Formally verified compilers guarantee the absence of correctness bugs introduced during the compilation, but do not deal with other type of bugs, such as security bugs. In our previous work, we addressed the challenge of turning CompCert, a formally verified compiler, into a formally verified secure compiler. The notion of security we focused on is the preservation of “cryptographic constant-time”, a popular side-channel protection against timing-based and cache-based attacks. However, proving that CompCert is secure with respect to this property first required to modify several parts of the compiler. This extended abstract will focus on the changes we made to the CompCert compiler.

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 12:30: Foundations and timing channelsPriSC at Rosalie
Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security
10:30 - 10:54
Talk
Exorcising Spectres with Secure Compilers
PriSC
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
10:54 - 11:18
Talk
Trace-Relating Compiler Correctness and Secure Compilation
PriSC
Carmine AbateInria Paris, Roberto BlancoInria, Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniStanford University & CISPA , Éric TanterUniversity of Chile, Jérémy ThibaultInria Paris
Media Attached File Attached
11:18 - 11:42
Talk
Reconciling progress-insensitive noninterference and declassification
PriSC
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
11:42 - 12:06
Talk
Hermes: Implementing Cryptography without Side-channels
PriSC
Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
12:06 - 12:30
Talk
A CompCert Compiler that Preserves Cryptographic Constant-time
PriSC
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA
Media Attached