Broadly, I am interested in formal methods, programming language and security (generally, programming language security and secure compilation).
I am one of the main promotors of the secure compilation research field, having developed with my collaborators:
- secure compilation criteria (modular full abstraction, trace-preserving compilation, robustly safe compilation, robust hyperproperty preservation criteria);
- proof techniques for secure compilation (trace-based backtranslation, approximate context-based backtranslation);
- instances of secure compilers in action (secure compilation for Spectre, for PMA and for high-level capability machines);
- teaching material for secure compilation (see my teaching page);
More precisely, here is my (old/outdated) research statement.
- 2021: Novi/Facebook grant for our work on robust safety for the Move language.
- 2019: Distinguished Paper Award for Journey beyond full abstraction in CSF
- Xaver Fabian, PhD student at Cispa since September 2021
On formal verification for Spectre V2+ variants and their secure compilation.
- Matthis Kruse, PhD student at Cispa since October 2021
On formal foundations of composition for secure compilers.
Xaver Fabian (@Cispa, 2021)
Eric Martin (@Stanford, 2020-2021)
Koby Chan (@Stanford, 2020)
Wilson Nguyen (@Stanford, 2019)
Nicholas Barbier (@Stanford, 2019)
Max DiGiacomo (@Stanford, 2019)
Maximilian Schwenger (@MPI-SWS, 2017)
Akram El-Korashy (@MPI-SWS 2016-2020)
Matthias van der Hallen (@ KU Leuven, 2014)
Pieter van Geel (@ KU Leuven, 2013)
- Organiser/co organiser: PRISC’19, PRISC’18, 1st Secure Compilation Meeting
- PC: POPL'23, Aplas'22, SecDev'22, SecDev'21, CCS'21, CSF’20, SAC’19, SAC’18, SAC’17, FCS’16, SAC’16, SAC’15, ICCSW’14
- Reviewer: JFP, CSF'21, POPL’16, CSF’15, Elsevier’s COMLAN, FOCLASA’14, GPCE’14, Scientific World Journal, IFM’13, FSEN’13, ESOP’12, IWACO’11, Dagstuhl seminar on secure compilation
- Panel member: PLMW@PLDI'21