Research Overview (Back to Anupam Datta's Home Page)

• Foundations of Privacy: This project seeks to formalize privacy properties and develop mechanisms for enforcing privacy properties. The technical work is guided by and has impact on application domains (e.g., healthcare) that raise significant privacy concerns in modern society. Specific results include (1) Formalizing Contextual Integrity: A semantic model and logic of privacy that formalizes the position taken by contextual integrity, a philosphical account of privacy as a right to appropriate flows of personal information [Oakland 2006]; a more general privacy logic in which we present the first complete formalization of the entire HIPAA Privacy Rule and GLBA [WPES 2010]. (2) Principled Audit Mechanisms: A policy auditing algorithm that operates iteratively over incomplete logs and policies expressed in a privacy logic; application to check disclosure logs for compliance with the entire HIPAA Privacy Rule [CCS 2011]. A formalization of periodic audits in adversarial environments as an online learning problem and learning algorithms that provide operational guidance on auditing with imperfect information (e.g., on audits for detecting inappropriate accesses to patient records) [CSF 2011]
  • Keynote lecture: Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms at the 2011 International Conference on Information Systems Security
  • Invited tutorial: Foundations of Privacy at the 2011 Summer School on Security and Privacy organized by Microsoft Research and Indian Institute of Science
  • SHARPS team receives a $15 million grant from the HHS for research in Security of Health Information Technology [HHS Press Release] [CMU Press Release]
  • Talks: IBM T. J. Watson Research Center, Symantec Research, NYU/IBM Workshop on Managing Data Risk: Acquisition, Processing, Retention and Governance, NYU Computer Science Colloquium, University of Saarlandes and MPI-SWS  Information Security and Cryptography Seminar, University of Trier Computer Science Seminar, Keio University Philosophy Seminar
• Theory of Secure Systems: This project seeks to develop principled approaches for the analysis and design of practical secure systems. We reduce reasoning about semantic security properties to reasoning about properties of programs with suitable abstractions of security mechanisms and adversary capabilities. Specific results include (1) Logic of Secure Systems (LS^2): A logic of secure systems with a general treatment of interface-confined adversaries and principles for secure composition that transcend specific application domains; applications to secrecy properties of network protocols, access control properties of file systems [MFPS 2010, S&P 2011], and integrity properties of trusted computing systems, addressing the challenge of reasoning in the presence of adversaries that can modify code; the case study also identified an insecure interaction between two trusted computing mechanisms [Oakland 2009]; (2) Software Model Checking Semantic Security Properties: ASPIER - a cryptography-aware counter-example guided abstraction-refinement method and software model checking tool for verifying C source code of security protocols; application to the OpenSSL handshake protocol [CSF 2009]. A parametric verification technique for optimal reduction of the size of data structures in security mechanisms enabling automated model checking of address separation properties of practical security hypervisors [Oakland 2010]
  • 2011 AFOSR MURI Award on Science of Security: Modeling, Composition and Measurement
  • Invited Tutorial: Programming Language Methods for Compositional Security at the 2010 Oregon Programming Languages Summer School
  • Invited Talk: Compositional System Security with Interface-Confined Adversaries, 26th Annual Conference on Mathematical Foundations of Programming Semantics, May 2010
  • Invited panelist: Toward Semantic Security Properties of Software, Panel on Rigorous Security Analysis of Software at IEEE Computer Security Foundations Symposium, July 2009
  • Invited Panelist: Is there a Science of Security, and if so, what might it look like? Panel at the NSF/IARPA/NSA Workshop on the Science of Security, November 2008
• Protocol Composition Logic(PCL): PCL is a logic for proving security properties of network protocols [Book Chapter 2011]. Two central results for PCL are a set of composition theorems [JCS 2005, CCS 2005, Book Chapter 2008] and computational soundness theorems [ICALP 2005, CSFW 2006, ESORICS 2007, JCS 2010]. 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. 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.
  • Talks: CMU CyLab Seminar, CMU Computer Science Seminar, MSR Cambridge, Oxford Computing Laboratory, MIT Cryptography and Information Security Seminar, Princeton TACL Seminar, UPenn Computer Security Seminar, Cornell Computer Security Seminar, UC Berkeley Computer Security Seminar, MITACS Digital Security Seminar at Carleton University, University of Toronto Computer Science Seminar, University of Wisconsin Computer Science Colloquium, UCSD Computer Science Seminar, UCSC Computer Science Seminar, UCLA Computer Science Colloquium, UIUC Trust and Security Seminar
  • Papers invited to special issues of journals: CSFW 2003, CCS 2005, WITS 2007