Catalin Hritcu

According to our database, Catalin Hritcu authored at least 58 papers between 2005 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Securing Verified IO Programs Against Unverified Code in F.

Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter

Proc. ACM Program. Lang., January, 2024

SECOMP: Formally Secure Compilation of Compartmentalized C Programs.

Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach

CoRR, 2024

2023

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters

ACM Trans. Program. Lang. Syst., September, 2023

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters

IACR Cryptol. ePrint Arch., 2023

Securely Compiling Verified F* Programs With IO.

Cezar-Constantin Andrici, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Théo Winterhalter

CoRR, 2023

2022

SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation.

Akram El-Korashy, Roberto Blanco, Jérémy Thibault, Adrien Durier, Deepak Garg, Catalin Hritcu

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation.

Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault

ACM Trans. Program. Lang. Syst., 2021

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters

IACR Cryptol. ePrint Arch., 2021

Secure Compilation (Dagstuhl Seminar 21481).

David Chisnall, Deepak Garg, Catalin Hritcu, Mathias Payer

Dagstuhl Reports, 2021

Dynamic IFC Theorems for Free!

Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

The next 700 relational program logics.

Kenji Maillard, Catalin Hritcu, Exequiel Rivas, Antoine Van Muylder

Proc. ACM Program. Lang., 2020

Trace-Relating Compiler Correctness and Secure Compilation.

Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault

Proceedings of the Programming Languages and Systems, 2020

2019

Dijkstra monads for all.

Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter

Proc. ACM Program. Lang., 2019

Trace-Relating Compiler Correctness and Secure Compilation.

Carmine Abate, Roberto Blanco, Stefan Ciobaca, Deepak Garg, Catalin Hritcu, Marco Patrignani, Éric Tanter, Jérémy Thibault

CoRR, 2019

Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy

Proceedings of the Programming Languages and Systems, 2019

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, Jérémy Thibault

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

The Quest for Formally Secure Compartmentalizing Compilation.

Catalin Hritcu

, 2019

2018

Recalling a witness: foundations and applications of monotonic state.

Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy

Proc. ACM Program. Lang., 2018

Secure Compilation (Dagstuhl Seminar 18201).

Amal Ahmed, Deepak Garg, Catalin Hritcu, Frank Piessens

Dagstuhl Reports, 2018

Exploring Robust Property Preservation for Secure Compilation.

Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, Jérémy Thibault

CoRR, 2018

Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.

Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Catalin Hritcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy

CoRR, 2018

The Meaning of Memory Safety.

Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce

Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.

Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin

Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise.

Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Andrew Tolmach

Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017

Verified low-level programming embedded in F.

Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy

Proc. ACM Program. Lang., 2017

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract).

Deepak Garg, Catalin Hritcu, Marco Patrignani, Marco Stronati, David Swasey

CoRR, 2017

Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract).

Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach

CoRR, 2017

A Monadic Framework for Relational Verification (Functional Pearl).

Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin

CoRR, 2017

Verified Low-Level Programming Embedded in F^*.

Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy

CoRR, 2017

Everest: Towards a Verified, Drop-in Replacement of HTTPS.

Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue

Proceedings of the 2nd Summit on Advances in Programming Languages, 2017

Beginner's luck: a language for property-based generators.

Leonidas Lampropoulos, Diane Gallois-Wong, Catalin Hritcu, John Hughes, Benjamin C. Pierce, Li-yao Xia

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Dijkstra monads for free.

Danel Ahman, Catalin Hritcu, Kenji Maillard, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Testing noninterference, quickly.

Catalin Hritcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo de Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis

J. Funct. Program., 2016

A verified information-flow architecture.

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

J. Comput. Secur., 2016

Beyond Full Abstraction: Formalizing the Security Guarantees of Low-Level Compartmentalization.

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce

CoRR, 2016

Dijkstra Monads for Free.

Danel Ahman, Catalin Hritcu, Guido Martínez, Gordon D. Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy

CoRR, 2016

Dependent types and multi-monadic effects in F.

Nikhil Swamy, Catalin Hritcu, 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

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation.

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, Benjamin C. Pierce

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015

The Joint EasyCrypt-F*-CryptoVerif School 2014.

Catalin Hritcu

ACM SIGLOG News, 2015

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components.

Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach

CoRR, 2015

Micro-Policies: Formally Verified, Tag-Based Security Monitors.

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach

Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Foundational Property-Based Testing.

Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Micro-Policies: Formally Verified, Tag-Based Security Monitors.

Catalin Hritcu

Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, 2015

Architectural Support for Software-Defined Metadata Processing.

Udit Dhawan, Catalin Hritcu, Raphael Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight Jr., Benjamin C. Pierce, André DeHon

Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, 2015

2014

Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations.

Michael Backes, Catalin Hritcu, Matteo Maffei

J. Comput. Secur., 2014

2013

All Your IFCException Are Belong to Us.

Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, Greg Morrisett

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Testing noninterference, quickly.

Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

2012

Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis.

Catalin Hritcu

PhD thesis, 2012

Semantic subtyping with an SMT solver.

Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, David E. Langworthy

J. Funct. Program., 2012

Hardware Support for Safety Interlocks and Introspection.

Udit Dhawan, Albert Kwon, Edin Kadric, Catalin Hritcu, Benjamin C. Pierce, Jonathan M. Smith, André DeHon, Gregory Malecha, Greg Morrisett, Thomas F. Knight Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David K. Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan

Proceedings of the Sixth IEEE International Conference on Self-Adaptive and Self-Organizing Systems Workshops, 2012

On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols.

Michael Backes, Alex Busenius, Catalin Hritcu

Proceedings of the NASA Formal Methods, 2012

2011

Union and Intersection Types for Secure Protocol Implementations.

Michael Backes, Catalin Hritcu, Matteo Maffei

Proceedings of the Theory of Security and Applications - Joint Workshop, 2011

Automatically Verifying Typing Constraints for a Data Processing Language.

Michael Backes, Catalin Hritcu, Thorsten Tarrach

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2009

A Step-indexed Semantics of Imperative Objects

Catalin Hritcu, Jan Schwinghammer

Log. Methods Comput. Sci., 2009

Achieving Security Despite Compromise Using Zero-knowledge.

Michael Backes, Martin P. Grochulla, Catalin Hritcu, Matteo Maffei

Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

2008

Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus.

Michael Backes, Catalin Hritcu, Matteo Maffei

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Type-checking zero-knowledge.

Michael Backes, Catalin Hritcu, Matteo Maffei

Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2005

A Reference Implementation of ADF (Agent Developing Framework): Semantic Web-Based Agent Communication.

Catalin Hritcu, Sabin C. Buraga

Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2005), 2005