Anupam Datta

Adjunct Professor, Electrical and Computer Engineering

Bio

Anupam Datta is an Adjunct Professor of Electrical and Computer Engineering at Carnegie Mellon University. His research focuses on enabling real-world complex systems to be accountable for their behavior, especially as they pertain to privacy, fairness, and security. His work has helped create foundations and tools for accountable data-driven systems. Specific examples include an accountability tool chain for privacy compliance deployed in industry, automated discovery of gender bias in the targeting of job-related online ads,  and principled tools for explaining decisions of artificial intelligence systems. Datta serves as lead PI of a large NSF project on Accountable Decision Systems, on the Steering Committee of the Conference on Fairness, Accountability, and Transparency in socio-technical systems, and as an Editor-in-Chief of Foundations and Trends of Privacy and Security. He obtained Ph.D. and M.S. degrees from Stanford University and a B.Tech. from IIT Kharagpur, all in Computer Science.

Education

Ph.D., 2005 
Computer Science 
Stanford University

M.S., 2002 
Computer Science 
Stanford University

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

Research

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.

Keywords

• Scientific foundations of security and privacy
• Accountable machine learning