Marco Patrignani

Research Interests

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.

Grants and Awards

  • 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

Research Group

  • 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.

Open Positions

Former Group Members and Students

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)

Professional Activity

  • 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