Research Interests
Broadly, I am interested in formal methods, programming language and security (generally, programming language security and secure compilation).
I am an active promotor 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
- 2023: Prin-PNRR project: Amadeus
- 2022: Mysten Labs gift for our work on formalising Sui-Move.
- 2022: CCS Distinguished Paper Award for Automatic detection of speculative execution combinations.
- 2022: Rita Levi Montalcini grant (2022-2025).
- 2021: Novi/Facebook grant for our work on robust safety for Move.
- 2019: CSF Distinguished Paper Award for Journey beyond full abstraction.
Open Positions
I am looking for:
1 PhD student (at UniTN) on PL & security
1 PhD student (at CISPA) on PL & security
1 student researcher (at UniTN)
Strong background in programming languages semantics is required, as well as will to move to Trento and travel internationally.
Research Group
- Xaver Fabian, PhD student at Cispa and UniTN 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. - Luca Giacometti, BSc student researcher at UniTN since February 2024
On confidentiality for Move. - Andrea Stedile, Researcher at UniTN since February 2024
Thesis Students
- Sabin Andone, MSc, on Exploring Rust to MSWasm Compilation
- Matteo Zanotto, MSc, on Verification for the Sui Blockchain
- Taras Rashkevich, MSc, on A Tagbased Filesystem in Rust
- Alessio Zeni, BSc, on A Rust Learning Platform
- Luca Podavini, BSc, on Move Fuzzer
- Andrea Ballarini, BSc, on EVM to Move Compilation
- Luca Sartore, BSc, on Jigsaw Recognition
- Federico Frigerio, BSc, on A Rust Website for Software Faires
- Federico Pezzato, BSc, on Rust Drivers for 3d Printers
Former Group Members and Students
Luca Giacometti (BSc @UniTN, 2023), Andrea Stedile (MSc @UniTN, 2023), Sacha Bordais-Poulard (MSc @UniTN, 2023), Guillaume Massal (MSc @UniTN, 2023)
Xaver Fabian (@Cispa, 2021)
Koby Chan (@Stanford, 2020), Eric Martin (@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
- Chair: Prisc'25, Prisc'24, FCS'23, FCS'22
- Organiser/co organiser: PRISC’19, PRISC’18, 1st Secure Compilation Meeting
- PC: CSF'24, Prisc'23, 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