CAREER: Formal Verification of Stateful Distributed Systems and Their Compositions

Formal verification has made considerable progress in ensuring the correctness of system designs, but verifying distributed systems remains a significant challenge. Existing research on verifying distributed systems suggests general verification strategies that have limited scalability or concentrate on specific systems without sufficient attention to modularity and proof reuse. These limitations become apparent when verifying large-scale distributed systems with multiple distributed subsystems. Verifying different subsystems requires redundant work, and insufficient modularity impedes the verification process as a small code change entails a significant amount of proof rewriting. This project's novelties are composable semantic models that capture a variety of weakly consistent distributed system semantics and their correctness proofs and methodologies that reuse the models to simplify and scale the verification of distributed systems. The project's impacts are improved reliability and assurance of small to large-scale distributed systems, such as individual distributed key-value stores and cloud services that rely on multiple distributed systems. Additional impacts include new courses on verifying distributed systems. This project focuses on modeling and verifying weakly consistent distributed systems, the most widely deployed distributed system family. The key approach is to first model and verify the distributed system semantics rather than a specific implementation for high utility. A semantic model modularly captures common behaviors and states of distributed systems that observe the same semantics as an object and hides node and network-level details of the system for simple reasoning. The model encompasses reusable proofs of safety and liveness properties that must be satisfied by the system implementation. The model's proofs are reused to verify different system implementations under the same semantics through refinement. Semantic models are designed to compose with each other. Composability facilitates the reuse of designs and proofs of weaker semantic models to create stronger semantic models. The semantic models simplify the verification of composite distributed systems. Individual subsystems can be verified using corresponding semantic models, and interactions of the subsystems can be reasoned and verified based on simple model-level behaviors rather than sophisticated implementation-level behaviors. The model-based reasoning of interactions and the model's compositionality allow for modularly defining and verifying existing and new distributed system semantics that span multiple distributed 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.