Trustworthy Protocols and Systems

The security universe includes a large class of computer systems (cryptographic protocols, trusted computing systems, hypervisors, virtual machine monitors, and Web browsers, to name a few) that are designed to provide security properties in the presence of actively interfering adversaries. A unifying theme of this work is to develop theories of security that include formal models of systems, adversaries, and properties, and support rigorous analyses indicating that the system satisfies the intended security property or identifying attacks on it. Given the complexity of these systems, two central classes of techniques that we have developed to achieve scalability are (a) composition techniques that enable us to conduct security analysis of complex systems by analyzing the smaller components from which they are built; and (b) abstraction techniques that enable us to reduce the security analysis of a complex system to that of a simpler system. The techniques are provably sound, i.e. no attacks are missed by applying them. We have applied these techniques to several classes of systems: (a) trusted computing systems - proving attestation properties and discovering a composition attack on two standard protocols; (b) hypervisors -discovering attacks that violate address separation properties and proving absence of attacks on the fixed designs; (c) network protocols – proving authentication and confidentiality properties of the OpenSSL handshake implementation and rediscovering a version rollback attack on it.

We are also exploring the formal foundations of trustworthy systems were programs and people interact. A specific problem in this area that we are working on is usable and secure password management.

Compositional Security

A. Datta, J. Franklin, D. Garg, L. Jia, D. Kaynar, On Adversary Models and Compositional Security, IEEE Security & Privacy 9(3): 26-32 (2011) (Special Issue on the Science of Security) . [ Paper]

D. Garg, J. Franklin, D. Kaynar, A. Datta, Compositional System Security with Interface-Confined Adversaries, in Proceedings of 26th Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, May 2010. [ Paper] [ Full Version ] Invited Paper
A. Datta, J. Franklin, D. Garg, D. Kaynar, A Logic of Secure Systems and its Application to Trusted Computing, in Proceedings of 30th IEEE Symposium on Security and Privacy, May 2009. [ Paper ] [Full Version]
D. Garg, J. Franklin, D. Kaynar, A. Datta, A Logic for Reasoning about Networked Secure Systems, in Joint Workshop FCS-ARSPA-WITS (co-located with CSF 2008 and LICS 2008), June 2008. [ Paper ] [ Full Version ]

Our other projects on compositional security

· Protocol Composition Logic(PCL) (Applications: Industrial authentication and key exchange protocols)

· Program Equivalence, Games and Universal Composability

Abstractions for Reasoning about System Security

J. Franklin, Abstractions for Model Checking System Security, PhD Dissertation, Computer Science Department, CMU, May 2012.
J. Franklin, S. Chaki, A. Datta, J. McCune, A. Vasudevan, Parametric Verification of Address Space Separation, in Proceedings of ETAPS Conference on Principles of Security and Trust, March 2012. [ Paper] [Full Version] ETAPS Best Paper Nominee
J. Franklin, S. Chaki, A. Datta, A. Seshadri, Scalable Parametric Verification of Secure Systems: How to Verify Reference Monitors without Worrying about Data Structure Size, in Proceedings of 31^st IEEE Symposium on Security and Privacy, May 2010. [ Paper ]
S. Chaki, A. Datta, ASPIER: An Automated Framework for Verifying Security Protocol Implementations, in Proceedings of 22nd IEEE Computer Security Foundations Symposium, July 2009. [ Paper ]

Usable and Secure Password Management [Project Page]

· J. Blocki, M. Blum, A. Datta, Self-Rehearsing Passwords, Working Paper, November 2012.