back to home page

Cătălin Hrițcu

Publications

bibtex file

Conference Papers

1. Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Cătălin Hrițcu, and Andrew Tolmach. SECOMP: Formally Secure Compilation of Compartmentalized C Programs. Accepted at CCS'24, Draft from July 2024.
   • Coq development
   • An extended abstract about this work was presented at PriSC'23
2. 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*. To appear in PACMPL, 8(POPL):74:1--74:34, January 2024.
   • F* development
   • An extended abstract about this work was presented at PriSC'23
3. 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. To appear in ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). January 2024.
   • Coq development
4. 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.
   • Coq development
5. 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.
   • Superseded by journal paper with the same name, see below.
   • Coq development
   • CSF 2021 presentation video and slides; Coq Workshop 2021 presentation; and TYPES 2021 presentation
6. 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.
   • Agda development
7. 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.
   • Coq development
   • Superseded by journal paper entitled "An Extended Account of Trace-relating Compiler Correctness and Secure Compilation", see below.
8. 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.
   • Proof-of-concept implementation in Coq
9. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martinez, Cătălin Hrițcu, Exequiel Rivas, and Éric Tanter. Dijkstra Monads for All. PACMPL, 3(ICFP):104:1– 104:29, August 2019.
   • Verification examples and the implementation of our framework in F*
   • Verification examples and a formalization in Coq
10. 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.
    • Coq development
    • A previous extended abstract was called Robust hyperproperty preservation for secure compilation
11. 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.
12. 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.
    • Coq development
    • A previous extended abstract was called Formally Secure Compilation of Unsafe Low-Level Components
13. 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
14. 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, PACMPL, 2(POPL):65:1-65:30, January 2018.
    • Online appendices and software artifacts
15. 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
    • Code for the examples
16. Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hrițcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy, Verified Low-Level Programming Embedded in F*. In 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), PACMPL, 1(ICFP):17:1–17:29, September 2017.
17. Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Cătălin Hrițcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, and Jean-Karim Zinzindohoué. Everest: Towards a Verified, Drop-in Replacement of HTTPS. 2nd Summit on Advances in Programming Languages (SNAPL), May 2017.
18. Danel Ahman, Cătălin Hrițcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra Monads for Free. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 515--529. ACM, January 2017.
19. Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hrițcu, John Hughes, Benjamin C. Pierce, Li-yao Xia. Beginner's Luck: A Language for Random Generators. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), pages 114--129. ACM, January 2017.
20. Yannis Juglaret, Cătălin Hrițcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF). To appear. arXiv:1602.04503. Author Preprint of May 6 2016.
    • A draft version of the paper was entitled Beyond Full Abstraction
21. Nikhil Swamy, Cătălin Hrițcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin. Dependent Types and Multi-Monadic Effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256-270, January 2016.
22. Zoe Paraskevopoulou, Cătălin Hrițcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP), volume 9236 of Lecture Notes in Computer Science, pages 325-343. Springer, August 2015.
23. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hrițcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy (Oakland S&P), pages 813-830. IEEE Computer Society, May 2015.
    • Coq proofs
24. Udit Dhawan, Cătălin Hrițcu, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and André DeHon. Architectural Support for Software-Defined Metadata Processing. In 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 487-502. ACM, March 2015.
25. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 165-178. ACM, January 2014.
    • Superseded by journal paper with the same name, see below.
26. Cătălin Hrițcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos. Testing Noninterference, Quickly. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP). pages 455-468, ACM Press. September 2013.
    • Superseded by journal paper with the same name, see below.
27. Cătălin Hrițcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy (Oakland), pages 3-17, IEEE Computer Society Press, May 2013.
    • Coq formalization and proofs are available here.
    • Breeze interpreter, libraries, and sample applications are available here.
    • A previous version of this work was called Exceptionally Available Dynamic IFC, July 2012.
28. Michael Backes, Alex Busenius, Cătălin Hrițcu. On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. 4th NASA Formal Methods Symposium (NFM 2012), pages 371-387, April 2012.
    • Online appendix containing details that had to be omitted in the NFM paper due to the lack of space.
    • Implementation, case studies, documentation, Coq formalization, and proofs are all available on the page of the expi2java project.
29. Michael Backes, Cătălin Hrițcu, and Thorsten Tarrach. Automatically Verifying Typing Constraints for a Data Processing Language. In First International Conference on Certified Programs and Proofs (CPP 2011), pages 296-313, Springer, December 2011.
    • Implementation, full Coq proofs and additional details available on the page of the DVerify project.
    • Preliminary version presented at the BOOGIE 2011 workshop, July 2011.
30. Michael Backes, Cătălin Hrițcu, and Matteo Maffei. Union and Intersection Types for Secure Protocol Implementations. In Theory of Security and Applications (TOSCA'11), Invited paper, April 2011.
    • Superseded by journal paper entitled "Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations", see below.
31. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hrițcu, David Langworthy. Semantic Subtyping with an SMT Solver, In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), September 2010.
    • Superseded by journal paper with the same name, see below.
32. Michael Backes, Martin Grochulla, Cătălin Hrițcu, and Matteo Maffei. Achieving Security Despite Compromise Using Zero-knowledge. In 22th IEEE Symposium on Computer Security Foundations (CSF 2009), pages 308-323, IEEE Computer Society Press, July 2009.
    • Full version that contains all the technical details, March 2009.
    • Prototype of the protocol transformation by Martin Grochulla, March 2009.
    • A preliminary version of this paper was presented at ARSPA-WITS'09, March 2009.
33. Michael Backes, Cătălin Hrițcu, and Matteo Maffei. Type-checking Zero-knowledge. In 15th ACM Conference on Computer and Communications Security (CCS 2008), pages 357-370, ACM Press, October 2008.
    • Machine-checked soundness proof in Coq by Cătălin Hrițcu, May 2011.
    • Full version that additionally contains all the technical details of the type system, a brief discussion about security despite compromise, and all the proofs, November 2008.
    • Implementation of the type-checker for zero-knowledge by Stefan Lorenz, Kim Pecina, Cătălin Hrițcu, and Thorsten Tarrach, September 2008.
    • A preliminary version of this paper was presented at FCS-ARSPA-WITS'08, June 2008.
34. Michael Backes, Cătălin Hrițcu, and Matteo Maffei. Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In 21th IEEE Symposium on Computer Security Foundations (CSF 2008), pages 195-209, IEEE Computer Society Press, June 2008.

Journal Papers

35. 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.
    • Conference version won Distinguished Paper Award at CSF 2021
    • Coq development
    • CSF 2021 presentation video and slides; Coq Workshop 2021 presentation; and TYPES 2021 presentation
36. 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. An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation. ACM Transactions on Programming Languages and Systems (TOPLAS). Volume 43, Issue 4, pages 1-48. ACM, December 2021.
    • Coq development
37. Cătălin Hrițcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, and Dimitrios Vytiniotis. Testing Noninterference, Quickly. Special Issue of Journal of Functional Programming (JFP) for ICFP 2013. 26:e4 (62 pages), April 2016.
    • Testing code
38. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hrițcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. Journal of Computer Security (JCS); Special Issue on Verified Information Flow Security, 24(6):689--734, December 2016.
    • Coq proofs
39. Michael Backes, Cătălin Hrițcu, and Matteo Maffei. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations, Journal of Computer Security (JCS); Special Issue on Foundational Aspects of Security, 22(2):301-353, February, 2014.
    • Preliminary version appeared in Theory of Security and Applications (TOSCA'11), Invited paper, April 2011.
    • Machine-checked soundness proof in Coq by Cătălin Hrițcu, February 2011.
    • Prototype implementation (F5) by Thorsten Tarrach and Cătălin Hrițcu, November 2010.
40. Gavin M. Bierman, Andrew D. Gordon, Cătălin Hrițcu, David Langworthy. Semantic Subtyping with an SMT Solver. Journal of Functional Programming, 22(1):31-105, Cambridge University Press, March 2012.
    • The Dminor implementation is still available via the Internet Archive Wayback Machine
    • A recent independent implementation of the Dminor type system is available in the formulog project.
    • More information can be found on the Dminor project website, which is also still available via the Wayback Machine.
    • An abridged version appeared at ICFP 2010, September 2010
    • The Dminor model and some of the proofs in this paper are formalized in Coq, November 2010.
41. Cătălin Hrițcu, Jan Schwinghammer. A Step-indexed Semantics of Imperative Objects. Logical Methods in Computer Science (LMCS), 5(4), December 2009.
    • A preliminary version of this work was presented at the Workshop on Foundations of Object-Oriented Languages (FOOL'08), January 2008.

Books

42. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations: Logical Foundations, Electronic textbook, August 2018.
43. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hrițcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Software Foundations: Programming Language Foundations, Electronic textbook, August 2018.

Book Chapter

44. Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hrițcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Luck: A Probabilistic Language for Testing. Foundations of Probabilistic Programming, pages 449-488. Cambridge University Press. November 2020.

Editor

45. David Chisnall, Deepak Garg, Cătălin Hrițcu, Mathias Payer.
    Secure Compilation (Dagstuhl Seminar 21481). Dagstuhl Reports 11(10):173–204, 2021.
46. Cătălin Hrițcu and Andrei Popescu, editors. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, Virtual Event, Denmark, January 17-19, 2021. ACM 2021
47. Jasmin Blanchette and Cătălin Hrițcu, editors. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. ACM, 2020.
48. Amal Ahmed, Deepak Garg, Cătălin Hrițcu, Frank Piessens.
    Secure Compilation (Dagstuhl Seminar 18201). Dagstuhl Reports 8(5): 1-30, 2018.

Theses

49. Cătălin Hrițcu. The Quest for Formally Secure Compartmentalizing Compilation.
    Habilitation Thesis, ENS Paris, January 2019.
    • Main Coq formalizations available here and here
50. Cătălin Hrițcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD Thesis, Saarland University, Jan 2012.
    • Coq formalizations, implementations, samples, and further details available on the pages of the Zero-knowledge Type-checker and of the F5 Toolchain for RCF.
51. Cătălin Hrițcu. Step-indexed Semantic Model of Types for the Functional Object Calculus. Master's Thesis, Saarland University, Saarbrücken, Germany, May 2007.
    • Awarded the Günter-Hotz Medal by the "Freunde der Saarbrücker Informatik".

Drafts, Informal Publications, and Workshops

52. Roberto Blanco, Christian Doczkal, Jakob Feldtkeller, Tim Güneysu, and Cătălin Hrițcu. Short Paper: Mechanized Proofs of Masking Security. 18th Workshop on Programming Languages and Analysis for Security (PLAS 2023 at CCS 2023). November 2023.
53. 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.
    • F* development
54. 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.
    • Coq development
55. Jérémy Thibault and Cătălin Hrițcu. Nanopass back-translation of multiple traces for secure compilation proofs. Extended Abstract at Workshop on Principles of Secure Compilation (PriSC), January 2021.
56. Alejandro Aguirre, Cătălin Hrițcu, Chantal Keller, and Nikhil Swamy. From F* to SMT (extended abstract). Talk at 1st International Workshop on Hammers for Type Theories (HaTT), July 2016.
    • Detailed report on Alejandro's Master's internship: Towards a Provably Correct Encoding from F* to SMT
    • Unpublished "Rough Diamond" that supersedes the HaTT extended abstract above
57. Udit Dhawan, Albert Kwon, Edin Kadric, Cătălin Hrițcu, Benjamin C. Pierce, Jonathan M. Smith, Gregory Malecha, Greg Morrisett, Thomas F. Knight, Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan, and André DeHon, Hardware Support for Safety Interlocks and Introspection. In SASO Workshop on Adaptive Host and Network Security, September 2012.