Shipwright: Proving liveness of distributed systems with Byzantine participants

TL;DR

Shipwright is a verification framework that proves correctness and liveness of decentralized systems with malicious participants, demonstrated on a verified PBFT implementation in Go.

Contribution

It introduces techniques for formal reasoning about Byzantine participants, modular proofs, and cryptographic message verification, enabling verified executable distributed protocols.

Findings

Successfully verified liveness of PBFT prototype

Demonstrated system operation in various failure scenarios

Enabled modular and sound reasoning about cryptographic messages

Abstract

Ensuring liveness in a decentralized system, such as PBFT, is critical, because there may not be any single administrator that can restart the system if it encounters a liveness bug. At the same time, liveness is challenging to achieve because any single participant could be malicious, and yet the overall system must make forward progress. While verification is a promising approach for ensuring the absence of bugs, no prior work has been able to verify liveness for an executable implementation of PBFT. Shipwright is a verification framework for proving correctness and liveness of distributed systems where some participants might be malicious. Shipwright introduces three techniques that enable formal reasoning about decentralized settings with malicious participants, allow developers to decompose their system and proof in a modular fashion into sub-protocols and sub-proofs, and support sound reasoning about cryptographic signatures that may be embedded in messages. We used Shipwright to implement and verify an initial prototype of agreement on a single log entry in PBFT (with a few limitations) and translate it to an executable implementation in Go. We experimentally demonstrate its operation and liveness both in the common case and in several failure scenarios.