My picture

I am a computer science student in the Parisian Master of Research in Computer Science (MPRI) at Ecole Normale Supérieure Paris-Saclay.

As part of that program, I am currently an Intern at the Max Planck Institute for Security and Privacy, where I work with Cătălin Hrițcu on formally secure compilation against speculative side-channel attacks.

Publications

Papers

FSLH: Flexible Mechanized Speculative Load Hardening

Distinguished Paper Award
Jonathan Baumann, Roberto Blanco, Léon Ducruet, Sebastian Harwig, and Cătălin Hrițcu

38th IEEE Computer Security Foundations Symposium (CSF) (2025)

Paper (arXiv) Rocq Development (GitHub) Presentation Slides

Internships and Bachelor Thesis

Towards More Efficient and Trustworthy Formally Secure Verification Against Speculative Side-Channel Attacks

Jonathan Baumann, supervised by Cătălin Hrițcu

Parisian Master of Research in Computer Science (MPRI) (2025)

Internship Report FSLH Rocq Development (GitHub) Speculative Semantics Rocq Development (GitHub)

Proofs of Cryptographic Primitives in CCSA Logic

Jonathan Baumann, supervised by Guillaume Scerri and Théo Vignon

Ecole Normale Supérieure Paris-Saclay (2024)

Internship Report Presentation Slides

Verifying Spectre Countermeasures Using Hypersimulations

Jonathan Baumann, supervised by Julian Rosemann

Saarland University (2023)

Bachelor’s Thesis Coq Development (CoqDoc) Presentation Slides

Education