Anupam Data is a Research Scientist with CyLab, the Computer Science Department and the department of Electrical and Computer Engineering. The overarching goal of his research program is to provide a theoretically well-founded basis for security practice. The work of his research group 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.
posted by Richard Power
CyLab Chronicles: What aspect of research would you like to highlight?
DATTA: 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 CyLab efforts focusing on design and implementation of secure systems by providing assurance that such systems are, in fact, secure. I have three substantial ongoing projects in this space, but would like to focus on one. The project is called Protocol Composition Logic (PCL). I have been working on this project with collaborators at Stanford and Kestrel for the past six years or so. This project has had impact on industrial security protocol standards. It is also being currently taught in graduate security courses at several universities.
CyLab Chronicles: What technology are you working on?
DATTA: PCL is a prominent method for security analysis of network protocols. A major advantage of PCL over existing methods is that the analysis can be done in a modular fashion, i.e. you can take a large industrial protocol such as the IEEE 802.11i wireless LAN security standard, prove security of each of its components independently, and combine these proofs using our method to obtain a proof of the complete protocol. This "divide and conquer" paradigm is common in other areas of computer science, but was not possible in reasoning about deployed security protocols prior to our work.
CyLab Chronicles: What are the unique attributes of your work?
DATTA: A fundamental question in computer security is the following: Does a given protocol or system guarantee certain security properties even in the face of attack? Our work provides a theoretically well-founded approach for answering this question for widely deployed network protocols such as SSL, IEEE 802.11i, Kerberos, and the IPSec standards.
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.
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.
CyLab Chronicles: What problem(s) does your work address?
DATTA: 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. Our work on PCL provides a principled, practical approach for establishing that such industrial protocols are, in fact, secure.
CyLab Chronicles: What are the commercial implications of your work?
DATTA: This work has significant commercial implications. Many applications such as internet banking and online stores (dealing with billions of dollars) rely on the underlying network protocols to be secure. It is also important for companies because proprietary information flows through corporate VPNs that are required to be secure. The industrial network protocol standards are developed by standards bodies such as the IETF and IEEE working groups that include employees of companies such as Microsoft, CISCO, Intel and Sun Microsystems. It is helpful for companies to have assurance in the security of these protocols prior to implementation and deployment. There have been several cases of interaction between these standards bodies and researchers working on formal security analysis. For example, there was a recent attack on the Kerberos PKINIT protocol identified by our collaborators at the University of Pennsylvania. Consequently, the standard was modified to fix the vulnerability and Microsoft released a patch to fix its implementation. I should add that, in addition to PCL, there are now several highly successful methods and tools for security protocol analysis that are now ready for industrial use. This research area has come of age.
See all CyLab Chronicles articles