Cătălin Hriţcu

PhD student in Computer Science at Saarland University
Information Security and Cryptography Group

News

Starting in May 2011 I am Research Associate at the University of Pennsylvania, Department of Computer & Information Science, working on the CRASH/SAFE project under the supervision of Prof. Benjamin C. Pierce.

Office: Moore GRW 078

Office Phone: +1-215-898-5886

Address:

University of Pennsylvania
Department of Computer & Information Science
3330 Walnut Street
Philadelphia, PA 19104-6389

Research Interests

• Language-based Security
• Type systems
• Semantics of Programming Languages
• Verification
• Formal Methods in Software Engineering

Recent Publications and Drafts

Here is my complete list of publications (also on Google Scholar, MS Academic Search, and DBLP).

• Michael Backes, Alex Busenius, Cătălin Hriţcu. On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols. Accepted at 4th NASA Formal Methods Symposium (NFM 2012). 31 January 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.
• Michael Backes, Cătălin Hriţcu, and Matteo Maffei. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations, Submitted to special issue of the Journal of Computer Security (JCS) for TOSCA-SecCo, January 16, 2012.
  • Preliminary version to appear 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.
• Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy. Semantic Subtyping with an SMT Solver. To appear in Journal of Functional Programming, December 2011.
  • More information can be found on the Dminor project website at Microsoft Research.
  • An abridged version appeared in 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), September 2010
  • A Microsoft Research technical report (MSR-TR-2010-99) contains additional details and full proofs, December 2011.
  • The Dminor model and some of the proofs in this paper are formalized in Coq, November 2010.
• 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), December 2011.
  • Preliminary version presented at the BOOGIE 2011 workshop, July 2011.
  • Implementation, Coq proofs and additional details available on the page of the DVerify project.

Recent Talks

Here is my complete list of talks.

• Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis
  • Thesis defense, Saarland University: slides (2012-01-10)
• Featherweight Breeze
  • Guest Lecturer in Benjamin Pierce's Advanced Topics in Programming Languages Lecture (2011-11-30 and 2011-12-05)
• Breeze: A Language For Writing Secure Software
  • Stevens Institute of Technology: (2011-11-28)
• Union, Intersection, and Refinement Types and Reasoning about Type Disjointness for Analyzing Protocol Implementations
  • Penn PLClub: slides (2011-07-20)
  • MSR-INRIA Joint Centre, Parc Orsay Université: slides (2010-12-07)
• Control Hijacking: Defenses
  • Guest Lecturer in Michael Backes' Security Lecture: slides (2010-10-28)
  • Guest Lecturer in Michael Backes' Practical Aspects of Security Lecture: slides (2009-05-22)
• Semantic Subtyping with an SMT Solver
  • 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010): slides; video (2010-09-27)
  • Workshop on Relations and Data Integrity Constraints and Languages (RADICAL 2010): slides; video
    (2010-05-10)
  • Information Security and Cryptography Group: slides (2009-12-16)

Students

• Alex Busenius
  • Master's Thesis, Finished 2011-04-04:
    Mechanized Formalization of a Transformation from an Extensible Spi Calculus to Java
  • Bachelor's Thesis, Finished 2008-10-28:
    Expi2Java - An Extensible Code Generator for Security Protocols
[First employment Capgemini]
• Thorsten Tarrach
  • Master's Thesis, Finished 2010-08-31:
    Automatically Verifying "M" Modeling Language Constraints
  • Bachelor's Thesis, Finished 2008-10-27:
    Spi2F# - A Prototype Code Generator for Security Protocols
[First employment Troxo/Atomia]
• Martin Grochulla
  • Master's Thesis, Finished 2009-01-06 (co-advised with Matteo Maffei)
    Security Despite System Compromise with Zero-Knowledge Proofs
[Now PhD student at the MPI-INF]

Tools

• New: F5: a tool-chain for RCF, with Thorsten Tarrach
• New: DVerify: a verification tool for the "M" language by Thorsten Tarrach
• New: Dminor: a type-checker using semantic subtyping with Andy Gordon, Gavin Bierman, and Dave Langworthy
• Expi2Java: an extensible code generator for security protocols by Alex Busenius
• Protocol transformation for achieving security despite compromise by Martin Grochulla
• Spi2F#: a prototype code generator for security protocols by Thorsten Tarrach
• Zero-knowledge type-checker with Stefan Lorenz, Kim Pecina and Thorsten Tarrach

Teaching Assistant

• Software Foundations - UPenn CIS500, Spring 2012
• Practical Aspects of Security - Advanced Lecture, Summer 2009 (Best lecture award)
• Selected Topics of Information Security and Cryptography - Seminar, Winter 2008/09
• Selected Topics of Information Security and Cryptography - Seminar, Winter 2007/08
• Introduction to Computational Logic - Core Lecture, Summer 2007
• Language-based Security - Advanced Lecture, Winter 2006/07

Contact

E-mail (preferred): catalin.hritcu@gmail.com

(More ways to find me)

Misc

• My curriculum vitae
• My blog (Smiling)
• Pronouncing my name: /kətəlin hritsku/, mp3, aiff
• Spelling my name in LaTeX: C\u{a}t\u{a}lin Hri\c{t}cu
• Spelling my name in HTML: Cătălin Hriţcu