|
Security protocols enable useful tasks over untrusted networks. For example, confidential communication over the Internet between users and Web services like Google, Facebook, Amazon and Bank of America rely on protocols like SSL/TLS and the supporting Public Key Infrastructure (PKI). These protocols are designed to provide global security properties like authentication and confidentiality when various parties (e.g., the user, the Web service, and participants in the PKI such as certificate authorities) execute their prescribed programs. However, when individual parties deviate from their prescribed programs and the global security property is violated, it is important to hold agents accountable by detecting deviant behavior and determining which deviations actually caused the violation. Such determinations are useful in a wide range of distributed security settings, including in protocols for authentication and key exchange, electronic voting, and online auctions.
This project develops logic and language-based methods for deviance and causal determination in distributed systems. The project addresses the following scientifically challenging tasks: (1) Developing a language for distributed computing in which prescribed behavior of agents are represented with contracts. The contracts are specified via types and a type-directed distributed monitoring infrastructure is designed to detect deviance from contracts. The technical approach is based on novel dependent and stateful session types to express and verify security-relevant properties of systems. (2) Developing a formal blame semantics for distributed systems that is extensional (protocol- or system-independent). Recognizing that some deviations may not affect the security property, the blame semantics combines deviance from contracts with a novel definition of programs as actual causes of global security properties. The formalization of actual causation in this setting, while inspired by counterfactual theories of actual causation in philosophy and in computer science, goes beyond those theories by dealing with interacting distributed programs with nondeterministic operational semantics. (3) Applications of these methods to conduct a comprehensive study of proposed protocols for augmenting accountability in the public key infrastructure.
The project has potential for significant broader impact on society. Recent results have exposed the fragility of the Public Key Infrastructure on which hundreds of millions of people around the world rely to protect their communication over the Internet. A systematic basis for design, analysis, and comparison of protocols that improve accountability of the PKI can help protect Internet users from malicious adversaries who seek to snoop on their communications. The project also provides extensive training and educational opportunities for undergraduate and graduate students at Carnegie Mellon University.
Anupam Datta is an Associate Professor at Carnegie Mellon University where he
holds a joint appointment in the Computer Science and Electrical and Computer
Engineering Departments. His research focuses on the scientific foundations of
security and privacy. Datta's work has led to new principles for securely
composing cryptographic protocols and software systems; applications of these
principles have influenced several IEEE and IETF standards. His work on privacy
protection has led to formalizations of privacy as contextual integrity and
purpose restrictions on information use; accountability mechanisms for privacy
protection; and their applications in healthcare and Web privacy. Datta has
authored a book and over 40 other publications on these topics. He serves on
the Steering Committee and as the 2013-14 Program Co-Chair of the IEEE Computer
Security Foundations Symposium. Datta obtained Ph.D. (2005) and M.S. (2002)
degrees from Stanford University and a B.Tech. (2000) from IIT Kharagpur, all
in Computer Science.
|
TWC: Small: Blameworthy Programs: Accountability via Deviance and Causal Determination