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

点击翻译按钮获取中文摘要

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.