Comparse: Provably Secure Formats for Cryptographic Protocols
ACM CCS 2023.
[doi]
[eprint]
TreeSync: Authenticated Group Management for Messaging Layer Security
USENIX Security '23.
[USENIX]
[eprint]
This paper won the Internet Defense Prize and received a Distinguished Paper Award.
The Messaging Layer Security (MLS) Protocol
IETF RFC (contributor).
[datatracker]
[rfc]
I am an active participant in the IETF MLS working group, where I authored several key improvements such as the disambiguation of signatures and the strengthening of group membership agreement.
Co-winner of the 2023 Internet Defense Prize.
Distinguished Paper Award at USENIX Security ‘23.
POPL 2024 (sub-reviewer)
ESOP 2023 (Artifact Evaluation Committee)
Systèmes numériques at ENS Paris (Sept. 2023 - Jan 2024)
Systèmes numériques at ENS Paris (Sept. 2022 - Jan 2023)
Systèmes numériques at ENS Paris (Sept. 2021 - Jan 2022)
Comparse: Provably Secure Formats for Cryptographic Protocols
at ACM CCS 2023.
[slides]
This is the 12-minutes talk for the paper “Comparse: Provably Secure Formats for Cryptographic Protocols”, given at ACM CCS 2023.
"Don't roll your own crypto": les méthodes formelles au service de la sécurité
at Devfest Toulouse (in french).
[recording]
[slides]
I gave a short talk at Devfest Toulouse 2019, giving a brief overview of what formal methods can be used for (aimed at developers who never heard of this).
End-to-End Encrypted Group Chats with MLS: Design, Implementation and Verification
at Microsoft Research (08/2023) ; Cornell Tech (08/2023) ; IRISA (01/2024) ; NYU (03/2024) ; MIT (04/2024).
[slides]
[slides v2]
This is the long version (45 to 60 minutes) of the talk for the paper “TreeSync: Authenticated Group Management for Messaging Layer Security”, given at various places.
The second version of the slides include a digression on the paper “Comparse: Provably Secure Formats for Cryptographic Protocols”, to explain more deeply what happened behind the signature ambiguity attack.
TreeSync: Authenticated Group Management for Messaging Layer Security
at USENIX Security '23.
[slides]
This is the 12-minutes talk for the paper “TreeSync: Authenticated Group Management for Messaging Layer Security”, given at USENIX Security ‘23.
Applications de Brainfuck, langage minimaliste mais Turing-complet
at Devfest Toulouse (in french).
[recording]
[slides]
I gave a short talk at Devfest Toulouse 2019, explaining how it was humanly possible to write useful Brainfuck programs. After explaining the syntax of the language, I explained some useful code patterns such as conditions or array management, which allow to write complex programs.
Des tuyaux pour se qualifier au baseball
at Informatique pour Tous (in french).
[recording]
[slides]
I gave a talk that was aimed to explain a computer science notion for high-school student. I decided to explain the max-flow min-cut theorem and the Ford-Fulkerson algorithm, applied on a problem of deciding whether a baseball team can still qualify or not. I definitely lacked a lot of presentation skills (you can count the “euuuuh”), however I think I found the simplest explanations for the max-flow alogrithm.
A verification framework for secure machine learning
Internship for 2nd year of Master's Degree at INRIA, Paris.
With
[PDF]
[slides]
I worked five months in the Prosecco team at INRIA. I wrote a global and local specifications for the online phase of the SPDZ2k protocol, and proved that they computed the same thing.
Faster CakeML compilation with a verified linear scan register allocator
Internship for 1st year of Master's Degree at Chalmers, Göteborg (Sweden).
With
[PDF]
[slides]
I worked five months in the CakeML team to implement a verified linear-scan register allocator. The motivation was that the register allocation was the slowest part of the compilation process, hence a faster algorithm could drastically reduce compilation time.
Détection automatique des adresses exploitables d'un algorithme de cryptographie par timing du cache processeur
Internship for 3rd year of Bachelor's Degree at Secure-IC, Paris.
With
[PDF]
[slides]
I worked two months on cache timing attacks (before Spectre or Meltdown were known). I found a procedure to analyse a cryptographic library and automatically find parts of the code which break secret independance, and might leak a private key to an attacker running on the same computer.