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.
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
- Conference: 25-28 June 2019, Stevens Institute of Technology, Hoboken, NJ, USA
- Program Verification with F* course at Summer School on
Verification Technology, Systems, and Applications, VSTA 2019
- School: 1-5 July 2019 at University of Luxembourg
- Writing and Verifying Functional Programs in Coq course at Summer School
on Cryptography, Blockchain, and Program Verification, Mathinfoly 2019
- Application deadline: 26 May 2019
- School: 24-31 August 2019 at INSA, Lyon, France
- Certified Programs and Proofs, CPP 2020 (PC Co-Chair)
- Abstract deadline: 16 October 2019
- Submission deadline: 21 October 2019
- Conference: 20-21 January 2020, New Orleans, Louisiana, USA
- Dagstuhl Seminar 20201 on Secure Compilation (Co-Organizer)
- Seminar: 10-15 May, 2020, Schloss Dagstuhl, Germany
- Runtime Verification, RV 2019 (PC member)
- Submission deadline: 21 May 2019
- Conference: 8-11 October 2019, Porto, Portugal
- IEEE Cybersecurity Development Conference, SecDev 2019 (PC member)
- Conference: 25 - 27 September 2019, McLean, VA, USA
-
Habilitation defense on Tuesday, 29 January 2019 at Inria Paris
(Thesis)
-
Principles of Programming Languages, POPL 2019
(Artifact Evaluation Co-Chair)
- ACM Conference Computer and Communications Security, CCS 2018 (PC member)
- Formally Secure Compartmentalizing Compilation course at
International School on Foundations of Security Analysis and Design (FOSAD 2018)
- Working Formal Methods Symposium, FROM 2018 (Invited Speaker)
- Dagstuhl Seminar 18201 on Secure Compilation (Co-Organizer)
- European Symposium on Programming, ESOP 2018 (PC member)
- IEEE European Symposium on Security and Privacy, EuroS&P 2018 (PC member)
- Principles of Secure Compilation, PriSC @ POPL 2018 (PC Chair, Co-organizer)
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:
- Kenji Maillard (PhD Student, ENS Paris)
- Carmine Abate (PhD Student, Inria Paris)
- Jérémy Thibault (PhD Student, Inria Paris)
- Guido Martínez (Co-Supervised PhD Student, CIFASIS-CONICET Rosario)
- Exequiel Rivas (Starting Researcher Position)
- Roberto Blanco (Postdoctoral Researcher)
- Florian Groult (Research Engineer)
- Théo Laurent (Research Engineer)
- Antoine Van Muylder (Research Intern, Paris 7 University)
- Cezar Constantin Andrici (Research Intern / Engineer, University of Iasi, starting in July 2019)
- Ramkumar Ramachandra (Research Intern / Engineer, starting in August 2019)
- Éric Tanter (Visiting Professor, University of Chile, returning in August 2019)
- Adrien Durier (Postdoctoral Researcher, starting in fall 2019)
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,
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.
To appear 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, 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.
-
Niklas Grimm,
Kenji Maillard,
Cédric Fournet,
Cătălin Hriţcu,
Matteo Maffei,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem Rastogi,
Nikhil Swamy, and
Santiago Zanella-Béguelin.
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations.
In 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 130--145, January 2018
Talks
Here are my recent and upcoming talks. For a complete list of my talks please look here.
- The Quest for Formally Secure Compartmentalizing Compilation
- Journey Beyond Full Abstraction:
Exploring Robust Property Preservation for Secure Compilation
- Verified Effectful Programming in F*
- When Good Components Go Bad
- What is secure compilation?
- Principles of Secure Compilation, PriSC'18
- Program Chair's Welcome Message: slides (2018-01-13)
- What's new in F*?
- Presentation of Inria Prosecco team
- European Symposium on Security and Privacy, EuroS&P 2017
- General Chair's Welcome Message: slides (2017-04-26)
- Efficient Formally Secure Compilers to a Tagged Architecture
Teaching
Here are my recent courses. For a complete list of my teaching please look here.
- Upcoming: 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
- Upcoming: 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
