Currently, I am a postdoctoral researcher in the Formally Verified Security group at the Max Planck Institute for Cyber Security and Privacy (previously a Starting Researcher in the Prosecco team at Inria Paris). I work with Cătălin Hriţcu in the ERC SECOMP project (and previously in the DARPA SSITH HOPE project).
My research interests are centered around the development and application of formal methods to solve computer security problems, developed along both axes:
Programming languages: proof assistants; formal specification, testing and verification; proof certificates; type systems; computational logic.
Computer security: secure compilation; compartmentalization; security policies; secure hardware.
The principal objective of my work at Prosecco is to build secure compilation chains that preserve useful classes of security properties while scaling to realistic programming languages and enabling efficient and secure program execution.
Previously, I was a doctoral researcher in the Parsifal team (now Partout) at the LIX laboratory at École polytechnique and Inria Saclay - Île de France. I was advised by Dale Miller working in the ERC ProofCert project.
A grand unifying theme and pragmatic motivation of my research is an ambition that I am convinced is both lofty and realistic: this is the need for trust (which encompasses a notion of security) and correctness — in theorems as in the entire pantheon of formalizable artifacts, with software as primus inter pares in today’s world — and a discipline that treats these as first-class abstractions.