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

prisc-2020-papers
10:30 - 12:30: Principles of Secure Compilation 2020 - Foundations and timing channels at Rosalie
Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security
prisc-2020-papers10:30 - 10:54
Talk
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
prisc-2020-papers10:54 - 11:18
Talk
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
prisc-2020-papers11:18 - 11:42
Talk
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
prisc-2020-papers11:42 - 12:06
Talk
Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
prisc-2020-papers12:06 - 12:30
Talk
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA
Media Attached