Cătălin Hrițcu
Institution: Max Planck Institute for Security and Privacy / CASA
Research Hub(s):
Hub A: Future Cryptography
Hub B: Embedded Security
Hub C: Secure Systems
E-Mail: Catalin.Hritcu@mpi-sp.org
Website: https://www.mpi-sp.org/hritcu
Twitter: @chritcu
Publications:
SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking Simulation SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F* SECOMP: Formally Secure Compilation of Compartmentalized C Programs Securing Verified IO Programs Against Unverified Code in F* Short Paper: Mechanized Proofs of Masking Security The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs Dynamic IFC Theorems for Free! SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq FSLH: Flexible Mechanized Speculative Load Hardening
