Program

Week Wed. 03 Thu. 04 Fri. 05 List

	Wed. 03	Thu. 04	Fri. 05
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	Opening words 8:45 - 9:00 (15min) Opening words Keynote: Secure Compilation: Formal Foundations and (Some) Applications 9:00 - 10:00 (1h) Keynote: Secure Compilation: Formal Foundations and (Some) Applications Marco Patrignani Coffee break 10:00 - 10:30 (30min) Coffee break Protocol analysis 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) Lunch 12:10 - 14:00 (1h50) Lunch Program analysis 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) Coffee break 15:15 - 15:45 (30min) Coffee break Hardware and side-channel 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) Tool session 17:00 - 19:00 (2h) Tool session Dinner 19:30 - 21:00 (1h30) Dinner	Keynote: DY Fuzzing: Putting a Dolev-Yao attacker in the fuzzing loop 9:00 - 10:00 (1h) Keynote: DY Fuzzing: Putting a Dolev-Yao attacker in the fuzzing loop Steve Kremer Coffee break 10:00 - 10:30 (30min) Coffee break Formal methods and cryptography 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) Lunch 12:10 - 14:00 (1h50) Lunch Visite chateau d'Oléron 14:00 - 18:00 (4h) Visite chateau d'Oléron Cocktail 18:30 - 19:30 (1h) Cocktail Banquet 19:30 - 21:00 (1h30) Banquet	Keynote: Epistemic Verification of Information-Flow Properties in Programs 9:00 - 10:00 (1h) Keynote: Epistemic Verification of Information-Flow Properties in Programs Ioana Boureanu Coffee break 10:00 - 10:30 (30min) Coffee break E-voting 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) Trusted Execution Environment 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) Business meeting 12:10 - 12:30 (20min) Business meeting Lunch 12:30 - 14:00 (1h30) Lunch Symbolic execution 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) Coffee break 15:15 - 15:45 (30min) Coffee break Protocol analysis 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) Rump sessions 16:35 - 17:35 (1h) Rump sessions Dinner 19:30 - 21:00 (1h30) Dinner

Online user: 1

Privacy