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

Speculative execution attacks like Spectre can be used to violate confidentiality in all modern general-purpose CPUs. Recently, many compiler-level countermeasures have been proposed to mitigate the impact of Spectre-style attacks. However, the correctness and security of these countermeasures has not been ascertained yet. Even worse, while some of the existing countermeasures seem to be secure, others are known to be insecure and produce vulnerable programs.

In this paper we report on our ongoing effort towards formally reasoning about the effectiveness of these countermeasures. For this, we combine recent frameworks for reasoning about speculative information flows with a secure compilation theory telling that a compiler is secure when it preserves certain classes of (hyper)properties. We argue that Spectre-like attacks arise from violations of \emph{speculative non-interference}, a non-interference-like property. By lifting speculative non-interference to the secure compilation setting, we obtain a precise notion of security against Spectre-style attacks for compiler-level countermeasures. We believe that this criterion is the first step towards formally reasoning about the security of compiler-level countermeasures against Spectre-style attacks, and we discuss our research plan.

Exorcising Spectres with Secure Compilers (exorciseSpectre@prisc_pdf.pdf)9.10MiB

Sat 25 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

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
Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute
Media Attached File Attached
prisc-2020-papers10:54 - 11:18
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
Johan BayAarhus University, Aslan AskarovAarhus University
Media Attached File Attached
prisc-2020-papers11:42 - 12:06
Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
prisc-2020-papers12:06 - 12:30
Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA
Media Attached