以太坊2.0 Beacon Chain的形式化验证
Formal Verification of the Ethereum 2.0 Beacon Chain
摘要：
我们报告我们的经验，在形式化验证的参考实现的信标链。Beacon Chain是新的权益证明以太坊2.0网络的骨干组件：它负责跟踪有关验证者，他们的权益，他们的证明（投票）的信息，如果发现一些验证者不诚实，就削减他们（他们失去了一些权益）。信标链是关键任务，其中的任何错误都可能危及整个网络。由以太坊基金会开发的Beacon Chain参考实现是用Python编写的，并提供了每个Beacon Chain的网络参与者（节点）必须实现的状态机的详细操作描述。我们已经正式指定并验证了使用验证友好语言Dafny的Beacon Chain参考实现（大部分和关键部分）中不存在运行时错误。在这项工作的过程中，我们发现了几个问题，提出了经过验证的修复方案。我们还综合了功能正确性规范，使我们能够提供超出运行时错误的保证。我们的软件产品可以在https://github.com/ConsenSys/eth2.0-dafny上找到。
英文摘要：
We report our experience in the formal verification of the reference implementation of the Beacon Chain. The Beacon Chain is the backbone component of the new Proof-of-Stake Ethereum 2.0 network: it is in charge of tracking information about the validators, their stakes, their attestations (votes) and if some validators are found to be dishonest, to slash them (they lose some of their stakes). The Beacon Chain is mission-critical and any bug in it could compromise the whole network. The Beacon Chain reference implementation developed by the Ethereum Foundation is written in Python, and provides a detailed operational description of the state machine each Beacon Chain's network participant (node) must implement. We have formally specified and verified the absence of runtime errors in (a large and critical part of) the Beacon Chain reference implementation using the verification-friendly language Dafny. During the course of this work, we have uncovered several issues, proposed verified fixes. We have also synthesised functional correctness specifications that enable us to provide guarantees beyond runtime errors. Our software artefact is available at https://github.com/ConsenSys/eth2.0-dafny.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
