Program

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  
Online user: 1 Privacy
Loading...