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 - 9:00 (15min)
Opening words
9:00 - 10:00 (1h)
Keynote: Secure Compilation: Formal Foundations and (Some) Applications
Marco Patrignani
10:00 - 10:30 (30min)
Coffee break
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 - 14:00 (1h50)
Lunch
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 - 15:45 (30min)
Coffee break
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 - 19:00 (2h)
Tool session
19:30 - 21:00 (1h30)
Dinner
9:00 - 10:00 (1h)
Keynote: DY Fuzzing: Putting a Dolev-Yao attacker in the fuzzing loop
Steve Kremer
10:00 - 10:30 (30min)
Coffee break
10:30 - 12:10 (1h40)
Formal methods and cryptography
Charlie Jacomme (session chair)
› Proving e-voting mixnets in the CCSA model: zero-knowledge proofs and rewinding
- Margot Catinaud, Laboratoire Méthodes Formelles
10:30-10:55 (25min)
› A Probabilistic Logic for Concrete Security
- Théo Vignon, Laboratoire Méthodes Formelles
10:55-11:20 (25min)
› Secrecy by typing in the computational model
- Clément Hérouard, Institut de Recherche en Informatique et Systèmes Aléatoires
11:20-11:45 (25min)
› Verification of security protocols : using SMT solvers in the Squirrel prover
- Stanislas Riou, Université de Rennes
11:45-12:10 (25min)
12:10 - 14:00 (1h50)
Lunch
14:00 - 18:00 (4h)
Visite chateau d'Oléron
18:30 - 19:30 (1h)
Cocktail
19:30 - 21:00 (1h30)
Banquet
9:00 - 10:00 (1h)
Keynote: Epistemic Verification of Information-Flow Properties in Programs
Ioana Boureanu
10:00 - 10:30 (30min)
Coffee break
10:30 - 11:20 (50min)
E-voting
Joseph Lallemand (session chair)
› Election Verifiability with ProVerif
- Véronique Cortier, CNRS, Loria
10:30-10:55 (25min)
› ProVerif Proofs over an Internet Voting System using Short Voting Codes
- Moser Florian, Inria Nancy - Grand Est
10:55-11:20 (25min)
11:20 - 12:10 (50min)
Trusted Execution Environment
Guillaume Scerri (session chair)
› A UC analysis of Android Protected Confirmation
- Maïwenn Racouchot, Inria
11:20-11:45 (25min)
› Practical Replay Attack on Intel's RA-TLS: A Formal Proof of Insecurity
- Muhammad Usama Sardar, TU Dresden
11:45-12:10 (25min)
12:10 - 12:30 (20min)
Business meeting
12:30 - 14:00 (1h30)
Lunch
14:00 - 15:15 (1h15)
Symbolic execution
Grégoire Menguy (session chair)
› Boosting the BINSEC symbolic execution engine: A France CyberSecurity Challenge journey
- Frédéric Recoules, CEA LIST
14:00-14:25 (25min)
› Attacker Control and Bug Prioritization
- Guilhem Lacombe, CEA LIST, Université Paris-Saclay
14:25-14:50 (25min)
› Inference of Robust Reachability Constraints
- Yanis Sellami, Laboratoire Sûreté des Logiciels
14:50-15:15 (25min)
15:15 - 15:45 (30min)
Coffee break
15:45 - 16:35 (50min)
Protocol analysis
Bruno Blanchet (session chair)
› Towards nonce-misuse resistant protocols
- Tristan Claverie, ANSSI, Institut National des Sciences Appliquées - Rennes, SYSTÈMES LARGE ÉCHELLE
15:45-16:10 (25min)
› Simulation multi-agent d'attaques sur protocoles distribués
- Erwan Mahe, CEA-LIST
16:10-16:35 (25min)
16:35 - 17:35 (1h)
Rump sessions
19:30 - 21:00 (1h30)
Dinner
