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 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
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.
- Andrea Stedile, Researcher at UniTN since February 2024
On the Amadeus project and the Actum library.
MSc, BSc Thesis Students & Interns
- Stefano Dal Mas, MS Intern, on ColorWasm Formalisation
- Riccardo Germenia, MS Intern, on UC Simulator autoextractor
- Taras Rashkevich, MSc, on A Tagbased Filesystem in Rust
- Alessio Amiri, BSc, on Blockchain protocols in Actum
- Giulio Bazzoli, BSc, on Tock!os security analysis
- Alfredo Bombace, BSc, on Spectector SMT checking in Coq
- Lorenzo Bodini, BSc, on 2d Trentino Trasporti Visualizer
- Lorenzo Cattai, BSc, on Rust Godot
- Ilya Emeliyanov, BSc, on Hackaprompt VisualCode plugin
- Federico Frigerio, BSc, on A Rust Website for Software Faires
- Rafiu Hossain, BSc, on Object Capabilities for Java IDE
- Lorenzo Midiri, BSc, on Sanbapolis web view infrastructure
- Federico Pezzato, BSc, on Rust Drivers for 3d Printers
- Francesco Piazzi, BSc, on Raft in Actum
- Agostino Pisanelli, BSc, on Content-Based FS Literature
- Marcel Stolin, BSc, on ETAS-related thesis
- Giovanni Zanibellato, BSc, on Sanbapolis offline view module
Former Group Members and Students
Luca Podavini (BSc @Unitn, 2024), Patrick Cerka (BSc @Unitn, 2024), Matteo Possamai (BSc @Unitn, 2024), Sebastiano Tocci (BSc @Unitn, 2024),
Alessio Zeni (BSc @Unitn, 2024), Luca Sartore (BSc @Unitn, 2024), Fabio Giovanazzi (BSc @Unitn, 2024),
Andrea Ballarini (BSc @Unitn, 2024), Roberto Cornacchiari (BSc @Unitn, 2024), Sabin Andone (MSc @Unitn, 2024)
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
- Keynote: @GTMFS'24 [ slides ]
- Chair: Prisc'25, Prisc'24, FCS'23, FCS'22
- Organiser/co organiser: PRISC’19, PRISC’18, 1st Secure Compilation Meeting
- PC: Itasec'25, PLAS'24, CSF'24, Itasec'24, SecDev ‘24, Prisc'23, POPL'23, SecDev'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