LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
Blockchains operating at the global scale demand high-performance byzantine fault-tolerant (BFT) consensus protocols.
Most classic PBFT-like protocols suffer from an issue known as the leader bottleneck, which severely limits their throughput and resource utilization.
Recently, Directed Acyclic Graph, or DAG-based protocols, have emerged as a promising approach for eliminating the leader bottleneck and achieving better performance.
They attain higher throughput by separating data dissemination and block ordering.
However, their safety and liveness logic is also significantly more elaborate.
So far, most DAG-based protocols have only enjoyed on-paper security proofs, and it is not clear how to construct formal proofs of these protocols efficiently.
We introduce LiDO-DAG, a concurrent object model that abstracts the common logic of these protocols.
LiDO-DAG is constructed by combining a DAG abstraction and LiDO, a recently proposed abstraction for leader-based consensus.
To demonstrate that our framework enables rapid validation of new DAG-based protocol designs,
we implemented LiDO-DAG in Coq and applied it to three recent DAG-based protocols, including Narwhal, Bullshark, and Sailfish.
Our framework readily yields mechanized safety and liveness proofs for all three protocols, which are also the first mechanized liveness proofs of any DAG-based protocol.
Our framework has also revealed an optimization for Sailfish that improves its worst-case latency.
Fri 20 JunDisplayed time zone: Seoul change
14:00 - 15:20 | Static Anlysis and VerificationPLDI Research Papers at Orchid Chair(s): Manu Sridharan University of California at Riverside | ||
14:00 20mTalk | PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs PLDI Research Papers Gabriel Ebner Microsoft Research, Guido Martínez Microsoft Research, Aseem Rastogi Microsoft Research, Thibault Dardinier ETH Zurich, Megan Frisella University of Washington, Tahina Ramananandro Microsoft Research, Nikhil Swamy Microsoft Research DOI File Attached | ||
14:20 20mTalk | LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols PLDI Research Papers Longfei Qiu Yale University, Jingqi Xiao Yale University, Ji-Yong Shin Northeastern University, Zhong Shao Yale University DOI | ||
14:40 20mTalk | Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses PLDI Research Papers Fabian Stemmler TU Munich, Michael Schwarz TU Munich, Julian Erhard TU Munich; LMU Munich, Sarah Tilscher TU Munich; LMU Munich, Helmut Seidl TU Munich DOI Pre-print Media Attached | ||
15:00 20mTalk | Relational Abstractions Based on Labeled Union-Find PLDI Research Papers Dorian Lesbre Université Paris-Saclay - CEA LIST, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Hichem Rami Ait-El-Hara OCamlPro; Université Paris-Saclay - CEA LIST, François Bobot Université Paris-Saclay - CEA LIST DOI |