Jérémy Thibault

I am currently a PhD student in the Formally Verified Security group at the Max Planck Institute for Security and Privacy, supervised by Cătălin Hriţcu. I used to work in the Prosecco team at Inria Paris.

My current work lies at the intersection of programming language theory, formal methods, and computer security: using techniques from these fields, I build formally secure compilers, i.e. compilers that are proved to preserve security properties. In particular, I am designing proof techniques for secure compilation that (1) may be implemented in a proof assistant; and (2) scale up to compilers for realistic languages. As the most recent example, we built SECOMP, an extension of CompCert that compiles compartmentalized C code.

Curriculum Vitae

My CV is available in English (long version) and in French (long version)

Publications

Conferences

Jérémy Thibault, Joseph Lenormand, and Catalin Hritcu.
“Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs,”
CoRR abs/2503.19609 (2025), https://doi.org/10.48550/ARXIV.2503.19609.
- Accepted at ITP'25
- Rocq development
Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Cătălin Hriţcu, and Andrew Tolmach.
“SECOMP: Formally Secure Compilation of Compartmentalized c Programs,”
in Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, CCS ’24 (ACM, 2024), 1061–75, https://doi.org/10.1145/3658644.3670288.
- Rocq development
Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, and Cătălin Hriţcu.
“SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation,”
in 2022 IEEE 35th Computer Security Foundations Symposium (CSF) (IEEE, 2022), 64–79, https://doi.org/10.1109/csf54842.2022.9919680.
- Rocq development
Carmine Abate, Roberto Blanco, Ștefan Ciobâcă, Adrien Durier, Deepak Garg, Cătălin Hrițcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault.
“Trace-Relating Compiler Correctness and Secure Compilation,”
in Programming Languages and Systems (Springer International Publishing, 2020), 1–28, https://doi.org/10.1007/978-3-030-44914-8_1.
- Superseded by An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
- Rocq development
Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault.
“Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation,”
in 2019 IEEE 32nd Computer Security Foundations Symposium (CSF) (IEEE, 2019), https://doi.org/10.1109/csf.2019.00025.
- Distinguished Paper Award
- Rocq development

Journals

Carmine Abate, Roberto Blanco, Ştefan Ciobâcă, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, and Jérémy Thibault.
“An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation,”
ACM Trans. Program. Lang. Syst. 43, no. 4 (2021): 14:1–48, https://doi.org/10.1145/3460860.
- Supersedes Trace-Relating Compiler Correctness and Secure Compilation
- Rocq development

Informal publications

Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Jérémy Thibault, and Andrew Tolmach.
“When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise,” 2019, https://arxiv.org/abs/1802.00588.
- Rocq development
- Contribution: significant improvement to the proof by removing the use of partial semantics
Jérémy Thibault.
“A Trace-Based Proof Technique for Secure Compilation,” 2019.
- Extended abstract submitted for the student research competition at POPL'19

Service

Workshop PC

PriSC'25

Sub-reviewer

POPL'24, JCS, RV, JFP

Artifact evaluation committee

OOPSLA'24, POPL'23

Teaching

Teaching assistant for Foundations of Programming Languages, Verification, and Security (Winter Semester 2023-2024, Ruhr Universität Bochum, Germany).
(One semester course based on Software Foundations Vol. 2)
Teaching assistant for Writing and Verifying Functional Programs in Coq (Summer School on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019, Lyon, France)

Internships

Internship in the Prosecco Team at Inria.
Subject: “A Trace-based Proof Technique for Secure Compilation”.
- Supervision: Cătălin Hriţcu.
- From February 2018 to June 2018
- The work was integrated in our paper, Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Internship in the Logic and semantics group at Aarhus University.
Subject: “Improving language-based predictive mitigation for information-flow security"
- Supervision: Aslan Askarov.
- From June 2017 to August 2017
- Internship report: Improving language-based predictive mitigation for information-flow security.
Internship in the SUMO Team at Irisa (Rennes, France).
Subject: «Games with hierarchical objectives»
- Supervision: Ocan Sankur
- From May 2016 to July 2016