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