与往常一样，在 eth2 前线继续发生着许多事情。除了撰写的进展更新和其他公开的总结外，各客户端团队、贡献者和社区成员/预期验证者们都很忙！

今天，本文将涵盖一些重大的存款合约 (deposit contract) 相关新闻，以及实现规范 v0.12 版本的重要步骤。

摘要

• 新的 Solidity 存款合约已经经过形式化验证，并添加进了 bug 赏金计划中；

• 实现 v0.12 规范版本的 Eth2 多客户端测试网 Altona 预计将于下周发布；

• 继续资助 Sigma Prime 为 beacon-fuzz (多客户端差分模糊测试) 找寻 bug 的工作；

Solidity 存款合约 & 形式化验证

今天，我们要宣布一个全新的、更安全的 eth2 存款合约版本，使用 Solidity 语言编写！该合约保留了相同的公共接口 (添加了 EIP-165 supportsInterface 函数)，因此这是对所有现有客户端和开发工具都是完全透明的更改。实际上，其中的 Solidity 代码主要是对最初的 Vyper 合约逐行地翻译 (备注：最初的存款合约使用 Vyper 语言进行编写) ，以帮助进行审查和形式化验证。

在过去的几个月里，Alex Beregszaszi 使用 Solidity 语言重写了这个 eth2 存款合约，该合约已经由一个 Solidity 专家小组审核，并通过了 Runtime Verification 进行形式化验证，大量重用了最初为 Vyper 版本合约编写的 K 规范。

尽管之前的 Vyper 合约经过了严格的测试、审查和形式化验证，但仍然存在着对 Vyper 编译器目前的安全性的潜在担忧。在最初的 Vyper 字节码验证期间，发现了多个编译器 bug (并进行了修复)。除了形式化验证，Suhabe Bugrara (ConsenSys 的研发人员) 还对 Vyper 存款合约和形式化验证进行了审查，这引发了对正式的规范进行了许多改进 (这最终有助于对 Solidity 合约的重新验证)。尽管 Vyper 合约的形式化验证被评估为是可靠的，但只要该合约使用 Vyper 编译器，Suhabe 就不推荐其字节码是安全的。

同时，ConsenSys Diligence 和 Trail of Bits 对 Vyper 编译器进行了安全调查报告，发现了更多的 bug，并对该编译器代码库的系统性问题提出了担忧。

尽管有这些发现，Vyper 仍然是一种很有前景的语言。基于 python 的编译器仍在开发中，许多贡献者正在研究对这种语言进行形式化，并研究其他编译器。

虽然我们对经过了形式化验证的字节码很有信心，但在 Vyper 编译器中发现的问题使得我们严重依赖于对字节码进行验证。最好是从一个通常被认为安全的编译器开始，然后验证字节码，而不是从一个存在已知问题的编译器开始，然后验证这些已知 (或未知) 问题没有在字节码中出现。 (责任编辑：admin)