Cătălin Hrițcu
Tenured faculty and head of the Formally Verified Security group
at the
Max Planck Institute for Security and Privacy (MPI-SP) in
Bochum, Germany.
Between October 2013 and April 2020 I was a
tenured researcher (chargé de recherche)
at Inria Paris
in the Prosecco team.
Between May 2011 and
September 2013 I was a Postdoctoral Research Associate at
the University of Pennsylvania,
working under the supervision
of Benjamin
C. Pierce.
In the fall of 2016 I held a Visiting Researcher position at
Microsoft Research Redmond.
I received my PhD
from Saarland
University in Saarbrücken, Germany
and recently also a Habilitation from ENS Paris.
Quick Links:
Contact;
Interests;
Group;
Publications;
Talks;
Teaching;
Tools;
Misc
Research Projects
News/Events
- Certified Programs and Proofs, CPP (Steering Committee Chair since February 2021)
-
On 1 May 2020 I joined the new Max Planck Institute for Security and Privacy (MPI-SP)
in Bochum, Germany as a Tenured Faculty (W2).
- Certified Programs and Proofs, CPP 2020 and 2021 (PC & Conference Co-Chair)
- Computer Security Foundations, CSF 2020 and 2021 (PC member)
- Conference (CSF 2021): 22-25 June 2021, Online
-
Symposium on Security and Privacy, Oakland S&P 2021 (PC Member)
- Conference: 23-27 May 2021, Online
- Dagstuhl Seminar
20201 21481 on Secure Compilation (Co-Organizer)
- Seminar:
10-15 May, 2020 28 Nov - 3 Dec, 2021, Schloss Dagstuhl, Germany
- Nominated for EATCS Award
for the best ETAPS 2020 paper in theoretical computer science for
Trace-Relating Compiler Correctness and Secure Compilation
-
Kenji Maillard has successfully defended his
PhD thesis on 25 Nov 2019
- Distinguished Paper Award at CSF 2019 for Journey Beyond Full Abstraction
-
Habilitation defense on Tuesday, 29 January 2019 at Inria Paris
(Thesis)
-
Principles of Programming Languages, POPL 2018 & 2019
(Artifact Evaluation Co-Chair)
E-mail (preferred): catalin.hritcu@gmail.com
Address:
Universitätsstraße 140, 44799 Bochum, Germany
Research Interests
My research is primarily focused on developing rigorous formal
techniques for solving security problems. I am
particularly interested in:
-
formal methods for computer and network security:
memory safety,
compartmentalization,
dynamic monitoring,
integrity
-
programming-languages techniques:
type systems,
verification,
proof assistants,
property-based testing,
semantics,
formal metatheory,
certified tools
-
design and verification of security-critical systems:
reference monitors,
secure compilation chains,
secure hardware
Formally Verified Security Research Group
I am very fortunate to work with a group of outstanding students and starting researchers:
I still closely collaborate with some former members of my group at Inria Paris:
For a complete list of past members of my group please look here.
Recent Publications and Drafts
For a complete list of my papers please look here
(also on DBLP and Google Scholar).
-
Carmine Abate,
Philipp G. Haselwarter,
Exequiel Rivas,
Antoine Van Muylder,
Théo Winterhalter,
Cătălin Hrițcu,
Kenji Maillard, and
Bas Spitters.
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
Cryptology ePrint Archive: Report 2021/397, March 2021.
-
Maximilian Algehed,
Jean-Philippe Bernardy, and
Cătălin Hrițcu.
Dynamic IFC Theorems for Free!
To appear in 34nd
IEEE Computer Security Foundations Symposium (CSF), June 2021.
-
Carmine Abate,
Roberto Blanco,
Ștefan Ciobâcă,
Adrien Durier,
Deepak Garg,
Cătălin Hrițcu,
Marco Patrignani,
Éric Tanter, and
Jérémy Thibault.
Trace-Relating Compiler Correctness and Secure Compilation.
In 29th European Symposium on Programming (ESOP), pages 1--28. Springer, April 2020.
Nominated for EATCS Award for the best ETAPS 2020 paper in theoretical computer science.
-
Kenji Maillard,
Cătălin Hrițcu,
Exequiel Rivas, and
Antoine Van Muylder.
The Next 700 Relational Program Logics.
PACMPL, 4(POPL):4:1--4:33, January 2020.
-
Kenji Maillard,
Danel Ahman,
Robert Atkey,
Guido Martínez,
Cătălin Hrițcu,
Exequiel Rivas, and
Éric Tanter.
Dijkstra Monads for All.
PACMPL, 3(ICFP):104:1– 104:29, August 2019.
-
Carmine Abate,
Roberto Blanco,
Deepak Garg,
Cătălin Hrițcu,
Marco Patrignani, and
Jérémy Thibault.
Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation.
In 32nd
IEEE Computer Security Foundations Symposium (CSF), pages 256--271. June 2019.
Distinguished Paper Award.
-
Guido Martínez,
Danel Ahman,
Victor Dumitrescu,
Nick Giannarakis,
Chris Hawblitzel,
Cătălin Hrițcu,
Monal Narasimhamurthy,
Zoe Paraskevopoulou,
Clément Pit-Claudel,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem Rastogi,
Nikhil Swamy,
Meta-F*: Proof automation with SMT, Tactics, and Metaprograms.
In 28th European Symposium on Programming (ESOP), pages 30-59. Springer, May 2019.
-
Carmine Abate,
Arthur Azevedo de Amorim,
Roberto Blanco,
Ana Nora Evans,
Guglielmo Fachini,
Cătălin Hrițcu,
Théo Laurent,
Benjamin C. Pierce,
Marco Stronati, and
Andrew Tolmach.
When Good Components Go Bad:
Formally Secure Compilation Despite Dynamic Compromise.
In 25th ACM Conference on Computer and Communications Security (CCS), pages 1351--1368, ACM. October 2018.
-
Arthur Azevedo de Amorim,
Cătălin Hrițcu, and
Benjamin C. Pierce.
The Meaning of Memory Safety.
In 7th International Conference on Principles of Security and Trust (POST), pages 79--105, April 2018.
- A previous draft was entitled
Alpha is for Address! The Essence of Memory Safety
- Coq proofs available here and here
-
Danel Ahman,
Cédric Fournet,
Cătălin Hrițcu,
Kenji Maillard,
Aseem Rastogi, and
Nikhil Swamy.
Recalling a Witness: Foundations and Applications of Monotonic State.
In 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL),
PACMPL, 2(POPL):65:1-65:30, January 2018.
Talks
Here are my recent and upcoming talks. For a complete list of my talks please look here.
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- Formally Verified Security
- Certified Programs and Proofs, CPP 2020
- The Next 700 Relational Program Logics
- Recent: Everest All Hands: slides (2019-10-11)
- Dijkstra Monads for All
- Recent: Everest All Hands: slides (2019-10-10)
- When Good Components Go Bad
- The Quest for Formally Secure Compartmentalizing Compilation
- Verified Effectful Programming in F*
- What is secure compilation?
- Principles of Secure Compilation, PriSC'18
- Program Chair's Welcome Message: slides (2018-01-13)
Teaching
Here are my recent courses. For a complete list of my teaching please look here.
- Recent: Writing and Verifying Functional Programs in Coq course at
Summer School on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019,
24-31 August 2019 at INSA, Lyon, France
- Recent: Program Verification with F* course at Summer School on
Verification Technology, Systems, and Applications, VSTA 2019,
1-5 July 2019 at University of Luxembourg
- Formally Secure Compartmentalizing Compilation course at
International School on Foundations of Security Analysis and Design (FOSAD),
27-28 August, 2018, Bertinoro, Italy
- Program Verification with F* course at
EPIT 2018 Software Verification Spring School, 7-11 May, 2018, Aussois, France
- Verifying Cryptographic Implementations with F* at
Computer-aided security proofs summer school. Aarhus, Denmark, October, 2017
- Verifying Cryptographic Implementations with F* course at Models and Tools for Cryptographic Proofs summer school, Nancy, France, July 2017
- Program Verification with F* at the Parisian Master of Research in Computer Science (MPRI), January 2017
- Verifying Cryptographic Protocol Implementations with F* course at Computer Aided Analysis of Cryptographic Protocols summer school, Bucharest, Romania, September 2016
- F* Course: Type Systems for Security Verification, Saarland University, March 2015
- F* tutorial
Here are my current software projects. For a complete list of software please look here.
Misc
