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

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

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.