08:00
09:00
10:00
11:00
12:00
13:00
14:00
15:00
16:00
17:00
18:00
19:00
20:00
21:00
›8:45 (15min)
8:45 - 9:00 (15min)
Opening words
›9:00 (1h)
9:00 - 10:00 (1h)
Keynote: Secure Compilation: Formal Foundations and (Some) Applications
Marco Patrignani
›10:00 (30min)
10:00 - 10:30 (30min)
Coffee break
›10:30 (1h40)
10:30 - 12:10 (1h40)
Protocol analysis
Alexandre Debant (session chair)
› Formal analysis of WideVine DRM in Tamarin
- Joseph Lallemand, Irisa, CNRS, Univ Rennes
10:30-10:55 (25min)
› A Unified Symbolic Analysis of WireGuard
- Dhekra Mahmoud, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes
10:55-11:20 (25min)
› Formal verification of the Lightning Network protocol
- Léo Louistisserand, Université de Lorraine, CNRS, Inria, LORIA
11:20-11:45 (25min)
› Formal verification of the ETSI proposal on a standard QKD protocol
- Thomas Prévost, Modèles Discrets pour les Systèmes Complexes, Signal, Images et Systèmes
11:45-12:10 (25min)
›12:10 (1h50)
12:10 - 14:00 (1h50)
Lunch
›14:00 (1h15)
14:00 - 15:15 (1h15)
Program analysis
Julien Signoles (session chair)
› Black-box Precondition Inference through Constraint Acquisition
- Grégoire Menguy, Direction de Recherche Technologique (CEA)
14:00-14:25 (25min)
› Precise and efficient memory analysis for low level languages
- Julien Simonnet, CEA- Saclay
14:25-14:50 (25min)
› Extended abstract: Systematic Evaluation of Automated Tools for Side-Channel Vulnerability Detection in Cryptographic Libraries
- Antoine Geimer, Univ Rennes, Univ Lille, CNRS, Inria
14:50-15:15 (25min)
›15:15 (30min)
15:15 - 15:45 (30min)
Coffee break
›15:45 (1h15)
15:45 - 17:00 (1h15)
Hardware and side-channel
Sébastien Bardin (session chair)
› On Kernel Safety and Speculative Execution
- Davide Davoli, Université Côte d'Azur, Inria
15:45-16:10 (25min)
› Proving Hardware Security of CPUs to Analyze Software Resistance against Faults Attacks
- Simon Tollec, Université Paris-Saclay, CEA, List
16:10-16:35 (25min)
› Formalizing Hardware Security Mechanisms Using SMT Solvers
- Pierre WILKE, CentraleSupelec
16:35-17:00 (25min)
›17:00 (2h)
17:00 - 19:00 (2h)
Tool session
›19:30 (1h30)
19:30 - 21:00 (1h30)
Dinner
