publications and Talks (sorted by year).

 

Here is a link to my DBLP entries and to my Google scholar page.

I encourage people to write articles using syntax highlighting (here are the macros of that article while here are general macros for typesetting PL).

  1. ๏Patrignani. Why Should Anyone Use Colours? [ .pdf | arxiv ]


Given the high usage, here is a guide describing how to use and compile your own version of the robust compilation diagram from our CSF’19 paper, as well as the sources mentioned in said guide [ .pdf | .zip ]


2020

  1. ๏Durst, Feldman, Huff, Akeley, Daly, Bernstein, Patrignani, Fatahalian, Hanrahan. Type-Directed Scheduling Of Streaming Accelerators. In PLDI’20. [ .pdf ]

  2. ๏Abate, Blanco, Ciobaca, Durier, Garg, Hritcu, Patrignani, Tanter, Thibault. Trace-Relating Compiler Correctness and Secure Compilation. In ESOP’20. [ .pdf | arxiv ]

  3. ๏Patrignani, Wahby, Künnemann. Universal Composability is Secure Compilation. In Prisc’20. [ arxiv | slides | video ]

  4. ๏Guarnieri, Patrignani. Exorcising Spectres with Secure Compilers. In Prisc’20. [ arxiv | video ]

  5. ๏Vassena, Patrignani. Memory Safety Preservation for WebAssembly. In Prisc’20. [ arxiv | video ]


2019

  1. ๏Abate, Blanco, Garg, Hritcu, Patrignani, Thibault. Journey Beyond Full Abstraction. In CSF’19 (Distinguished Paper Award) [ .pdf | .bib | arxiv | coq | techreport ]

        Aka: Exploring Robust Property Preservation for Secure Compilation.

  1. ๏Patrignani, Garg. Robustly Safe Compilation. In ESOP’19 [ .pdf | .bib | arxiv | techreport | slides ]

  2. ๏Patrignani, Ahmed, Clarke. Formal Approaches to Secure Compilation. In ACM Computing Surveys (CSUR). [ .pdf | .pdf (full) | .bib | online | online appendix ]


2018

  1. ๏Garg, Hritcu, Patrignani, Stronati, Swasey: Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract). In PriSC’18 [ arxiv | slides ]

  2. ๏Devriese, Patrignani, Piessens: Parametricity versus the Universal Type In POPL’18 [ .pdf | techrep | .bib ]


2017

  1. ๏Devriese, Patrignani, Piessens, Keuchel. Modular, Fully-Abstract Compilation by Approximate Back-Translation. In LMCS [ .pdf | .bib | techrep | coq ]

  2. ๏Tsampas, El-Korashy, Patrignani, Devriese, Garg, Piessens. Towards Automatic Compartmentalization of C Programs on Capability Machines. In FCS’17 [ .pdf ]

  3. ๏Patrignani, Garg: Secure Compilation and Hyperproperty Preservation. In CSF’17 [ .pdf | .bib | techrep | slides ]


2016

  1. ๏Patrignani, Devriese, Piessens: On Modular and Fully-Abstract Compilation. In CSF’16 [ .pdf | .bib | techrep | arxiv | slides ]

  2. ๏Larmuseau, Patrignani, Clarke: Implementing a Secure Abstract Machine. In SAC’16 [ .pdf ]

  3. ๏Devriese, Patrignani, Piessens: Fully-Abstract Compilation by Approximate Back-Translation. In POPL’16 [ .pdf | .bib | techrep ]


2015

  1. ๏Larmuseau, Patrignani, Clarke: A Secure Compiler for ML Modules. In APLAS’15 [ .pdf ]

  2. ๏Larmuseau, Patrignani, Clarke: A High-Level Model for an Assembly Language Attacker by Means of Reflection. In SETTA’15 [ .pdf ]

  3. ๏Patrignani, Devriese, Piessens. Multi-Module Fully Abstract Compilation (Extended Abstract). In FCS’15 [ .pdf | .bib | slides ]

  4. ๏Patrignani. The Tome of Secure Compilation: Fully Abstract Compilation to Protected Modules Architectures. Ph.D. Thesis [ .pdf | link | .bib | slides ]

  5. ๏Patrignani, Clarke: Fully Abstract Trace Semantics for Protected Module Architectures. In Elsevier’s COMLAN. [ .pdf | link | .bib ]

  6. ๏Patrignani, Agten, Strackx, Jacobs, Clarke, Piessens: Secure Compilation to Protected Module Architectures. In ACM TOPLAS. [ .pdf | link | .bib ]


2014

  1. ๏Larmuseau, Patrignani, Clarke: Operational Semantics for Secure Interoperation. In PLAS’14. [ .pdf | .bib ]

  2. ๏Patrignani, Clarke: Fully Abstract Trace Semantics for Low-level Isolation Mechanisms. In SAC’14. [ .pdf | .bib | techrep| slides ]


2013

  1. ๏Patrignani, Clarke, Piessens: Secure Compilation of Object-Oriented Components to Protected Module Architectures. In APLAS’13. [ .pdf | .bib | techrep | slides ] Algorithm: SCOO-algo.zip


2012

  1. ๏Patrignani, Clarke: Fully Abstract Trace Semantics of Low-Level Protection Mechanisms -- Abstract. In NWPT’12. [ .pdf | .bib | slides ]

  2. ๏Patrignani, Matthys, Proença, Hughes, Clarke: Formal Analysis of Policies in Wireless Sensor Network Applications. In SESENA’12. [.pdf | .bib | slides ]


2011

  1. ๏Patrignani, Clarke, Sangiorgi: Ownership Types for the Join Calculus. In FMOODS/FORTE’11. [ .pdf | .bib | techrep | slides ]




OTHER TALKS:

  1. •Foundations and Applications of Secure Compilation

    (@ Libra / Facebook) 20/03/’20 [ slides ]

  1. •Exorcising Spectres with Secure Compilers

    (@ Stanford security lunch)  11/03/’20 [ slides ]

  1. •Some more Secure Compilation

    (@ Crypto ski retreat) 07/03/’20 *sketchy* [ slides ]

  1. •Robustly-Safe Compilation

    (@ Stanford security lunch) 04/’19 [ slides ]

  1. •What is Secure Compilation?

    (@ Stanford security lunch) 10/’18 [ slides ]

  1. •Robust is the new black

    (@ Leuven 12/’17) *sketchy* [ slides ]

  1. •Secure Compilation Lecture

    (@ UniBo 10/’17) [ slides ]

  1. •5-minutes advertisement for PRiSC

    (@ CSF’17) [ slides ]

  1. •SCM’17 opening: What is Secure Compilation

    (@ SCM ’17) [ slides ]

  1. •Secure compilation and hyperproperties preservation

    (@MPI retreat) ?/’16 [ poster ]

  1. •Secure compilation and hyperproperties

    (@INRIA, Paris 08/’16) [ slides ]

  1. •Secure compilation

    (@NE, Boston 01/’16) [ slides ]

  1. •Popl’16 paper and followup

    (@Leuven 12/’15) *sketchy* [ slides ]

  1. •Secure compilation

    (@Saarbrucken 04/’15) [ slides ]

  1. •Secure compilation and my research

    (@Uppsala 04/’14) [ slides ]

  1. •Session types and capabilities

    (@ Imperial 01/’14) *sketchy* [ slides ]