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.