文章基本信息

标题：On the Formal Verification of the Stellar Consensus Protocol
本地全文：下载
作者：Giuliano Losa ; Mike Dodds
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2020
卷号：84
页码：1-9
DOI：10.4230/OASIcs.FMBC.2020.9
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：The Stellar Consensus Protocol (SCP) is a quorum-based BFT consensus protocol. However, instead of using threshold-based quorums, SCP is permissionless and its quorum system emerges from participantsâ self-declared trust relationships. In this paper, we describe the methodology we deploy to formally verify the safety and liveness of SCP for arbitrary but fixed configurations. The proof uses a combination of Ivy and Isabelle/HOL. In Ivy, we model SCP in first-order logic, and we verify safety and liveness under eventual synchrony. In Isabelle/HOL, we prove the validity of our first-order encoding with respect to a more direct higher-order model. SCP is currently deployed in the Stellar Network, and we believe this is the first mechanized proof of both safety and liveness, specified in LTL, for a deployed BFT protocol.
关键词：Consensus; Blockchains; First-Order Logic; Stellar; Ivy Prover; Decidability