|
Tuesday, March 28, 2023
| Time | Event | (+) |
| 08:45 - 09:00 | Welcome - Charlie Jacomme & Joseph Lallemand | |
| 09:00 - 10:00 | Keynote: JavaScript security: fake or real? (Can formal methods help us decide?) - Tamara Rezk | |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:20 | Program Verification - chair: Benjamin Farinier | (+) |
| 10:30 - 10:55 | › Adversarial Reachability for Program-level Security Analysis - Soline Ducousso, Univ. Paris-Saclay, CEA, List, Saclay, France | |
| 10:55 - 11:20 | › A theory of injection-based vulnerabilities in formal grammars - Pierre-Francois Gimenez, Institut de Recherche en Informatique et Systèmes Aléatoires | |
| 11:20 - 11:40 | Break | |
| 11:40 - 12:30 | Protocol Analysis - chair: Itsaka Rakotonirina | (+) |
| 11:40 - 12:05 | › A systematic study of Bluetooth key agreements with Tamarin - Tristan Claverie, ANSSI | |
| 12:05 - 12:30 | › Formal analysis of security for the protocol OPC-UA v1.05 - Vincent DIEMUNSCH, Inria à Nancy | |
| 13:00 - 14:00 | Lunch | |
| 14:15 - 15:05 | Real Time - chair: Jannik Dreier | (+) |
| 14:15 - 14:40 | › Extending ASTD with real time - Diego Oliveira, Université de Sherbrooke | |
| 14:40 - 15:05 | › Security Going Live: on the Verification of Real-Time Components of Security Protocols (ongoing work) - Itsaka Rakotonirina, Max Planck Institute for Security and Privacy [Bochum] | |
| 15:05 - 16:20 | Logic for Security - chair: Bruno Blanchet | (+) |
| 15:05 - 15:30 | › Expressing and Verifying Privacy with Epistemic Logic - Fortunat Rajaona, University of Surrey | |
| 15:30 - 15:55 | › A Higher-Order Indistinguishability Logic for Cryptographic Reasoning - David Baelde, Irisa, CNRS, Univ Rennes | |
| 15:55 - 16:20 | › Max#SAT and adaptive attacker synthesis - Thomas Vigouroux, VERIMAG | |
| 16:20 - 16:50 | Coffee break | |
| 16:50 - 17:40 | Constant time - chair: Pierre Wilke | (+) |
| 16:50 - 17:15 | › Constant Time Security at a Low Cost for Embedded Systems Through Hardware/Software Cooperation - Jean-Loup Hatchikian-Houdot, Inria, Univ Rennes, CNRS, IRISA | |
| 17:15 - 17:40 | › Provably Secure Speculation for the Constant-Time Policy - Lesly-Ann Daniel, imec-DistriNet, KU Leuven | |
| 17:40 - 18:30 | Rump Session | |
| 19:30 - 21:00 | Dinner |
Wednesday, March 29, 2023
| Time | Event | (+) |
| 09:00 - 10:00 | Keynote - Symbolic verification of security protocols: modelling and verifying unlinkability - Stéphanie Delaune | |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:45 | Hardware - chair: David Monniaux | (+) |
| 10:30 - 10:55 | › Analysis of Fault Effects on Formal RISC-V Microarchitecture Models - Simon Tollec, CEA | |
| 10:55 - 11:20 | › Formalisation of hardware security mechanisms - Pierre WILKE, CentraleSupélec, Inria, Univ Rennes, CNRS IRISA, Rennes, France | |
| 11:20 - 11:45 | › SoK: Attestation in Confidential Computing - Muhammad Usama Sardar, TU Dresden | |
| 11:45 - 12:30 | Business Meeting | |
| 12:45 - 13:45 | Lunch | |
| 14:00 - 18:00 | Boat Tour - We will explore Morlaix's bay, followed by a free time on Ile de Batz. | |
| 19:30 - 21:00 | Dinner -- Banquet was moved to Thursday |
Thursday, March 30, 2023
| Time | Event | (+) |
| 09:00 - 10:00 | Keynote - Formally verified compilation, security and faults - David Monniaux | |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:45 | Tools for Protocol Analysis - chair: Guillaume Scerri | (+) |
| 10:30 - 10:55 | › Enhancing Automation in Tamarin - Maïwenn Racouchot, Loria, Inria Nancy | |
| 10:55 - 11:20 | › Systematic translation of Cryptographic Axioms by Bi-deduction - Justine Sauvage, Inria de Paris | |
| 11:20 - 11:45 | › Unrestricting restrictions in ProVerif - Vincent Cheval, Inria Paris, Prosecco | |
| 13:00 - 14:00 | Lunch | |
| 14:15 - 15:05 | Protocol Analysis - chair: Alexandre Debant | (+) |
| 14:15 - 14:40 | › Conception et vérification d'un protocole de vote par correspondance - Léo Louistisserand, Ecole Normale Supérieure Paris-Saclay | |
| 14:40 - 15:05 | › Attacking and Fixing Protocols using Exponentiation Mix-Net Automatically with Refined Models - Dhekra Mahmoud, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes - Jannik Dreier, Proof techniques for security protocols - Pascal Lafourcade, Laboratoire dÍnformatique, de Modélisation et dÓptimisation des Systèmes | |
| 15:05 - 15:55 | Program Verification - chair: Frédéric Besson | (+) |
| 15:05 - 15:30 | › Quantization for opaque predicate location. - Alexandre Gonzalvez, Institut de Recherche en Informatique et Systèmes Aléatoires | |
| 15:30 - 15:55 | › StarMalloc: A Modern, Security-Oriented Verified Memory Allocator - Antonin Reitz, Inria Paris | |
| 15:55 - 16:25 | Coffee break | |
| 16:25 - 18:00 | Tool Session | |
| 19:00 - 21:00 | Banquet -- moved from Wednesday |
|
|