FMitF: Track I: ADVERT: Compositional Atomic Specifications for Distributed System Verification

由于处理并发性和网络异步性的固有复杂性，分布式系统难以验证。在正式指定和验证分布式系统方面已经取得了重大进展，但是现有的方法侧重于对分布式系统的特定实例进行推理，并且在隐藏实现细节的同时很少公开常见的高级行为。因此，今天验证单个分布式系统需要冗余推理，并且缺乏高级模型使得难以处理现代应用程序通常由多个分布式系统组成的新挑战。这个项目的新颖之处是一个组合原子分布式对象模型，它促进了对分布式系统的单个和组合的推理和验证，以及一个正式的验证工具，ADVERT，它可以用来构建大规模的认证分布式系统。该项目的影响包括显著提高大型软件基础设施（如云）的可靠性和安全性的新工具，以及运行在基础设施之上的应用程序，以及关于分布式系统设计和验证的新课程，这些课程将扩大代表性不足的群体的参与。原子分布式对象模型封装了各个分布式系统的关键安全属性。该项目开发了多个基于网络的规范，这些规范捕获分布式系统中类似类的公共网络级行为。基于网络的规范帮助单个系统验证它们与原子分布式对象模型的细化关系，提供来自公共系统行为的可重用证明，并充当验证模板，免费建立封装在原子对象模型中的安全属性。一旦基于原子分布式对象模型验证了单个分布式系统是正确和安全的，就可以使用该模型的高级抽象来推断多个分布式系统交互。该项目开发了一个基于原子分布式对象模型的分布式系统验证框架ADVERT，用于验证单个分布式系统及其交互。研究人员通过具体的例子证明，由于对象接口非常简单，原子分布式对象模型甚至可以直接证明复合分布式系统的属性。最后，研究人员验证了用c语言编写的真实世界的尖端分布式系统。其中一个目标系统是分布式共享内存，它使用可编程交换机、低延迟网络和运行共识协议的多个分片分布式组件。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Distributed systems are difficult to verify due to their inherent complexity from handling concurrency and network asynchrony. Significant advances have been made in formally specifying and verifying distributed systems, but existing approaches focus on reasoning about specific instances of distributed systems and do little to expose the common high-level behaviors while hiding the implementation details. As a result, verifying individual distributed systems today requires redundant reasoning, and the absence of a high-level model makes it difficult to address the new challenges that modern applications are often composed of multiple distributed systems. This project's novelties are a compositional atomic distributed object model that facilitates reasoning and verification of both individual and composition of distributed systems, and a formal verification tool, ADVERT, that can be used to build large-scale certified distributed systems. The project's impacts include new tools to significantly improve the reliability and security of large-scale software infrastructures, such as the cloud, and applications that run on top of the infrastructure, and also new courses on distributed-system design and verification that will broaden the participation of underrepresented groups.The atomic distributed object model encapsulates the key safety properties of individual distributed systems. The project develops multiple network-based specifications that capture the common network-level behavior of similar classes of distributed systems. A network-based specification helps individual systems to verify their refinement relation to the atomic distributed object model, provides reusable proofs that are derived from common system behaviors, and acts as a verification template that establishes the safety properties encapsulated in the atomic object model for free. Once individual distributed systems are verified to be correct and safe based on the atomic distributed object model, the high-level abstraction of the model can be used to reason about multiple distributed system interactions. The project develops a distributed system verification framework, ADVERT, based around the atomic distributed object model, to verify individual distributed systems and their interactions. The investigators demonstrate through concrete examples that proving properties even of composite distributed systems can be straightforward with the atomic distributed object model due to the elegantly simple object interface. Finally, the investigators verify real-world cutting-edge distributed systems written in C. One of the target systems is a distributed shared memory that uses a programmable switch, a low-latency network, and multiple sharded distributed components that run consensus protocols.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.