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.
Our other projects on compositional security
· Protocol Composition Logic(PCL) (Applications: Industrial authentication and key exchange protocols)
Abstractions for Reasoning about System Security
Usable and Secure Password Management [Project Page]