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

FMITF：轨道 I：ADVERT：分布式系统验证的组合原子规范

基本信息

批准号：
2019285
负责人：
Zhong Shao
金额：
$ 74.99万
依托单位：
Yale University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-10-01 至 2024-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2019285&HistoricalAwards=false
关键词：
FMitF Track ADVERT Compositional Atomic

项目摘要

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.

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

项目成果

期刊论文数量（8）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems

DOI：
10.1145/3485474
发表时间：
2021-10
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Wolf Honoré;Jieung Kim;Ji-Yong Shin;Zhong Shao
通讯作者：
Wolf Honoré;Jieung Kim;Ji-Yong Shin;Zhong Shao

Adore: atomic distributed objects with certified reconfiguration

Adore：具有经过认证的重新配置的原子分布式对象

DOI：
10.1145/3519939.3523444
发表时间：
2022
期刊：
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
0
作者：
Honoré, Wolf;Shin, Ji-Yong;Kim, Jieung;Shao, Zhong
通讯作者：
Shao, Zhong

TimeDice: Schedulability-Preserving Priority Inversion for Mitigating Covert Timing Channels Between Real-time Partitions

DOI：
10.1109/dsn53405.2022.00052
发表时间：
2022-06
期刊：
2022 52nd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)
影响因子：
0
作者：
Man-Ki Yoon;Jung-Eun Kim;Richard M. Bradford;Zhong Shao
通讯作者：
Man-Ki Yoon;Jung-Eun Kim;Richard M. Bradford;Zhong Shao

Verified compilation of C programs with a nominal memory model