Jérémy Thibault

Me

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

Research Interests

I am broadly interested in the intersection of programming languages and security. I believe formal verification can be used to make the world a safer and better place.

I am currently focusing my attention on secure compilation, and I am more particularly interested in building secure compilers that can be formally verified to be secure in proof assistants.

Curriculum Vitae

My CV is available in French and in English.

Publications

Conferences

• 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 35th IEEE Computer Security Foundations Symposium (CSF), pages 64--79. August 2022.
  • Coq 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 29th European Symposium on Programming (ESOP), pages 1--28. Springer, April 2020.
  • Superseded by An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
  • Coq development
• Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, and Jérémy Thibault.
  Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.
  In 32nd IEEE Computer Security Foundations Symposium (CSF), pages 256--271. June 2019. Distinguished Paper Award.
  • Coq development

Articles in Journals

• 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.
  An Extended Account of Trace-relating Compiler Correctness and Secure Compilation.
  In ACM Transactions on Programming Languages and Systems. Volume 43. Issue 4. December 2021.
  • Supersedes Trace-Relating Compiler Correctness and Secure Compilation
  • Coq development

Under Review

• 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.
  • Under review at CCS'24
  • See also the extended abstract submitted at PriSC'23: SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine.

Informal

• Jérémy Thibault, and Cătălin Hrițcu
  Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs.
  • Extended abstract submitted at PriSC'21
• Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hrițcu, 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.
  • Coq 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 .
  • Extended abstract submitted for the student research competition at POPL'19

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

Contact

You can contact me by e-mail at firstname.lastname@mpi-sp.org, where firstname = jeremy and lastname = thibault.