Program
| 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 |
|
| 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 |
|
|
Loading...