Journées 2022 du GT "Méthodes Formelles pour la Sécurité", GdR Sécurité Informatique

Breakfast

Welcome

Sébastien Bardin et Jannik Dreier

Keynote: Semantic preservation of constant-time policies during compilation

Sandrine Blazy

Coffee break

GT MFS

Protocol Verification 1 - Chair: Joseph Lallemand

› Systematic, automated discovery of security protocol attacks that exploit weaknesses in common hash functions - Charlie Jacomme, CISPA 10:30-10:50 (20min)

› A comprehensive security analysis of the Belenios protocol and more - Alexandre Debant, Inria Nancy - Grand Est 10:50-11:10 (20min)

› Formal analysis of LAKE-EDHOC - Maïwenn Racouchot, Racouchot - Elise Klein, Klein 11:10-11:30 (20min)

Break

GT MFS

Cryptographic Implementations - Chair: Caroline Fontaine

› Formal Verification Challenges on High-Speed Cryptographic Implementations - Miguel Quaresma, MPI-SP - Tiago Oliveira, MPI-SP 11:50-12:10 (20min)

› A CompCert Backend with Symbolic Encryption - 12:10-12:30 (20min)

Lunch

Keynote: Symbolic execution by compiling symbolic handling into binaries with SymCC and SymQEMU

Aurélien Francillon

Coffee break

GT MFS

Static Analysis 1 - Chair: Michael Marcozzi

› Improving Static Analysis Precision by Minimal Program Refinement - Charles Babu M, Univ. Paris-Saclay, CEA, List, Saclay, France 15:30-15:50 (20min)

› Assessing bug replicability for more security-minded bug finding - Guillaume Girol, Laboratoire Sûreté des Logiciels 15:50-16:10 (20min)

› Efficient Symbolic Algorithms for Software Verification Against Fault Attacks - Soline Ducousso, Univ. Paris-Saclay, CEA, List, Saclay, France 16:10-16:30 (20min)

Break

GT MFS

Program Verification 1 - Chair: Julien Signoles

› Verifying Low-Level, Concurrent Programs with Steel - Aymeric Fromherz, Inria 17:00-17:20 (20min)

› Model Checking of Vulnerabilities in SmartContracts: A Solidity-to-CPN Approach Extended Abstract - 17:20-17:40 (20min)

› Verifying Redundant-Check Based Countermeasures: A Case Study - Thibault Martin, CEA LIST - Nikolai Kosmatov, Thales Research and Technology - Virgile Prevosto, CEA LIST 17:40-18:00 (20min)

Banquet