TWC: Small: Blameworthy Programs: Accountability via Deviance and Causal Determination

安全协议允许在不受信任的网络上执行有用的任务。例如，用户与谷歌、Facebook、亚马逊和美国银行等网络服务之间通过互联网进行的保密通信依赖于诸如SSL/TLS和支持的公钥基础设施(PKI)等协议。这些协议旨在当各方(例如，用户、Web服务和PKI参与者，如证书颁发机构)执行其规定的程序时，提供诸如身份验证和机密性之类的全局安全属性。然而，当个别各方偏离其规定的计划并违反全局安全属性时，重要的是通过检测异常行为并确定哪些偏差实际导致了违规来追究代理的责任。这种确定在广泛的分布式安全设置中很有用，包括用于身份验证和密钥交换、电子投票和在线拍卖的协议。这个项目开发了基于逻辑和语言的方法来确定分布式系统中的偏差和因果关系。该项目解决了以下具有科学挑战性的任务：(1)开发一种用于分布式计算的语言，其中指定的代理行为用合同表示。合同是通过类型指定的，并设计了一个面向类型的分布式监控基础设施来检测合同的偏差。该技术方法基于新的依赖的和有状态的会话类型来表达和验证系统的安全相关属性。(2)为分布式系统开发了一种形式化的、可扩展的(协议或系统无关的)指责语义。认识到一些偏差可能不会影响安全属性，指责语义将来自合同的偏差与程序的新定义结合在一起，作为全局安全属性的实际原因。在这种情况下，实际因果的形式化受到哲学和计算机科学中实际因果的反事实理论的启发，通过处理具有非确定性操作语义的交互分布式程序，超越了这些理论。(3)应用这些方法对公钥基础设施中加强问责的拟议协议进行全面研究。该项目有可能对社会产生更广泛的重大影响。最近的结果暴露了公钥基础设施的脆弱性，全世界数亿人依赖公钥基础设施来保护他们在互联网上的通信。设计、分析和比较改进PKI责任的协议的系统基础可以帮助保护Internet用户免受试图窥探其通信的恶意对手的攻击。该项目还为卡内基梅隆大学的本科生和研究生提供广泛的培训和教育机会。

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.