Mechanising blockchain consensus
Mechanising blockchain consensus
复制标题
DOI：
10.1145/3167086
复制
发表时间：
2018-01
期刊：
影响因子：
--
通讯作者：
George Pîrlea;Ilya Sergey
中科院分区：
文献类型：
--
作者：
George Pîrlea;Ilya Sergey
我们提出了基于区块链的分布式共识协议的第一个形式化，并在交互式证明助手中证明了其一致性。我们的开发包括块森林数据结构的参考机制，这是实现可证明正确的每个节点协议逻辑所必需的。我们还定义了一个网络模型，实现协议的形式复制状态转换系统。该协议的执行是通过一个小步骤的异步消息传递，其中包可以重新排列或复制操作语义建模。在这项工作中，我们专注于全球系统安全的概念，证明一种形式的最终一致性。为此，我们提供了一个关于块森林的纯功能实现的定理库，定义了一个归纳系统不变量，并表明，在静态系统状态下，它意味着每个节点的交易分类账的状态的全局协议。我们的发展是参数方面的实现几个安全原语，如散列函数，一个概念的证明对象，验证接受功能，和分叉选择规则。我们精确地验证了这些假设，证明全球系统的共识，并讨论了它们的充分性。本文中描述的所有结果在Coq中形式化。
We present the first formalisation of a blockchain-based distributed consensus protocol with a proof of its consistency mechanised in an interactive proof assistant. Our development includes a reference mechanisation of the block forest data structure, necessary for implementing provably correct per-node protocol logic. We also define a model of a network, implementing the protocol in the form of a replicated state-transition system. The protocol's executions are modeled via a small-step operational semantics for asynchronous message passing, in which packages can be rearranged or duplicated. In this work, we focus on the notion of global system safety, proving a form of eventual consistency. To do so, we provide a library of theorems about a pure functional implementation of block forests, define an inductive system invariant, and show that, in a quiescent system state, it implies a global agreement on the state of per-node transaction ledgers. Our development is parametric with respect to implementations of several security primitives, such as hash-functions, a notion of a proof object, a Validator Acceptance Function, and a Fork Choice Rule. We precisely characterise the assumptions, made about these components for proving the global system consensus, and discuss their adequacy. All results described in this paper are formalised in Coq.