Anupam Datta

Associate Professor – CyLab ECECS
Department Electrical and Computer Engineering
Office 2118 Collaborative Innovation Center
Email
Website http://www.andrew.cmu.edu/user/danupam/
Assistant Kelley Conley

Research Interests

My research focuses on the scientific foundations of security and privacy. I formalize security and privacy properties, design mechanisms for enforcing these properties, and principled analysis techniques for rigorously demonstrating that proposed mechanisms achieve desired properties. Much of my work has focused on reducing reasoning about security to reasoning about programs with suitable abstractions of security mechanisms (e.g., cryptographic primitives, hardware-based security features) and adversary capabilities (e.g., see my work on cryptographic protocols and trustworthy systems). More recently, I have started formally investigating the role of people in security and privacy (e.g., see my work on privacy, audit, and accountability).

Privacy, Audit and Accountability

Privacy has become a significant concern in modern society as personal information about individuals is increasingly collected, used, and shared, often using digital technologies, by a wide range of organizations. One goal of this project is to precisely articulate what privacy means in various settings, and whether and how it can be achieved. In other words, we seek to develop conceptual and technical frameworks in which privacy notions (policies) are given precise semantics, algorithms for enforcing such policies, and characterizations of classes of policies that can or cannot be enforced. In addition to general results of this form, another goal of the project is to study specific application domains that raise significant privacy concerns in modern society and to apply these results (or specialized versions thereof) to these domains. Our current focus is on the healthcare domain. We are also thinking about privacy issues on the web and in online social media.

Specifically, to mitigate privacy concerns, organizations are required to respect privacy laws in regulated sectors (e.g., HIPAA in healthcare, GLBA in financial sector) and to adhere to self-declared privacy policies in self-regulated sectors (e.g., privacy policies of companies such as Google and Facebook in Web services). We investigate the possibility of formalizing and enforcing such practical privacy policies using computational techniques. We formalize privacy policies that prescribe and proscribe flows of personal information as well as those that place restrictions on the purposes for which a governed entity may use personal information. Recognizing that traditional preventive access control and information flow control mechanisms are inadequate for enforcing such privacy policies, we develop principled audit and accountability mechanisms with provable properties that seek to encourage policy-compliant behavior by detecting policy violations, assigning blame and punishing violators. We apply these techniques to several US privacy laws and organizational privacy policies, in particular, producing the first complete logical specification and audit of all disclosure-related clauses of the HIPAA Privacy Rule.

Trustworthy 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.

Cryptographic Protocols

Protocols that enable secure communication over an untrusted network constitute an important part of the current computing infrastructure. Common examples of such protocols are SSL, TLS, Kerberos, and the IPSec and IEEE 802.11i protocol suites. SSL and TLS are used by internet browsers and web servers to allow secure transactions in applications like online banking. The IPSec protocol suite provides confidentiality and integrity at the IP layer and is widely used to secure corporate VPNs. IEEE 802.11i provides data protection and integrity in wireless local area networks, while Kerberos is used for network authentication. The design and security analysis of such network protocols presents a difficult problem. In several instances, serious security vulnerabilities were uncovered in protocols many years after they were first published or deployed.

We have developed Protocol Composition Logic (PCL), a formal logic for proving security properties of such network protocols. Two central results for PCL are a set of composition theorems and a computational soundness theorem. In contrast to traditional folk wisdom in computer security, the composition theorems allow proofs of complex protocols to be built up from proofs of their constituent sub-protocols. The computational soundness theorem guarantees that, for a class of security properties and protocols, axiomatic proofs in PCL carry the same meaning as reduction-style cryptographic proofs. Tool implementation efforts are also underway. PCL and a complementary model-checking method have been successfully applied to a number of internet, wireless and mobile network security protocols developed by the IEEE and IETF Working Groups. This work identified serious security vulnerabilities in the IEEE 802.11i wireless security standard and the IETF GDOI standard. The suggested fixes have been adopted by the respective standards bodies.

In the News

  • ECE focus: computer security and privacy
  • Carnegie Mellon, 2007

    Research Area

    Computer Systems

    Education

    PhD, 2005
    Computer Science
    Stanford University

    MS, 2002
    Computer Science
    Stanford University

    BTech, 2000
    Computer Science and Engineering
    Indian Institute of Technology, Kharagpur