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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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.
  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

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Cătălin Hrițcu, Jan Schwinghammer. A Step-indexed Semantics of Imperative Objects. Logical Methods in Computer Science (LMCS), 5(4), December 2009.

Books

  1. 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.
  2. 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

  1. 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

  1. David Chisnall, Deepak Garg, Cătălin Hrițcu, Mathias Payer.
    Secure Compilation (Dagstuhl Seminar 21481). Dagstuhl Reports 11(10):173–204, 2021.
  2. 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
  3. 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.
  4. Amal Ahmed, Deepak Garg, Cătălin Hrițcu, Frank Piessens.
    Secure Compilation (Dagstuhl Seminar 18201). Dagstuhl Reports 8(5): 1-30, 2018.

Theses

  1. Cătălin Hrițcu. The Quest for Formally Secure Compartmentalizing Compilation.
    Habilitation Thesis, ENS Paris, January 2019.
  2. 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.
  3. 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.

Drafts, Informal Publications, and Workshops

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.