| Department | Electrical and Computer Engineering |
|---|---|
| Office | 2118 Collaborative Innovation Center |
| danupam@andrew.cmu.edu | |
| Website | http://www.andrew.cmu.edu/user/danupam/ |
Our goal 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 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.
A formalization of privacy as a right to appropriate flows of personal information(not simply confidentiality or control) and as a right to use of personal information for appropriate purposes.
Principled audit mechanisms for enforcing privacy properties, recognizing that traditional preventive access control and information flow control mechanisms are inadequate for enforcing practical privacy policies. The audit mechanisms address key scientific challenges: (1) operating with audit logs that are incomplete (i.e., missing relevant information) and accumulate information over time; (2) accounting for the imperfect nature of periodic audits (i.e., not all information in a log may be inspected) in a setting with adaptive adversaries whose exact incentives are not known. Applications to several US privacy laws, including the first complete logical specification and audit of all disclosure-related clauses of the HIPAA Privacy Rule.
Contemporary secure systems are complex and designed to provide subtle security properties in the face of attack. Examples of such systems include hypervisors, virtual machine monitors, security kernels, operating systems, web browsers, and secure co-processor-based systems such as those utilizing the Trusted Computing Group’s Trusted Platform Module (TPM). But are such systems really secure? What does it even mean for a system to be "secure"? What security property does a given system provide and against what class of adversaries?
The goal of this project is to develop principled approaches for modeling, analysis, and design of secure systems --- their architectures and implementations. We will provide rigorous definitions of security and adversary models for systems, a relatively unexplored and yet very important aspect of system security. A specific goal is to develop a unified framework for modeling secure systems and adversaries in terms of their capabilities and methods for proving the absence of all attacks that an adversary with these capabilities can launch. This is in contrast to the common practice of enumerating known attacks and arguing that the system is not susceptible to them. Finding the right definitions of end-to-end security of systems is also a wide open area. This work will draw on methods from logic, programming languages and software model checking.
One significant challenge here is finding the right abstractions: whenever we work with formal models, there is always the question of whether the model faithfully reflects the essential features of the actual system. We plan to validate our models by applying them to real systems: if, for example, an analysis in the model identifies previously known and unknown attacks on systems, then that provides evidence of its usefulness. Another significant challenge with analysis methods for secure systems is scaling these methods to complex, large scale, real systems. We are exploring several approaches to address this problem, in particular, secure composition and security-preserving translations.
Reasoning about security of a complex system in a modular manner (i.e., by separately proving security of the components that it is built from and then combining these proofs) is a major open problem in computer security. We are currently working on this problem, building on our prior successful work on modular reasoning about secure network protocols. We are also exploring methods for security-preserving translations that will enable us to prove security properties of an abstract model of a complex system, but guarantee that those properties carry over to the actual software implementation of the system. One example of how this approach may work in practice can be found in programming language methods where a high-level language is used to write code which then gets translated down to low-level executable code. Programs in the high-level language are easier to analyze than programs in the low level language. But do the guarantees carry over? There has been some progress in carrying over such guarantees for correctness properties, but less so for security properties, in particular, because the adversary at the low level may have additional capabilities that the high-level adversary does not. Another example of such an approach can be found in software model checking methods where abstract models are automatically extracted from source code (e.g., programs written in C) in a way that if no bugs of a certain class are found in the abstract model, then it is guaranteed (under some additional assumptions) that no bugs exist in the source code. Such methods have been applied for establishing correctness properties of some systems. But again, there is very little work along these lines for security properties of systems --- a gap that our work aims to fill.
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.
Carnegie Mellon, 2007
Computer Systems
PhD, 2005
Computer Science
Stanford University
MS, 2002
Computer Science
Stanford University
BTech, 2000
Computer Science and Engineering
Indian Institute of Technology, Kharagpur
