Marco Patrignani

Below is a list of my publications, sorted by year, followed by my talks.

Papers

My publications can also be found on DBLP or on my Google Scholar page.

I encourage people to write articles using syntax highlighting.

2024
  • Moreno, Williams, Guarnieri, Patrignani. Automatically Synthesizing Leakage Contracts from Counterexamples. In womENcourage 2024.
    [ .pdf ]
  • Künnemann, Patrignani, Cecchetti. Computational-Bounded Robust Compilation and Universally Composable Security. In CSF'24
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ site ]
  • Devriese, Martin, Patrignani. Mechanizing the Comparison of the Semantic Expressiveness of Recursive Types. In LMCS
    [ .pdf ] | [ .bib ] | [ arxiv ]
2023
  • Michael, Gollamudi, Bosamiya, Disselkoen, Denlinger, Watt, Parno, Patrignani, Vassena, Stefan. MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code. In POPL'23.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Patrignani, Blackshear: Robust Safety for Move. In CSF'23.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ slides ]
  • Patrignani, Kruse. Blame-Preserving Secure Compilation. In Prisc'23.
    [ .pdf ]
2022
  • Fabian, Guarnieri, Patrignani: Automatic Detection of Speculative Execution Combinations. In CCS'22. (Distinguished Paper Award)
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Crichton, Patrignani, Agrawala, Hanrahan: Modular Information Flow Through Ownership. In PLDI'22.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Devriese, Patrignani, Piessens: Two Parametricities versus three Universal Types. In ACM TOPLAS.
    [ .pdf ] | [ .bib ] | [ acm]
  • Kruse, Patrignani: Composing Secure Compilers. In Prisc'22.
    [ .pdf ]
2021
  • Patrignani, Martin, Devriese: On the Semantic Expressiveness of Recursive Types. In POPL'21.
    Superseded by the 2024 paper.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ short vid ] | [ long vid ]
  • Patrignani, Garg. Robustly Safe Compilation, an Efficient Form of Secure Compilation. In ACM TOPLAS.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ link ]
  • Patrignani, Guarnieri. Exorcising Spectres with Secure Compilers. In CCS'21.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ short vid ] | [ long vid ] | [ slides ]
  • Abate, Blanco, Ciobaca, Durier, Garg, Hritcu, Patrignani, Tanter, Thibault: An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation. In ACM TOPLAS.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • El-Korashy, Tsampas, Patrignani, Devriese, Garg, Piessens: CapablePtrs: Securely Compiling Partial Programs using the Pointers-as-Capabilities Principle. In CSF'21.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Fabian, Chan, Guarnieri, Patrignani: Formal Verification of Combined Spectre Attacks. In PLAS'21.
    [ .pdf ]
2020
  • Durst, Feldman, Huff, Akeley, Daly, Bernstein, Patrignani, Fatahalian, Hanrahan: Type-Directed Scheduling Of Streaming Accelerators. In PLDI’20.
    [ .pdf ] | [ link ]
  • Abate, Blanco, Ciobaca, Durier, Garg, Hritcu, Patrignani, Tanter, Thibault: Trace-Relating Compiler Correctness and Secure Compilation. In ESOP’20.
    Superseded by the TOPLAS 2021 paper.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Patrignani, Wahby, Künnemann: Universal Composability is Secure Compilation. In Prisc’20.
    [ arxiv ] | [ slides ] | [ video ]
  • Guarnieri, Patrignani: Exorcising Spectres with Secure Compilers. In Prisc’20.
    [ arxiv ] | [ video ]
  • Vassena, Patrignani: Memory Safety Preservation for WebAssembly. In Prisc’20.
    [ arxiv ] | [ video ]
2019
  • Abate, Blanco, Garg, Hritcu, Patrignani, Thibault: Journey Beyond Full Abstraction. In CSF’19 (Distinguished Paper Award) Aka: Exploring Robust Property Preservation for Secure Compilation.
    [ .pdf ] | [ .bib ] | [ arxiv ]
  • Patrignani, Garg: Robustly Safe Compilation. In ESOP’19.
    Superseded by the TOPLAS 2021 paper.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ techreport ] | [ slides ]
  • Patrignani, Ahmed, Clarke: Formal Approaches to Secure Compilation. In ACM Computing Surveys (CSUR).
    [ .pdf (full) ] | [ .bib ] | link ]
2018
  • Garg, Hritcu, Patrignani, Stronati, Swasey: Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). In PriSC’18.
    Superseded by the CSF 2019 paper.
    [ arxiv ] | [ slides ]
  • Devriese, Patrignani, Piessens: Parametricity versus the Universal Type In POPL’18.
    Superseded by the TOPLAS 2022 paper.
    [ .pdf ] | [ techrep ] | [ .bib ]
2017
  • Devriese, Patrignani, Piessens, Keuchel: Modular, Fully-Abstract Compilation by Approximate Back-Translation. In LMCS.
    [ .pdf ] | [ techrep ]
  • Tsampas, El-Korashy, Patrignani, Devriese, Garg, Piessens: Towards Automatic Compartmentalization of C Programs on Capability Machines. In FCS’17.
    [ .pdf ]
    Superseded by the CSF 2021 paper.
  • Patrignani, Garg: Secure Compilation and Hyperproperty Preservation. In CSF’17.
    [ .pdf ] | [ .bib ] | [ slides ]
2016
  • Patrignani, Devriese, Piessens: On Modular and Fully-Abstract Compilation. In CSF’16.
    [ .pdf ] | [ .bib ] | [ arxiv ] | [ slides ]
  • Larmuseau, Patrignani, Clarke: Implementing a Secure Abstract Machine. In SAC’16.
    [ .pdf ]
  • Devriese, Patrignani, Piessens: Fully-Abstract Compilation by Approximate Back-Translation. In POPL’16.
    Superseded by the LMCS 2017 paper.
    [ .pdf ] | [ .bib ]
2015
  • Larmuseau, Patrignani, Clarke: A Secure Compiler for ML Modules. In APLAS’15.
    [ .pdf ]
  • Larmuseau, Patrignani, Clarke: A High-Level Model for an Assembly Language Attacker by Means of Reflection. In SETTA’15.
    [ .pdf ]
  • Patrignani, Devriese, Piessens. Multi-Module Fully Abstract Compilation (Extended Abstract). In FCS’15.
    Superseded by the CSF 2016 paper.
    [ .pdf ]
  • Patrignani. The Tome of Secure Compilation: Fully Abstract Compilation to Protected Modules Architectures. Ph.D. Thesis.
    [ .pdf ] | [ .bib ] | [ slides ]
  • Patrignani, Clarke: Fully Abstract Trace Semantics for Protected Module Architectures. In Elsevier’s COMLAN.
    [ .pdf ] | [ link ] | [ .bib ]
  • Patrignani, Agten, Strackx, Jacobs, Clarke, Piessens: Secure Compilation to Protected Module Architectures. In ACM TOPLAS.
    [ .pdf ] | [ link ] | [ .bib ]
2014
  • Larmuseau, Patrignani, Clarke: Operational Semantics for Secure Interoperation._ In PLAS’14.
    [ .pdf ]
  • Patrignani, Clarke: Fully Abstract Trace Semantics for Low-level Isolation Mechanisms. In SAC’14.
    Superseded by the COMLAN 2015 paper.
    [ .pdf ] | [ .bib ] | [ techrep ] | [ slides ]
2013
  • Patrignani, Clarke, Piessens: Secure Compilation of Object-Oriented Components to Protected Module Architectures. In APLAS’13.
    Superseded by the TOPLAS 2015 paper.
    [ .pdf ] | [ .bib ] | [ techrep ] | [ slides ] | [ Algorithm: SCOO-algo.zip ]
2012
  • Patrignani, Clarke: Fully Abstract Trace Semantics of Low-Level Protection Mechanisms – Abstract. In NWPT’12.
    Superseded by the COMLAN 2015 paper.
    [ .pdf ]
  • Patrignani, Matthys, Proença, Hughes, Clarke: Formal Analysis of Policies In Wireless Sensor Network Applications._ In SESENA’12.
    [ .pdf ]
2011
  • Patrignani, Clarke, Sangiorgi. Ownership Types for the Join Calculus._ In FMOODS / FORTE'11.
    [ .pdf ] | [ .bib ] | [ slides ]
What do These Acronyms Mean?

In case you are a student and want to understand the list above, computer science research is published in conferences as well as journals, unlike other fields that only have journals. Both kinds are sorted by level, from the very top (aka A*), down (A, B+, B etc). Workshop publications are not ranked. Here’s a table to make sense of the papers above.

Acronym Kind Rank
POPL, CCS, PLDI Conference A*
ESOP, CSF Conference A
Forte, Sac, Aplas Conference B
PRISC Workshop
Toplas Journal A*
LMCS Journal A
COMLAN Journal B

Talks

  • Keynote: Secure Compilation: Formal Foundations and (Some) Applications
    (@GTMFS) 03/04/2024 [ slides ]
  • Compositional Secure Compilation against Spectre
    (@Dagstuhl) 29/11/2021 [ slides ]
  • Exorcising Spectres with Secure Compilers – CSC Report
    (@Cispa) 23/06/2021 [ slides ]
  • Grad School Panel
    (@ PLMW PLDI) 21/06/2021 [ slide ]
  • On the semantic expressiveness of recursive types
    (@ UPenn PL Club) 17/03/2021 [ slides ]
  • On the semantic expressiveness of recursive types
    (@ Stanford Software lunch) ?/11/2020 [ slides ]
  • Foundations and Applications of Secure Compilation
    (@ Libra / Facebook) 20/03/’20 [ slides ]
  • Exorcising Spectres with Secure Compilers
    (@ Stanford security lunch) 11/03/’20 [ slides ]
  • Some more Secure Compilation
    (@ Crypto ski retreat) 07/03/’20 sketchy [ slides ]
  • Robustly-Safe Compilation
    (@ Stanford security lunch) 04/’19 [ slides ]
  • What is Secure Compilation?
    (@ Stanford security lunch) 10/’18 [ slides ]
  • Robust is the new black
    (@ Leuven 12/’17) sketchy [ slides ]
  • Secure Compilation Lecture
    (@ UniBo 10/’17) [ slides ]
  • 5-minutes advertisement for PRiSC
    (@ CSF’17) [ slides ]
  • SCM’17 opening: What is Secure Compilation
    (@ SCM ’17) [ slides ]
  • Secure compilation and hyperproperties preservation
    (@MPI retreat) ?/’16 [ poster ]
  • Secure compilation and hyperproperties
    (@INRIA, Paris 08/’16) [ slides ]
  • Secure compilation
    (@NE, Boston 01/’16) [ slides ]
  • Popl’16 paper and followup
    (@Leuven 12/’15) sketchy [ slides ]
  • Secure compilation
    (@Saarbrucken 04/’15) [ slides ]
  • Secure compilation and my research
    (@Uppsala 04/’14) [ slides ]
  • Session types and capabilities
    (@ Imperial 01/’14) sketchy [ slides ]

If anyhing is missing, perhaps it can be found in my old homepage.