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 2024
(PC Member)
- Submission deadline: 11 July 2013
- Symposium: 17-19 January 2024, London, UK
- Computer Security Foundations, CSF (Test-of-Time Awards Chair in 2023 and 2024)
- Symposium (CSF 2023): 10-13 July 2023, Dubrovnik, Croatia
- Certified Programs and Proofs, CPP (Steering Committee Chair, since 2021)
- Principles of Secure Compilation, PriSC (Steering Committee Chair, since 2019)
- 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 Martinez, 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
- Certified Programs and Proofs, CPP 2020 and 2021 (PC & Conference Chair)
- Computer Security Foundations, CSF 2020 and 2021 (PC member)
-
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 (W2 Research Group Leader with Tenure).
- Distinguished Paper Award at CSF 2019 for Journey Beyond Full Abstraction
-
Principles of Programming Languages, POPL 2018 & 2019
(Artifact Evaluation Chair)
E-mail: 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,
Cătălin Hrițcu,
Guido Martínez,
Exequiel Rivas, and
Théo Winterhalter.
Securely Compiling Verified F* Programs With IO. Submitted to ICFP'23. March 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.
Submitted to CSF'23. 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.
-
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.
-
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.
In 34th
IEEE Computer Security Foundations Symposium (CSF), pages 608--622. June 2021.
Distinguished Paper Award.
-
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.
-
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.
Talks
Here are my recent and upcoming talks. For a complete list of my talks please look here.
- Formally Secure Compilation of Unsafe C Compartments
- Certified Programs and Proofs, CPP
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- Formally Verified Security
- 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: Proofs are Programs course at Ruhr University Bochum, 6 March--13 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
