|
Monday, March 21, 2022
| Time | Event | (+) |
| 07:45 - 08:45 | Breakfast | |
| 08:45 - 09:00 | Welcome - Sébastien Bardin et Jannik Dreier | |
| 09:00 - 10:00 | Keynote: Semantic preservation of constant-time policies during compilation - Sandrine Blazy | |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:30 | GT MFS - Protocol Verification 1 - Chair: Joseph Lallemand | (+) |
| 10:30 - 10:50 | › Systematic, automated discovery of security protocol attacks that exploit weaknesses in common hash functions - Charlie Jacomme, CISPA | |
| 10:50 - 11:10 | › A comprehensive security analysis of the Belenios protocol and more - Alexandre Debant, Inria Nancy - Grand Est | |
| 11:10 - 11:30 | › Formal analysis of LAKE-EDHOC - Maïwenn Racouchot, Racouchot - Elise Klein, Klein | |
| 11:30 - 11:50 | Break | |
| 11:50 - 12:30 | GT MFS - Cryptographic Implementations - Chair: Caroline Fontaine | (+) |
| 11:50 - 12:10 | › Formal Verification Challenges on High-Speed Cryptographic Implementations - Miguel Quaresma, MPI-SP - Tiago Oliveira, MPI-SP | |
| 12:10 - 12:30 | › A CompCert Backend with Symbolic Encryption - Paolo Torrini - INRIA | |
| 12:30 - 14:00 | Lunch | |
| 14:00 - 15:00 | Keynote: Symbolic execution by compiling symbolic handling into binaries with SymCC and SymQEMU - Aurélien Francillon | |
| 15:00 - 15:30 | Coffee break | |
| 15:30 - 16:30 | GT MFS - Static Analysis 1 - Chair: Michael Marcozzi | (+) |
| 15:30 - 15:50 | › Improving Static Analysis Precision by Minimal Program Refinement - Charles Babu M, Univ. Paris-Saclay, CEA, List, Saclay, France | |
| 15:50 - 16:10 | › Assessing bug replicability for more security-minded bug finding - Guillaume Girol, Laboratoire Sûreté des Logiciels | |
| 16:10 - 16:30 | › Efficient Symbolic Algorithms for Software Verification Against Fault Attacks - Soline Ducousso, Univ. Paris-Saclay, CEA, List, Saclay, France | |
| 16:30 - 17:00 | Break | |
| 17:00 - 18:00 | GT MFS - Program Verification 1 - Chair: Julien Signoles | (+) |
| 17:00 - 17:20 | › Verifying Low-Level, Concurrent Programs with Steel - Aymeric Fromherz, Inria | |
| 17:20 - 17:40 | › Model Checking of Vulnerabilities in SmartContracts: A Solidity-to-CPN Approach Extended Abstract | |
| 17:40 - 18:00 | › Verifying Redundant-Check Based Countermeasures: A Case Study - Thibault Martin, CEA LIST - Nikolai Kosmatov, Thales Research and Technology - Virgile Prevosto, CEA LIST | |
| 20:00 - 23:00 | Banquet |
Tuesday, March 22, 2022
| Time | Event | (+) |
| 07:45 - 09:30 | Breakfast | |
| 09:30 - 15:00 | Social Event: Guided discovery of the Esterel Massif by foot (and bus). Picknick on the beach at lunchtime. - Social Event: Guided discovery of the Esterel Massif by foot (and bus). Picknick on the beach at lunchtime. | |
| 16:00 - 17:00 | GT MFS - Static Analysis 2 - Chair: Nikolai Kosmatov | (+) |
| 16:00 - 16:20 | › Analyse de contre-mesures dans le cadre d'attaques multiples - Etienne Boespflug, VERIMAG | |
| 16:20 - 16:40 | › Stack smashing analysis by abstract interpretation of binary code - Julien Forget, Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires | |
| 16:40 - 17:00 | › Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks - Francesco Parolini, Sorbonne University | |
| 17:00 - 17:30 | Coffee break | |
| 17:30 - 18:10 | GT MFS - Network Security - Chair: Marie-Laure Potet | (+) |
| 17:30 - 17:50 | › Learning and Knowledge for Anomaly Detection - Yannick Chevalier, IRIT | |
| 17:50 - 18:10 | › Formal analysis of security issues in dynamic virtual networks - Pierre Le Scornet, Université de Rennes 1 | |
| 18:45 - 19:45 | Tools Session | |
| 20:00 - 22:00 | Dinner |
Wednesday, March 23, 2022
| Time | Event | (+) |
| 07:45 - 09:00 | Breakfast | |
| 09:00 - 10:00 | Keynote: The security protocol verifier ProVerif and its major recent improvements - Bruno Blanchet | |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:30 | GT MFS - Constant Time - Chair: Adrien Koutsos | (+) |
| 10:30 - 10:50 | › Type-Directed Program Transformation for Constant-Time Enforcement - Gautier Raimondi, CELTIQUE | |
| 10:50 - 11:10 | › Structured Leakage and Applications to Cryptographic Constant-Time and Cost - Swarn Priya - Université Côte d'Azur, Inria Sophia Antipolis | |
| 11:10 - 11:30 | › End-to-end enforcement of fine-grained "cryptographic" constant-time policies - Basavesh Ammanaghatta Shivakumar - MPI-SP | |
| 11:30 - 11:50 | Break | |
| 11:50 - 12:30 | GT MFS - Protocol Verification 2 - Chair: Yannick Chevalier | (+) |
| 11:50 - 12:10 | › Vérification des mécanismes de sécurité des navigateurs Web - Benjamin Farinier, Sec&Priv, TU Wien | |
| 12:10 - 12:30 | › Equational Proofs for Distributed Cryptographic Protocols - Kristina Sojakova, Inria Paris | |
| 12:30 - 14:00 | Lunch | |
| 15:30 - 16:00 | Business Meeting | |
| 16:00 - 16:30 | Coffee break | |
| 16:30 - 17:30 | GT MFS - Computational Verification - Chair: Steve Kremer | (+) |
| 16:30 - 16:50 | › Mechanized Proofs of Adversarial Complexity and Application to Universal Composability - Adrien Koutsos, Programming securely with cryptography | |
| 16:50 - 17:10 | › A Formalization of the Proof of Correctness of a Number-Theoretic Transform in the Context of the Hakyber Cryptographic Primitive - Antoine Séré, Institut Polytechnique de Paris | |
| 17:10 - 17:30 | › CV2EC: Getting the Best of Two Worlds - Benjamin Grégoire, Inria Sophia Antipolis, Université Côte d'Azur | |
| 17:30 - 18:00 | Break | |
| 18:00 - 18:40 | GT MFS - Program Verification 2 - Chair: Laurent Mounier | (+) |
| 18:00 - 18:20 | › A General Framework for Supervisory Control of Opacity - Nour Souid, LIPN | |
| 18:20 - 18:40 | › Support for Detecting Integer Overflow Vulnerability - Salim Yahia Kissi, Kissi | |
| 19:00 - 20:00 | Rump Session | |
| 20:00 - 22:00 | Dinner |
|
|