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

协作研究：SaTC：核心：小型：分离逻辑中的机械化密码推理

• 批准号: 2314323
• 负责人: Arthur Azevedo de Amorim
• 金额: $ 28.13万
• 依托单位: Rochester Institute of Tech
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2314323&HistoricalAwards=false
• 关键词: Collaborative; Research; SaTC; CORE; Small

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.

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