I am a researcher at Inria and LORIA, member of the PESTO team.
My research interests mainly focus on formal methods for security and privacy. I design new verification techniques, algorithms and tools to effectively and efficiently analyze formal security properties. I generally enjoy research projects that combine both foundational contributions and practical applications, including analyzing real-world cryptographic protocols. More recently, I also took a great interest in fuzz testing techniques.
I did my PhD at Ecole Normale Supérieure de Cachan jointly advised by Stéphanie Delaune and David Baelde and a postdoc at ETH Zürich in the David Basin’s Information Security Group.
Download my CV (PDF)
New paper accepted at Security & Privacy'24 where we propose a new fuzzing technique we called Dolev-Yao model-guided Fuzzing. We provide a full-fledged implementation of such a DY fuzzer in Rust with our tool tlspuffin, which found four new CVEs on WolfSSL, including one critical and two high CVEs.
New paper accepted at Usenix'23 and presented at Real World Crypto (contributed talk) on the e-voting protocol used during the 2022 French legislative election, which was the largest ever political election using e-voting in the world. We reversed the protocol, found 6 verifiability and privacy attacks on the protocol, and proposed fixes, some of them have been already deployed. We also presented this work at Real World Crypto'23. Media coverage: here, there, and there.
My ProtoFuzz project (2023-2027) was funded by the ANR (280k euros) as a JCJC project (individual research projects coordinated by young researchers). I am looking for students (research interns, PhD students), postdocs, and engineers to join this research effort. In case you are interested, contact me via email.
Preprint PDF DOI Black-Hat USA'17 talk Media coverage Video of PoC Models
I serve in the program committee of European Symposium on Research in Computer Security (ESORICS) (2024–now) and of the HotSpot workshop (yearly work-shop since 2015, affiliated with IEEE European Symposium on Security and Privacy) (2021–now). I have previously served in the program committee of ACM ASIACCS symposium (2023) and of the Computer Security track at the 29th ACM Symposium on Applied Computing (SEC@SAC) (2019-2022).
I have been external scientific experts for the ANR (French National Agency for Research) Generic Call 2019-2020. I have reviewed papers for CCS, CSF, Euro S&P, ESORICS, ACM TOPS, JCS, etc.
I am the PI of the ProtoFuzz project (2023-2027) funded by ANR JCJ (280k euros). I am or was a member of the France 2030 ANR PEPR Cybersécurité (SVP) (2022-2026) and ANR Chair IA ASAP project (2020-2024), joint project between Huawei Technologies Singapore Research Center and ETH Zürich on 5G protocols (2018-2019). I have participated to the following projects: ANR Chair of research and teaching in artificial intelligence (ASAP), ERC Consolidator Grant SPOOC, ERC Starting Grant POPSTAR, various ANR projects.
We developed with Max Ammann (main developer, security engineer at Trail of Bits), Tom Gouville (PhD student), and Michael Mera (research engineer) a fuzzer implementing a novel model-guided kind of fuzzer. The novel idea is to use the security-related domain-specific Dolev-Yao formal model to guide the fuzzer towards finding logical attacks in security protocols. Research conducted with M. Ammann and S. Kremer.
Porridge is a standalone OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols. It is not restricted to the limited class of action-deterministic protocols as in prior works. It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups. Theory and practical results are described in our ESORICS’18 paper.
UKano is a tool that enables the automatic formal verification of unlinkability and anonymity for a large class of 2-agents protocols that was previously out of scope. It has been notably used to discover new attacks on ePassport protocols. I have written this tool by leveraging our new verification method proposed in our S&P’16 paper.
I have developed and implemented Partial Order Reduction techniques for a class of security protocols (those that are action-deterministic) in the tool Apte, dramatically improving its practical impact. I also have implemented a preliminary version of those techniques in the tool SPEC (more details).