Cătălin Hrițcu
Researcher (tenured, chargé de recherche)
at Inria Paris
in the Prosecco team.
Until September 2013 I was 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
- Distinguished Paper Award at CSF 2019 for Journey Beyond Full Abstraction
- Certified Programs and Proofs, CPP 2020 (PC Chair)
- Conference: 20-21 January 2020, New Orleans, Louisiana, USA
- Computer Security Foundations, CSF 2020 (PC member)
- Submission deadlines(!): 4 October 2019 and 7 February 2020
- Conference: June 2020, Boston, MA, USA
- Dagstuhl Seminar 20201 on Secure Compilation (Co-Organizer)
- Seminar: 10-15 May, 2020, Schloss Dagstuhl, Germany
- Runtime Verification, RV 2019 (PC member)
- IEEE Cybersecurity Development Conference, SecDev 2019 (PC member)
- Writing and Verifying Functional Programs in Coq course at Summer School
on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019
- Program Verification with F* course at Summer School on
Verification Technology, Systems, and Applications, VSTA 2019
-
Habilitation defense on Tuesday, 29 January 2019 at Inria Paris
(Thesis)
-
Principles of Programming Languages, POPL 2019
(Artifact Evaluation Co-Chair)
E-mail (preferred): catalin.hritcu@gmail.com
Current address:
2 rue Simone Iff, 75012 Paris, France (How to reach us)
Equivalent Address (address above is so new that mapping applications might not know it):
43 Rue du Charolais, 75012 Paris, France
Office: C218 (building C, 2nd floor)
Postal address:
Inria Prosecco team,
Centre de Recherche Inria de Paris,
2 rue Simone Iff, CS 42112, 75589 Paris Cedex 12, France
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
Research Group
I am very fortunate to work with a group of outstanding students,
young researchers, and engineers:
For a complete list of present and 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).
-
Kenji Maillard,
Cătălin Hrițcu,
Exequiel Rivas, and
Antoine Van Muylder.
The Next 700 Relational Program Logics.
arXiv:1907.05244. Conditionally accepted at POPL 2020.
-
Carmine Abate,
Roberto Blanco,
Ștefan Ciobâcă,
Deepak Garg,
Cătălin Hrițcu,
Marco Patrignani,
Éric Tanter, and
Jérémy Thibault.
Trace-Relating Compiler Correctness and Secure Compilation.
arXiv:1907.05320. July 2019.
-
Kenji Maillard,
Danel Ahman,
Robert Atkey,
Guido Martinez,
Cătălin Hrițcu,
Exequiel Rivas, and
Éric Tanter.
Dijkstra Monads for All.
To appear in 24th ACM
SIGPLAN International Conference on Functional Programming (ICFP),
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), 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), 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.
- 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)
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- 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
