On the Formal Verification of the Stellar Consensus Protocol
On the Formal Verification of the Stellar Consensus Protocol
复制标题
论恒星共识协议的形式化验证
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
A. Uysalel
中科院分区：
文献类型：
--
作者：
Helin Sahinturk;S. Turhan;Selvi Ozlem Can;Ali Abbas Ylmaz;A. Uysalel
恒星共识协议（SCP）是一种基于法定人数的BFT共识协议。然而，SCP不是使用基于阈值的法定人数，它是无许可的，它的法定人数系统来自参与者自我声明的信任关系。在本文中，我们描述的方法，我们部署正式验证的安全性和活性的SCP任意但固定的配置。证明使用Ivy和Isabelle/HOL的组合。在Ivy中，我们在一阶逻辑中对SCP进行建模，并在最终同步下验证安全性和活性。在Isabelle/HOL中，我们证明了我们的一阶编码相对于更直接的高阶模型的有效性。SCP目前部署在Stellar网络中，我们相信这是LTL中指定的第一个安全性和活性的机械化证明，用于部署BFT协议。2012 ACM主题分类软件及其工程→软件验证;网络→协议测试与验证
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. 2012 ACM Subject Classification Software and its engineering → Software verification; Networks → Protocol testing and verification