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.
I am also a PI of the CASA Excellence Center at
Ruhr University Bochum (RUB).
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
-
Principles of Programming Languages, POPL
(Artifact Evaluation Chair in 2018 and 2019;
also PC Member in 2017 and 2024)
- Symposium: 17-19 January 2024, London, UK
- Computer Security Foundations, CSF (Test-of-Time Awards Chair in 2023 and 2024;
also PC Member in 2020, 2021 and 2024)
- CSF 2024 Submission deadlines:
15 May 2023, 30 Sept 2023, and 3 Feb 2024
- CSF 2024 Symposium: 8-12 July 2024, Enschede, The Netherlands
- Certified Programs and Proofs, CPP (Steering Committee Chair since 2021;
also PC Chair and Conference Chair in 2020 and 2021; also PC member in 2016)
- Abstract deadline: 12 September 2023
- Submission deadline: 19 September 2023
- Conference: 15-16 January 2024, London, UK (with POPL)
- Principles of Secure Compilation, PriSC (Steering Committee Chair 2019--2023, Steering Committee Member since 2023, also PC Chair in 2018)
- Théo Winterhalter, former PostDoc in my group, took a tenured researcher position (CR) at Inria Saclay, in Deducteam, starting in October 2022. Kenji Mailard, graduated PhD student I supervised, has obtained a similar Inria position (ISFP), in the Gallinette team in Nantes.
- Arthur Azevedo de Amorim, graduated PhD student I co-supervised at University of Pennsylvania, started as Assistant Prof. at Rochester Institute of Technology in Jan 2023.
- Guido Martínez, co-supervised PhD student at CIFASIS-CONICET and UNR, Argentina, started as a Research Software Engineer at Microsoft Research in Redmond in Jan 2023.
- Carmine Abate, graduated PhD student I supervised at
MPI-SP, took a Formal Verification Researcher position in the Dresden Research Center of Huawei, starting in May 2022.
- Dagstuhl Seminar 21481 on Secure Compilation, December 2021 (Organizer)
- Distinguished Paper Award at CSF 2021 for
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
-
IEEE Symposium on Security and Privacy, Oakland S&P 2021 (PC Member)
- Cezar Constantin-Andrici won 1st prize at the Student Research Competition of ICFP 2020
-
On 1 May 2020 I joined the new Max Planck Institute for Security and Privacy (MPI-SP)
in Bochum, Germany as a Tenured Faculty (Research Group Leader with Tenure).
- Distinguished Paper Award at CSF 2019 for Journey Beyond Full Abstraction
E-mail: catalin.hritcu@mpi-sp.org or catalin.hritcu@gmail.com
Address:
Universitätsstraße 142, 44799 Bochum, Germany
On the RUB Campus, Building: Technologiezentrum Ruhr (TZR, aka MB), Office: S-W 106
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 security:
memory safety,
compartmentalization,
dynamic monitoring,
integrity
-
programming-languages techniques:
type systems,
program 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:
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).
-
Cezar-Constantin Andrici,
Ștefan Ciobâcă,
Cătălin Hrițcu,
Guido Martínez,
Exequiel Rivas,
Éric Tanter, and
Théo Winterhalter.
Securing Verified IO Programs Against Unverified Code in F*. Draft. July 2023.
-
Philipp G. Haselwarter,
Benjamin Salling Hvass,
Lasse Letager Hansen,
Théo Winterhalter,
Cătălin Hrițcu, and
Bas Spitters.
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
Draft. February 2023.
-
Jérémy Thibault,
Arthur Azevedo de Amorim,
Roberto Blanco,
Aïna Linn Georges,
Cătălin Hrițcu,
Andrew Tolmach.
SECOMP2CHERI: Securely Compiling Compartments
from CompCert C to a Capability Machine. Extended Abstract at
Workshop on Principles of Secure Compilation (PriSC).
Jan 2023.
-
Philipp G. Haselwarter,
Exequiel Rivas,
Antoine Van Muylder,
Théo Winterhalter,
Carmine Abate,
Nikolaj Sidorenco,
Cătălin Hrițcu,
Kenji Maillard, and
Bas Spitters.
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
In ACM Transactions on Programming Languages and Systems (TOPLAS).
Volume 45, Issue 3, July 2023.
-
Cezar-Constantin Andrici,
Théo Winterhalter,
Cătălin Hrițcu, and
Exequiel Rivas.
Verifying non-terminating programs with IO in F*.
Presentation at the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2022).
September 2022.
-
Théo Winterhalter,
Cezar-Constantin Andrici,
Cătălin Hrițcu,
Kenji Maillard,
Guido Martínez, and
Exequiel Rivas.
Partial Dijkstra Monads for All.
Extended abstract of presentation at the 28th International Conference on Types for Proofs and Programs (TYPES 2022).
June 2022.
-
Akram El-Korashy,
Roberto Blanco,
Jérémy Thibault,
Adrien Durier,
Deepak Garg, and
Cătălin Hrițcu.
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation.
In 35th
IEEE Computer Security Foundations Symposium (CSF).
August 2022.
-
Maximilian Algehed,
Jean-Philippe Bernardy, and
Cătălin Hrițcu.
Dynamic IFC Theorems for Free!
In 34nd
IEEE Computer Security Foundations Symposium (CSF), pages 1--14. 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.
Talks
Here are my recent and upcoming talks. For a complete list of my talks please look here.
- Formally Verified Security
- Formally Secure Compilation of Unsafe C Compartments
- Certified Programs and Proofs, CPP
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- The Next 700 Relational Program Logics
- Everest All Hands: slides (2019-10-11)
- Dijkstra Monads for All
- 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.
- Upcoming: Foundations of Programming Languages, Verification, and Security course at Ruhr University Bochum, October 2023--February 2024
- Recent: Proofs are Programs course at Ruhr University Bochum, March--July 2023
- 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
- 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
