POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This program is tentative and subject to change.

Sun 11 Jan 2026 16:36 - 16:54 at Salle 19 - Hardware Security Chair(s): Jérémy Thibault

Fault injections are physical attacks that disrupt systems’ hardware to create exploitable erroneous behaviors. Countermeasures that rely on software (exclusively or not) frequently need much more precise control of the binary code than available through high-level languages’ semantics. This causes significant friction when compiling, as lowerings and optimizations only obey semantics and often destroy security code or annotations.

As a step to address this issue, we introduce Tracing LLVM, an open-source extension of LLVM with primitives to protect and compile non-functional aspects of programs (backed mostly by implementation-defined behavior and internal LLVM API contracts). We showcase its current capabilities by protecting typical countermeasures, lowering source information to late stages, and composing four protection schemes on a PIN verification function.

Slides (prisc26-tracing-llvm.pdf)1021KiB

This program is tentative and subject to change.

Sun 11 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:00 - 17:30
Hardware SecurityPriSC at Salle 19
Chair(s): Jérémy Thibault EPFL
16:00
18m
Talk
FSLH: Flexible Mechanized Speculative Load Hardening
PriSC
Jonathan Baumann MPI-SP, Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Léon Ducruet Aarhus University, Sebastian Harwig MPI-SP and Ruhr University Bochum, Cătălin Hriţcu MPI-SP
16:18
18m
Talk
Towards Robust Secure Compilation in Presence of Speculative Execution
PriSC
Léopold Clément Télécom Paris, Ulrich Kühne Télécom Paris, Florian Brandner Télécom Paris, Renaud Pacalet Télécom Paris
16:36
18m
Talk
Compiling countermeasures against fault attacks with “Tracing LLVM”
PriSC
Sébastien Michelland Université Grenoble-Alpes - Grenoble INP - LCIS, Christophe Deleuze Université Grenoble-Alpes - Grenoble INP - LCIS, Laure Gonnord Université Grenoble-Alpes - Grenoble INP - LCIS
File Attached
16:54
18m
Talk
Modular and automatic formal verification of a RISC-V processor with security mechanisms
PriSC
Pierre Wilke CentraleSupélec, Cyprien Jules CentraleSupélec, Inria, CNRS, Univ. Rennes, Guillaume Hiet CentraleSupélec, Inria, CNRS, Univ. Rennes
17:12
18m
Talk
Fun with flags: How Compilers Break and Fix Constant-Time Code
PriSC
Antoine Geimer Univ. Lille, CNRS, Inria, Clémentine Maurice Univ. Lille, Inria, CNRS
Hide past events