Program
| Time |
Event |
(+)
|
|
08:45 - 09:00
|
Opening words |
|
|
09:00 - 10:00
|
Keynote: Secure Compilation: Formal Foundations and (Some) Applications - Marco Patrignani |
|
|
10:00 - 10:30
|
Coffee break |
|
|
10:30 - 12:10
|
Protocol analysis - Alexandre Debant (session chair) |
(+)
|
|
10:30 - 10:55 |
› Formal analysis of WideVine DRM in Tamarin - Joseph Lallemand, Irisa, CNRS, Univ Rennes |
|
|
10:55 - 11:20 |
› A Unified Symbolic Analysis of WireGuard - Dhekra Mahmoud, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes |
|
|
11:20 - 11:45 |
› Formal verification of the Lightning Network protocol - Léo Louistisserand, Université de Lorraine, CNRS, Inria, LORIA |
|
|
11:45 - 12:10 |
› 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 |
|
|
12:10 - 14:00
|
Lunch |
|
|
14:00 - 15:15
|
Program analysis - Julien Signoles (session chair) |
(+)
|
|
14:00 - 14:25 |
› Black-box Precondition Inference through Constraint Acquisition - Grégoire Menguy, Direction de Recherche Technologique (CEA) |
|
|
14:25 - 14:50 |
› Precise and efficient memory analysis for low level languages - Julien Simonnet, CEA- Saclay |
|
|
14:50 - 15:15 |
› Extended abstract: Systematic Evaluation of Automated Tools for Side-Channel Vulnerability Detection in Cryptographic Libraries - Antoine Geimer, Univ Rennes, Univ Lille, CNRS, Inria |
|
|
15:15 - 15:45
|
Coffee break |
|
|
15:45 - 17:00
|
Hardware and side-channel - Sébastien Bardin (session chair) |
(+)
|
|
15:45 - 16:10 |
› On Kernel Safety and Speculative Execution - Davide Davoli, Université Côte d'Azur, Inria |
|
|
16:10 - 16:35 |
› Proving Hardware Security of CPUs to Analyze Software Resistance against Faults Attacks - Simon Tollec, Université Paris-Saclay, CEA, List |
|
|
16:35 - 17:00 |
› Formalizing Hardware Security Mechanisms Using SMT Solvers - Pierre WILKE, CentraleSupelec |
|
|
17:00 - 19:00
|
Tool session |
|
|
19:30 - 21:00
|
Dinner |
|
| Time |
Event |
(+)
|
|
09:00 - 10:00
|
Keynote: DY Fuzzing: Putting a Dolev-Yao attacker in the fuzzing loop - Steve Kremer |
|
|
10:00 - 10:30
|
Coffee break |
|
|
10:30 - 12:10
|
Formal methods and cryptography - Charlie Jacomme (session chair) |
(+)
|
|
10:30 - 10:55 |
› Proving e-voting mixnets in the CCSA model: zero-knowledge proofs and rewinding - Margot Catinaud, Laboratoire Méthodes Formelles |
|
|
10:55 - 11:20 |
› A Probabilistic Logic for Concrete Security - Théo Vignon, Laboratoire Méthodes Formelles |
|
|
11:20 - 11:45 |
› Secrecy by typing in the computational model - Clément Hérouard, Institut de Recherche en Informatique et Systèmes Aléatoires |
|
|
11:45 - 12:10 |
› Verification of security protocols : using SMT solvers in the Squirrel prover - Stanislas Riou, Université de Rennes |
|
|
12:10 - 14:00
|
Lunch |
|
|
14:00 - 18:00
|
Visite chateau d'Oléron |
|
|
18:30 - 19:30
|
Cocktail |
|
|
19:30 - 21:00
|
Banquet |
|
| Time |
Event |
(+)
|
|
09:00 - 10:00
|
Keynote: Epistemic Verification of Information-Flow Properties in Programs - Ioana Boureanu |
|
|
10:00 - 10:30
|
Coffee break |
|
|
10:30 - 11:20
|
E-voting - Joseph Lallemand (session chair) |
(+)
|
|
10:30 - 10:55 |
› Election Verifiability with ProVerif - Véronique Cortier, CNRS, Loria |
|
|
10:55 - 11:20 |
› ProVerif Proofs over an Internet Voting System using Short Voting Codes - Moser Florian, Inria Nancy - Grand Est |
|
|
11:20 - 12:10
|
Trusted Execution Environment - Guillaume Scerri (session chair) |
(+)
|
|
11:20 - 11:45 |
› A UC analysis of Android Protected Confirmation - Maïwenn Racouchot, Inria |
|
|
11:45 - 12:10 |
› Practical Replay Attack on Intel's RA-TLS: A Formal Proof of Insecurity - Muhammad Usama Sardar, TU Dresden |
|
|
12:10 - 12:30
|
Business meeting |
|
|
12:30 - 14:00
|
Lunch |
|
|
14:00 - 15:15
|
Symbolic execution - Grégoire Menguy (session chair) |
(+)
|
|
14:00 - 14:25 |
› Boosting the BINSEC symbolic execution engine: A France CyberSecurity Challenge journey - Frédéric Recoules, CEA LIST |
|
|
14:25 - 14:50 |
› Attacker Control and Bug Prioritization - Guilhem Lacombe, CEA LIST, Université Paris-Saclay |
|
|
14:50 - 15:15 |
› Inference of Robust Reachability Constraints - Yanis Sellami, Laboratoire Sûreté des Logiciels |
|
|
15:15 - 15:45
|
Coffee break |
|
|
15:45 - 16:35
|
Protocol analysis - Bruno Blanchet (session chair) |
(+)
|
|
15:45 - 16:10 |
› Towards nonce-misuse resistant protocols - Tristan Claverie, ANSSI, Institut National des Sciences Appliquées - Rennes, SYSTÈMES LARGE ÉCHELLE |
|
|
16:10 - 16:35 |
› Simulation multi-agent d'attaques sur protocoles distribués - Erwan Mahe, CEA-LIST |
|
|
16:35 - 17:35
|
Rump sessions |
|
|
19:30 - 21:00
|
Dinner |
|
|
