区块链研究实验室|形式验证如何帮助防止Gridlock错误( 二 )_最近在Edgeware的Lockdrop智能合约中发

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

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

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

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

形式验证可以帮助吗？

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