|
Wednesday, April 3, 2024
| 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 |
Thursday, April 4, 2024
| 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 |
Friday, April 5, 2024
| 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 |
|
|