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. This work complements other efforts at CMU focusing on design and implementation of secure systems by providing assurance that such systems are, in fact, secure. 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 fi! xes have been adopted by the respective standards bodies.

(2) Foundations of Privacy

Privacy is an area of great current interest. Over the last few years, several privacy laws have been passed in the US and Europe. Organizations that handle sensitive personal information are required to use systems that comply with these laws. For example, health care organizations have to comply with HIPAA, financial institutions with GLBA, and websites that publish information about children with COPPA. This motivates the need for computational methods for specifying and enforcing privacy policies within organizations. We have developed a privacy policy language that is inspired by a philosophical theory of privacy called "contextual integrity" due to Helen Nissenbaum (NYU). The technical approach is based on temporal logic. Our preliminary results indicate that the language is a good fit for the forms of policies that appear in privacy laws, although much work still remains to be done.

Another dimension in the privacy space that we are currently exploring pertains to data privacy. Specifically, we seek to answer the following fundamental question: Given a database containing sensitive information about individuals, how should the data be anonymized so thatthe modified data does not reveal sensitive information about individuals (protects privacy), while still indicating certain general trends about the population (provides utility)? A theoretically well-founded solution to this problem that is useful in practice is still unknown.

(3) Trustworthy Systems

We have initiated a program to develop a theoretical basis for the design and analysis of secure systems. We define a system as a set of concurrent, interacting threads with shared mutable state. Interaction may take place locally through reads and writes to shared memory or over a network. This definition is motivated by our target application domain, which includes a number of deployed and industrial standard contemporary systems such as OS kernels, virtualmachinemonitors (VMMs), and co-processor-based systems such as those utilizing the Trusted Computing Group�s Trusted Platform Module (TPM) [31]. Our long-term goal is to develop a formal framework for modeling and analysis of secure systems at two levels of abstraction�system architecture and system implementation. A specific issue that we plan to address in developing and using this framework is to provide rigorous definitions of security and adversary models, a relatively unexplored area in system security. In addition, we hope to identify design principles for secure systems, as well as a core set of basic building blocks from which complex systems can be constructed via secure composition. We expect this effort to draw on methods from mathematical logic, type theory and software model-checking.