Anupam Datta
Research Scientist, CyLab, Computer Science, Electrical and Computer Engineering
www

The overarching goal of my research program is to provide a theoretically well-founded basis for security practice. Our work provides rigorous definitions for what it means for a system to be "secure", and methods and mechanized tools for verifying whether a given system actually is "secure" in this precise sense. I have 3 substantial ongoing projects in this space.

(1) Security Analysis of Network 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.

(2) Foundations of Privacy

Modern organizations, such as businesses, non-profits, government agencies, and universities, collect and use information from a variety of sources. These information sources, ranging from individuals entering personal information into social networking websites to cooperating enterprises exchanging customer or supplier information, may provide information of varying quality under specific expectations about how this information will be transmitted and used. Organizations, in turn, may be required by contract, regulations, or market forces to track conditions associated with the information they use, with failure to use information correctly potentially resulting in embarrassment, brand erosion, or financial loss. Thus, complex modern organizations face the problem of handling information in ways that respect privacy promises to individuals, comply with privacy laws and other regulations, minimize operational risk, and yet allow the core functions of the organization to be carried out efficiently and effectively. This problem is recognized as one of the greatest challenges facing organizations today (see, for example, a recent survey from Deloitte and the Ponemon Institute), with far-reaching implications for every individual in contemporary society.

This project develops methods, algorithms and prototype tools for integrating privacy, compliance, and risk evaluation into complex organizational processes. We also plan to explore, articulate and characterize formally the scope and nature of privacy expectations and regulations, addressing questions such as: what precise operating restrictions do laws such as HIPAA, GLBA, and FERPA impose on organizations? Can parts of these laws be formalized and used in information systems? What expectations does the public have for insurance companies, social networking sites, universities, and government agencies that collect personal information? How can those expectations be met and what is the risk of not doing so? How can aggregate anonymized information be revealed while still protecting personal privacy? This project draws on, develops and integrates ideas from philosophical studies of privacy, logical methods, quantitative methods for database privacy, and economics-inspired methods for privacy risk management.

Specifically, we have developed a privacy policy language that is inspired by a philosophical theory of privacy called "contextual integrity". Our preliminary results indicate that the language is a good fit for the forms of policies that appear in privacy laws.

(3) Trustworthy Systems

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 form 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, such as device drivers at Microsoft. But again, there is very little work along these lines for security properties of systems --- a gap that our work aims to fill.