以太坊 2.0 信标链的正式验证
编程语言
2021-10-26 v1 计算机科学中的逻辑
摘要
我们报告了在信标链参考实现正式验证方面的经验。信标链是新的权益证明以太坊 2.0 网络的骨干组件：它负责跟踪有关验证者、其权益、其证明（投票）的信息，并且如果发现某些验证者不诚实，则对其罚没（他们失去部分权益）。信标链是关键任务组件，其中的任何错误都可能危及整个网络。由以太坊基金会开发的信标链参考实现用 Python 编写，并提供了每个信标链网络参与者（节点）必须实现的状态机的详细操作描述。我们使用验证友好语言 Dafny 对信标链参考实现（很大且关键的部分）中的运行时错误进行了形式化规范与验证。在此工作过程中，我们发现了若干问题，提出了已验证的修复方案。我们还综合了功能正确性规范，使我们能够提供超越运行时错误的保证。我们的软件制品可在 https://github.com/ConsenSys/eth2.0-dafny 获取。
引用
@article{arxiv.2110.12909,
title = {Formal Verification of the Ethereum 2.0 Beacon Chain},
author = {Franck Cassez and Joanne Fuller and Aditya Asgaonkar},
journal= {arXiv preprint arXiv:2110.12909},
year = {2021}
}