Cătălin Hriţcu
Starting in May 2011 I am Research Associate at
the University of Pennsylvania,
working on the CRASH/SAFE
project under the guidance
of Benjamin
C. Pierce. I'm a member of
the Penn PL Club.
I received my PhD (summa cum laude)
from Saarland
University. While in Saarbrücken, I was a member of
the Information
Security and Cryptography Group and held fellowships
from the International Max Planck
Research School for Computer Science
and Microsoft
Research Cambridge. My current webpage is still
hosted here.
Contact
E-mail (preferred): catalin.hritcu@gmail.com
Office: Towne 223
Address:
University of Pennsylvania,
3330 Walnut Street,
Philadelphia, PA 19104-6389
News
Research Interests
My research is primarily focused on developing rigorous formal
techniques for solving security problems. I am
particularly interested in:
-
formal methods for computer and network security:
security protocols,
privacy,
anonymity,
zero-knowledge,
information flow control,
access control,
integrity protection
-
programming-languages techniques:
rigorous semantics,
type systems,
verification,
automatic testing,
formal metatheory,
formally certified tools
-
design and verification of security-critical systems:
microkernel components,
electronic voting systems,
crypto devices,
security-preserving compilers,
mobile devices,
etc.
Recent Publications and Drafts
For a complete list of my publications please look here
(also on Google Scholar).
- Cătălin Hriţcu,
John Hughes,
Benjamin C. Pierce,
Antal Spector-Zabusky,
Dimitrios Vytiniotis,
Arthur Azevedo de Amorim,
Leonidas Lampropoulos. Testing Noninterference, Quickly. Submitted to ICFP 2013. March 2013.
- 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), May 2013. To appear.
-
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.
- 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.
- 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.
- 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.
Recent and Upcoming Talks
For a complete list of my talks please look here.
- Upcoming: TBD
- Fresh:: All Your IFCException Are Belong To Us
- Fresh: Testing Noninterference, Quickly
- CRASH/SAFE: Clean-slate Co-design of a Secure Host Architecture
- All Your IFCException Are Belong To Us
- Poison-pills and dynamic information flow control
- On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
- Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis
- Thesis defense, Saarland University: slides (2012-01-10)
- Breeze: A Language For Writing Secure Software
- Union, Intersection, and Refinement Types and Reasoning about Type Disjointness for Analyzing Protocol Implementations
- Semantic Subtyping with an SMT Solver
Teaching
- Advanced Martial Arts in Coq
- CIS670 at UPenn, Fall 2012.
Guest lecturer for 2 lectures:
- Software Foundations
- CIS500 at UPenn, Spring 2012.
Guest lecturer for 6 lectures:
- Advanced Topics in Programming Languages
- CIS670 at UPenn, Fall 2011.
Guest lecturer for 2 lectures:
- Security
- Core Lecture, Saarland University, Winter 2010/11.
Guest lecturer for 1 lecture:
- Practical Aspects of Security Lecture
- Advanced Lecture, Saarland University, Summer 2009
(Best lecture award).
Guest lecturer for 3 lectures:
- Selected Topics of Information Security and Cryptography
- Seminar, Saarland University, Winter 2008/09.
Organizer; advised students on the following topic:
- Selected Topics of Information Security and Cryptography
- Seminar, Saarland University, Winter 2007/08.
Organizer; advised students on the following topics:
- Introduction to Computational Logic
- Core Lecture, Saarland University, Summer 2007.
Teaching assistant.
- Language-based Security
- Advanced Lecture, Saarland University, Winter 2006/07.
Teaching assistant; conducted weekly recitation sections.
Advised Students
- Sam Panzer & Nick Watson
- Senior design project at UPenn, 2011-10 to 2012-04:
Zephyr: A Content Management System in Breeze
- Alex Busenius
- Thorsten Tarrach
- Martin Grochulla
- New:
CRASH/SAFE:
clean-slate co-design of a secure
architecture, including novel hardware, zero-kernel operating
system, and programming language (team effort)
- New:
Breeze:
a programming language with dynamic information flow control
and label-based access control, with
Michael Greenberg, Ben Karel, Benoît Montagu,
Benjamin C. Pierce, Jesse A. Tov, and others
- F5: a tool-chain for RCF, with Thorsten Tarrach
- DVerify: a verification tool for the "M" language by Thorsten Tarrach
- Dminor: a type-checker using semantic subtyping with Gavin Bierman and Andy Gordon
- Expi2Java: an extensible code generator for security protocols by Alex Busenius
- Protocol transformation for achieving security despite compromise by Martin Grochulla
- Zero-knowledge type-checker with Stefan Lorenz, Kim Pecina and Thorsten Tarrach
Misc
