最近在Edgeware的Lockdrop智能合约中发现了一个隐藏的DoS错误（称为Gridlock），该合约已锁定了价值数亿美元的以太币。 由于存在此错误，Edgeware必须重新部署合约的稳定版本。因此，当前在主网上并行存在两个Lockdrop合约（旧版本和新版本）。（这意味着您可以向这两个合约中的任何一个发送交易以锁定您的以太币，直到旧的合约遭到攻击并无法使用为止。）

在本文中，我们将回顾Gridlock错误，并讨论形式验证如何有助于防止此类错误。

正如Neil McLaren的博客文章中所描述的那样，这个错误源于一个错误的（但非常合理的）假设，即新创建的帐户余额总是为零。

要了解更多详细信息，让我们看一下原始buggy合约（简化）代码片段：

本质上，lock函数会绕过收到的以太币金额（即msg.value）创建一个新lock合约账户，并确保新创建的账户（lockAddr）具有绕过的以太币余额。

尽管乍看之下看起来不错，但是此代码仅在新创建的帐户的余额为零时才有效，但不幸的是并非总是如此。 这是因为可以预先计算新帐户的地址，因此恶意用户甚至可以在通过lock函数创建之前向其发送一些以太币。 一旦发生这种情况，assert语句将在任何进一步的lock函数调用中继续失败，这意味着该函数将永远无法执行应做的事情，变得完全无法使用。

（请注意，此行为特定于EVM。在可以识别不存在的帐户并禁止其收取资金的其他VM中，该错误可能并不存在。）

形式验证可以帮助吗？

现在让我们解释一下如何通过正式验证，尤其是在EVM字节码级别的验证来发现Gridlock错误。

形式验证的基本过程之一是通过符号执行来探索给定程序的所有可能行为（在这种情况下为Lockdrop合同的EVM字节码）。在这里，我们使用KEVM验证程序来象征性地执行字节码。长话短说，上述lock函数字节码的符号执行将产生以下行为（例如由于用尽gas而导致的功能故障）。

1. 如果在新帐户地址上已经存在一个帐户，且现有帐户的代码为非空或其现时值为非零，则还原（由于第3行的新合同创建失败）。

2. 还原（由于第5行断言失败），如果新帐户地址上已经存在一个帐户，现有帐户的代码为空，其现时值为0，余额为非零。

3. 成功终止后，如果在新帐户地址上已经存在一个帐户，该帐户的现有代码为空，其现时数为零，其余额为零。 （如果现有帐户为非空，则清除其存储。）

4. 如果新帐户地址没有帐户，则成功终止。

（注意，第三个和第四个行为需要更多的条件，例如没有用完gas，或者正确地给出了枚举类型参数，但是为了简单起见，我们在这里省略了它们。）

一旦研究了合同的所有可能行为，下一个重要步骤便是仔细检查每种行为，以确保它是有意或无意的，否则就很难被利用。确实在上述四种可能的行为中，只希望有第四种，并且我们需要分析其他行为以检查它们是否可利用。

如果可以利用第一行为和第二行为，则可以将其用于DoS攻击。但是，据我们所知，第一个行为几乎是无法利用的，因为在密码上很难在给定的特定地址创建合约帐户（即具有非空代码的帐户）。 （为此，需要使用CREATE2操作码来查找对应于特定地址的盐，这与查找SHA3哈希的原像一样困难。）但是第二种行为是可利用的，因为可以轻松地启动一个如前所述，只需向其发送一些以太币即可在任何特定地址的非合同账户（即无代码的账户）。

另一方面，第三种行为（如果可以利用）可以用来耗尽其他人的“locked”以太币，这确实是致命的。然而据我们所知，由于与第一种情况相似的原因，它几乎无法被利用。 （一个人可以很容易地在一个特定的地址“启动”一个帐户，但是很难“拥有”该帐户，因为这需要找到密钥。）

综上所述，对lock函数节码的符号执行可能揭示了这三种不良行为，并且仔细检查它们可能发现其中一种可被DoS攻击利用，从而在部署之前修复了Gridlock错误。

吸取教训

EVM通常是不直观的。

Gridlock错误源自对EVM设计中某些非显而易见部分的错误理解。如果不考虑EVM级别的智能合约，就很容易错过这种EVM问题，并且可能会再次引入类似的bug。

形式验证可以提供帮助。

如果不采用有原则的方法，那么探索所有可能的行为（尤其是在EVM级别）并非易事。形式验证，尤其是它的符号执行过程，可以系统地探索给定智能合约的所有可能行为，这比仅手工检查代码要严格得多。

具体来说，我们的KEVM验证程序使用的是EVM的确切规范（又称KEVM），不会让您摆脱错误的假设。如上所示，它甚至会发现执行路径非常不可能，例如攻击者找到哈希的预映像并将其合同部署到下一个地址的情况。

 形式验证不是万灵丹。

虽然形式验证引导我们系统地探索和严格地推理给定程序的所有可能行为，实际上，它是找到程序的关键问题的最终途径，如果有的话，它仍然需要大量的人工努力，有时在智力上具有挑战性。例如即使我们自动找到了lock函数的三个不良行为，我们仍然需要手动地对它们的可利用性进行推理，这是非常重要的，并且需要安全专业知识。必须确保在手动推理过程中不遗漏任何关键细节。