The Cryptyc Project

Types for control patterns not just data structures

A joint project between Andy Gordon (MSRC) and Alan Jeffrey (DePaul University)

• Type systems for data structures in programming language have been getting better and gaining wider currency in the past ten years: witness the use of types in the JVM and the CLR for security and to enable automatic memory management.
• We believe that current research on type systems for control patterns is set to have a similarly big impact in the next ten years. Because of a variety of technological trends, we’re going to be writing more concurrent and security-critical code, and hence facing more concurrency bugs and security bugs. Types for control patterns are a new idea for catching such bugs, early, during the type-checking phase.
• Example: Cryptyc, a tool for type-checking security protocols.
• Embedded assertions make explicit the security goals of a protocol (e.g., authentication, key agreement, etc)
• Novel data types include trust information (e.g., whether data is secret, what beliefs conveyed by a random number challenge)
• Novel control types regulate runtime behaviour (e.g., can guarantee reliability of a challenge-response handshake)
• A soundness theorem asserts that the assertions embedded in any well-typed protocol are valid, even in the presence of an untyped, malicious opponent.
• Hence, the Cryptyc type-checker allows us to write and debug the security goals of protocols via a conventional code/type-check/debug cycle, without relying on more heavyweight tools like model-checkers or theorem-provers.
• We have successfully evaluated Cryptyc on a range of symmetric key protocols; work on larger class in progress.
• For an introduction, browse this talk
• Two papers appear at the IEEE Computer Security Foundations Workshop (at CSFW'01 and at CSFW'02).
• For more detail, see the Technical Reports MSR-TR-2001-48 and MSR-TR-2001-49, May 2001.