Collaborative Research: SaTC: CORE: Small: Mechanized Cryptographic Reasoning in Separation Logic

计算机辅助密码学已经开始影响现实世界协议的设计和实现。它的主要挑战之一是开发可维护的模型和证明。尤其重要的是，验证协议的假设和保证可以相互核对，以便协议和系统的设计可以通过密码学和安全性的形式化推理以稳健的方式发展。这个项目中使用的形式化推理方法是基于分离逻辑的，这是一种用于证明计算机系统中没有错误的数学框架。虽然存在许多这样的框架，但分离逻辑近年来吸引了相当大的兴趣，因为它简化了计算机系统如何使用诸如内存、磁盘空间等资源的分析。一般来说，对这些资源的推理是具有挑战性的，因为不同的系统组件可能以潜在冲突的方式使用相同的资源。例如，程序中的两个组件可能试图以相同的名称保存不同的文件，从而导致数据丢失。传统上，这些冲突是通过推理系统的每个部分同时在做什么来排除的，这使得系统分析变得复杂。相比之下，使用分离逻辑可以孤立地分析每个系统组件所做的工作，而不管系统的其余部分正在做什么。这使得分析更加自成体系，允许分离逻辑处理比传统方法更复杂的系统。尽管有许多成功的案例证明了这种能力，但有一类重要的组件在分离逻辑中经常被忽视：密码协议。面对开放的网络，为了抵御攻击者，联网系统必须使用复杂的密码协议进行通信。目前分离逻辑中的证明都是从这些协议中抽象出来的，假设了一个理想的模型，其中恶意代理对通信的能力是有限的。因为分析没有考虑底层协议，所以它可能会遗漏系统中的错误，这些错误是由于采用了错误的协议，或者只是由于以不正确的方式使用了正确的协议而导致的。该项目旨在通过使用密码推理扩展分离逻辑来提高程序验证的最新水平。通过明确考虑加密协议，该扩展将使分离逻辑开发更加可靠。该项目的目标是：(1)使用分离逻辑中的资源来建模密码术语；(2)简化对独立开发和验证的复合协议的分析；以及(3)将密码推理集成到现有的验证分布式系统的框架中。由此产生的逻辑将有两种变体：一种用于密码学的符号模型，它更适合于形式分析；另一种用于计算模型，它提供了更强有力的保证。逻辑的设计将建立在现有的协议分析方法的基础上，例如协议模型检查器或通用可组合性框架。该项目的一部分包括基于IRIS实现此逻辑的验证检查器，IRIS是构建在CoQ证明助手上的分离逻辑框架。这将允许逻辑支持分离逻辑的许多高级功能，同时保持相对较小和可信的代码库。对逻辑的评估将基于一系列案例研究，验证协议并将其整合到更大的系统中。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Computer-aided cryptography has started to impact the design and implementation of real-world protocols. One of its main challenges is the development of maintainable models and proofs. In particular, it is important that the assumptions and guarantees of verified protocols can be checked against each other, so that the design of protocols and systems can evolve in a robust manner through formalized reasoning for cryptography and security. The formal reasoning methods used in this project are based on separation logic, a mathematical framework for certifying the absence of bugs in computer systems. While many such frameworks exist, separation logic has attracted considerable interest in recent years because it simplifies the analysis of how computer systems employ resources such as memory, disk space, etc. Reasoning about these resources is challenging in general because different system components might use the same resource in potentially conflicting ways. For example, two components in a program might try to save different files under the same name, thus leading to data loss. Traditionally, these conflicts were ruled out by reasoning about what every part of the system is doing at the same time, rendering the analysis of systems complex. With separation logic, by contrast, it is possible to analyze what each system component does in isolation, regardless of what the rest of the system is doing. This makes the analysis more self contained, allowing separation logic to handle more complex systems compared to traditional methods. Despite many success stories demonstrating this power, there is an important class of components that are often overlooked in separation logic: cryptographic protocols. To withstand attackers when facing an open network, networked systems must communicate using intricate cryptographic protocols. Current proofs in separation logic abstract away from these protocols, assuming an ideal model where malicious agents have limited power over communication. Because the analysis does not take the underlying protocols into account, it might miss bugs in the system that result from employing a faulty protocol, or simply from employing a correct protocol in incorrect ways. This project aims to advance the state-of-the-art in program verification by extending separation logic with cryptographic reasoning. The extension will make separation logic developments more reliable by explicitly taking cryptographic protocols into account. The goals of the project are: (1) Using resources in separation logic to model cryptographic terms; (2) Simplifying the analysis of composite protocols that were developed and verified independently; and (3) Integrate cryptographic reasoning within existing frameworks for verifying distributed systems. The resulting logic will come in two variants: one for the symbolic model of cryptography, which is better suited for formal analysis, and one for the computational model, which offers stronger guarantees. The design of the logic will build upon existing approaches for protocol analysis, such as protocol model checkers or the universal composability framework. Part of the project consist of implementing a proof checker for this logic based on Iris, a framework for separation logic built on the Coq proof assistant. This will allow the logic to support many advanced features of separation logic while keeping a relatively small and trustworthy code base. The evaluation of the logic will be based on a series of case studies verifying protocols and integrating them in larger systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.