Collaborative Research: FMitF: Track I: Verifying distributed systems for liveness with Byzantine participants

About This Grant

Many distributed systems involve interactions among computers controlled by different parties. These systems must work correctly even when some of the participants are malicious and try to interfere with the system. In computer science , these kinds of malicious participants are called Byzantine participants. Various protocols and algorithms have been developed to ensure that the systems operate correctly so long as only a small fraction of the participants behave maliciously. However, implementations of these kinds of systems often have bugs. One class of bugs that is particularly challenging to address is liveness bugs, in which the system stops making progress and fails to complete operations. To reduce the incidence of bugs, researchers have developed an approach called formal verification, in which a mathematical proof is constructed that shows a software system is free from a certain class of bugs. However, existing methods for verifying the absence of liveness bugs have limitations that make them inapplicable to many important systems. This project develops new techniques for verifying the absence of liveness bugs in systems with malicious participants, expanding the kinds of systems that can be verified. In addition, the research team develops new tutorials, labs, and lectures on verification of distributed systems, and organizes the annual New England Systems Verification Day, which brings together verification researchers and industry practitioners. This project develops a new automation-friendly approach for modularly verifying the liveness of distributed systems with Byzantine participants. Especially, the project team develops novel liveness-preserving composition operators, which allow decomposing complex system proofs into smaller independent subprotocols. To reason about the use of cryptographic signatures in the distributed systems that tolerate Byzantine participants, the project uses a new model called the stapling model, which enables to analyze the signed messages in an automatable way. To prove the soundness of the stapling model and other components of the approach, this project develops an innovative program logic for proving liveness based on separation logic. 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.