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

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

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

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

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

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

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

区块链研究实验室|形式验证如何帮助防止Gridlock错误( 三 )