GT MFS 2023 - Sciencesconf.org

Welcome

Charlie Jacomme & Joseph Lallemand

Keynote: JavaScript security: fake or real? (Can formal methods help us decide?)

Tamara Rezk

Coffee break

Program Verification

chair: Benjamin Farinier

› Adversarial Reachability for Program-level Security Analysis - Soline Ducousso, Univ. Paris-Saclay, CEA, List, Saclay, France 10:30-10:55 (25min)

› A theory of injection-based vulnerabilities in formal grammars - Pierre-Francois Gimenez, Institut de Recherche en Informatique et Systèmes Aléatoires 10:55-11:20 (25min)

Break

Protocol Analysis

chair: Itsaka Rakotonirina

› A systematic study of Bluetooth key agreements with Tamarin - Tristan Claverie, ANSSI 11:40-12:05 (25min)

› Formal analysis of security for the protocol OPC-UA v1.05 - Vincent DIEMUNSCH, Inria à Nancy 12:05-12:30 (25min)

Lunch

Real Time

chair: Jannik Dreier

› Extending ASTD with real time - Diego Oliveira, Université de Sherbrooke 14:15-14:40 (25min)

› 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] 14:40-15:05 (25min)

Logic for Security

chair: Bruno Blanchet

› Expressing and Verifying Privacy with Epistemic Logic - Fortunat Rajaona, University of Surrey 15:05-15:30 (25min)

› A Higher-Order Indistinguishability Logic for Cryptographic Reasoning - David Baelde, Irisa, CNRS, Univ Rennes 15:30-15:55 (25min)

› Max#SAT and adaptive attacker synthesis - Thomas Vigouroux, VERIMAG 15:55-16:20 (25min)

Coffee break

Constant time

chair: Pierre Wilke

› Constant Time Security at a Low Cost for Embedded Systems Through Hardware/Software Cooperation - Jean-Loup Hatchikian-Houdot, Inria, Univ Rennes, CNRS, IRISA 16:50-17:15 (25min)

› Provably Secure Speculation for the Constant-Time Policy - Lesly-Ann Daniel, imec-DistriNet, KU Leuven 17:15-17:40 (25min)

Rump Session

Dinner