区块链 > 正文

以太坊2.0存款合同的正式验证(第一部分)

2019-07-02 16:35:28来源:

以太坊2.0是一种新的分片PoS协议,在其早期阶段(称为阶段0)与现有的PoW链(称为Eth1链)并行共存。虽然Eth1链由矿工提供支持,但新的PoS链(称为Beacon链)将由验证者驱动。

在Beacon链中,验证者的作用是创建(称为propose)和验证(称为attest)新区块。Beacon链的共识协议建立在重要小工具之上,Casper FFG用于最终区块化,LMD GHOST用于分叉选择规则,RANDAO用于生成随机数。只要大多数验证者在创建和验证新区块时诚实遵循协议,那么就可以保证链其所需的安全性和活跃性。

验证者集群是动态变化的,这意味着新的验证者可以选择加入和旧验证者可以随时选择退出。要成为(新)验证者,需要通过将交易(通过Eth1网络)发送到指定的智能合约(称为存款合同)来存入一定数量的以太币作为“stake”。存款合约记录存款历史,由Beacon链检索以维护动态验证者集群。(不过此存款流程将在稍后阶段发生变化。)

存款智能合约

用Vyper编写的存款智能合约采用Merkle树数据结构来存储存款历史,其中每当接收到新存款时Merkle树将被动态更新(即从左到右依次递增叶子节点)。合约中使用的Merkle树预计非常大。实际上,在当前版本的合约中实现了高度为32的Merkle树,其可以存储多达2^32个存款数量。由于Merkle树的数据量是非常大,所以每次收到新的存款时都需要重建整棵Merkle树是非常不切实际的。

为了减少时间和空间要求,从而节省gas成本,合约采用了增量Merkle树算法。增量算法具有O(h)时间和空间复杂度来重建Merkle树(更精确地,计算高度为h的Merkle树的根),而朴素算法将需要O(2^h)时间或空间复杂度。具体来说,该算法维护两个长度为h的数组,并且更新Merkle树的每次重建都需要仅计算从新叶(即新存款)到根的链,其中链的计算仅需要两个数组,从而实现Merkle树高的线性时间和空间复杂度。

然而,有效的增量算法导致存款合约的实施非常不透明,并且使得确保其正确性变得非常重要。考虑到存款合约的重要性,需要进行形式验证,而这也是最终保证合同正确性的唯一已知方式。

增量Merkle树算法的形式化验证

我们在运行验证时开始对存款合约进行正式验证,今天我们很高兴地宣布我们实现了第一个里程碑,即增量Merkle树算法的形式验证。

具体来说,我们首先严格形式化了增量Merkle树算法。然后,我们提取了存款合约中使用的算法的伪代码实现,并正式证明了伪代码实现的正确性。这意味着存款合约在源代码级别是正确的,也就是说,如果Vyper编译器或EVM字节码级功能正确性没有引入编译时错误,它将以增量方式正确计算Merkle树根。 (实际上,我们的下一个任务是确保字节码级别的正确性。)

意外发现

在我们的形式化和正确性证明工作的过程中,我们发现存款合同的一个微妙的Bug,但已在最新版本中修复以及一些重构建议,可以提高代码可读性和降低gas成本。

让我们详细阐述一下这个微妙的Bug。在我们被要求验证的合约版本中,当Merkle树的所有叶节点都充满了存储数据时,就会触发这个bug,在这种情况下,合约(特别是get-deposit-root函数)错误地计算树的根哈希,返回零根哈希(即空Merkle树的根哈希),而不考虑叶子节点的内容。例如,假设我们有一个高度为2的Merkle树,它有四个叶节点,并且每个叶节点都填充了某些存款数据,分别为D1,D2,D3和D4。虽然树的正确根哈希是hash(hash(D1,D2),hash(D3,D4)),但get_deposit_root函数返回hash(hash(0,0),hash(0,0)),这是不正确的。

由于代码的逻辑复杂,在不重写代码的情况下正确修复此Bug并非易事,因此我们提出了一种解决方法,只是强制永远不要填充最后一个叶节点,即只接受存放最多2^h-1个,其中h是树的高度。但是,我们注意到,在当前设置中触发此Bug行为是不可行的,因为最小沉积量为1以太,并且以太网的总供应量小于130M,远小于2^32,因此填充32高度树的所有叶子是不可行的。

因此,现在我们确信增量Merkle树算法及其存款合约的实现在源代码级别是正确的,接下来,我们将继续正式验证其编译的EVM字节码的行为是否如预期的那样。

相关阅读

  • 电影花絮
  • 电影情报
  • 圈子新闻
  • 电影新闻
  • 电影搜罗
  • 电视剧
  • 影视演员
推荐阅读