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.

分布式系统由于处理并发和网络异步而很难验证。在正式指定和验证分布式系统方面已取得了重大进展，但是现有的方法着重于推理分布式系统的特定实例，并且在隐藏实施细节的同时，几乎无能为力地公开常见的高级行为。结果，当今验证单个分布式系统需要冗余的推理，并且缺乏高级模型，因此很难应对现代应用程序通常由多个分布式系统组成的新挑战。该项目的新颖性是一种组成原子分布式对象模型，可促进分布式系统的个人和组成的推理和验证，以及一种正式的验证工具，广告，可用于构建大规模认证的分布式系统。该项目的影响包括新工具，可显着提高大规模软件基础架构的可靠性和安全性，例如云以及在基础架构之上运行的应用程序，以及在分布式系统设计和验证方面的新课程，这些课程将扩大了不足的对象模型模型分配的单个分配安全性属性。该项目开发了多种基于网络的规范，可捕获类似类别分布式系统类别类别类别的网络级别行为。基于网络的规范可帮助各个系统验证其与原子分布式对象模型的完善关系，提供可重复使用的证明，这些证明是从共同的系统行为中得出的，并充当验证模板，该模板建立了自由原子对象模型中封装的安全属性。一旦根据原子分布式对象模型验证了单个分布式系统是正确且安全的，则该模型的高级抽象可用于对多个分布式系统相互作用进行推理。该项目基于原子分布式对象模型开发了分布式系统验证框架，广告，以验证单个分布式系统及其交互。研究人员通过具体示例证明，由于优雅的简单对象接口，与原子分布式对象模型一起证明了复合分布式系统的特性，甚至可以直接使用。最后，研究人员验证了用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