形式化验证（Formal verification）如何确保完美的智能合同？

智能合约安全性是非常重要的。之前，我也写过关于以太坊字节码中常见安全问题的文章，但是像这样的大概检测只是浮于表面。理想情况下，我们想要保证我们的智能合约能够100%的正确。形式化验证（Formal verification）让我们可以确保某种错误的状态不会发生。

现在已经有很多对以太坊虚拟机语义模型的学术研究以及对使用不同框架的智能合约进行的形式化验证。在这篇文章中，我会描述一种基于符号执行和Z3定理证明的方法，并证明这个方法能够检查出很小的错误，例如那些因为Solidity内存寻址机制导致的。

我们选择Ownable作为例子，这是一个很常用的基础合约，可以将编写者的状态定义为构造器，调节器，以及转换编写者的作用。

计算状态空间

第一步是象征性地执行代码，并且将所有可能的程序状态展现出来。每个状态都由一系列具体或者符号值组成，同时也伴随着合同账单（存储量，剩余值。。。），还有虚拟机环境（程序计数器，调用数据等等），同时还有一系列的路径约束，也就是说只有满足了这些需求才能达到那种特定的状态。

Mythril的符号执行引擎通过完全自动化地方式计算出状态空间。为了通过这些代码来将可能的路径可视化，我们可以通过myth命令工具来绘制控制流图。

最后可以得到一张图表，其中包含了整个程序流程的概览。图表中每个节点，都代表一个基本代码块，边则表示路径条件。

完全映射的状态空间并不是总能存在：类似无界循环与递归契约的命令会导致状态的数量呈现指数级增长。不过由于以太坊的燃料概念，我们可以确定这种执行操作总是会停止。接下来，关于这点我会写更多，现在我们先专注于最简单的例子。

参数

如果有Ownable合约编译后的字码节，我们就可以尝试去证明Ownable按照以下安全特性的标准来说，是正确的。

“所有权只能够由合约拥有者自己转移。”

如果使用以太坊黄皮书的说法正式来说，这个安全特性可以描述为：全网状态用σ表示，机器状态用μ表示，以此类推。其中一些标记会在以下的图中解释，但是如果你不是很熟悉，可以先看下以太坊的黄皮书。

根据Solidity编译协议，owner这个参数是在0号存储槽（这个可以通过检查编译代码来进行确认）。因此，我们只对状态转移中σ => σ′部分的子集感兴趣，在0号存储槽里的内容也会因为改变：

根据以太坊虚拟机语言的定义，只有SSTORE命令可以改变整体状态。因此我们可以更容易地通过对总体状态中选择获得相关初始状态σ，以及机器状态 (σ, μ)：

如果可以满足下面的逻辑公式，错误状态就会出现。

用通俗的话说，我们尝试去证明在整个程序中不可能有某个点存在，在这个点上，不同的所有者可以进行切换，但是msg.sender命令却和现在的所有者不符合。

将这些参数写入Python程序

下面的程序将进行穷举搜索的方法来解答上面说的公式。如果这个公式在Ownable的状态空间下可以满足，我们就会得到一系列的确定值（状态和输入参数），这些数据会和参数不一样。反过来，如果这个公式最后证明不成立，我们就可以下结论，这个合约在给定的参数下是安全的。

在Ownable上运行分析，会得到如下结果：

因为没有找到任何反例，我们可以下结论：对所有者状态参数进行改变的时候，Ownable是安全的，但是有几个附加条件：

-假设以太坊虚拟机总是正确运行
-这个结果只适用于封闭情况下的Ownable合约，对于从其中衍生出来的合约不适用。

检测一个不是很明显的错误

上面得出的结论其实并不是很让人吃惊：看下Solidity的代码，很明显这些参数总是有的。但是有趣地是，我们的分析工具可以检测任何种类的错误，包括很小的错误，不会被被编写人员发现。考虑使用Pwnable.sol，经过修改的Pwnable.sol，增加了动态数组。

下面的结果，看起来也没这么糟糕：毕竟，transferOwnership()仍然是编写主变量的功能，而且是被onlyOwner()调节器。但是这次，分析工具开始抱怨了：

很明显，某些输入导致了主变量被覆盖。最后结果证明，是由于动态尺寸数组被覆盖：

-数组长度被储存在1号存储槽
-数据被存储在了地址keccak(1) + offset上。

当offset被设置为(MAX_UINT — keccac(1))，这加起来是零，所以我们是在零号存储槽获取数据。要注意这不仅是因为a1.length是在构造函数。但是，相同的问题也会偶尔发生：在Solidity中，数组长度变量经常是被管理解析的，而且 array.length—是一个常用的符号。

开发

为了解决这个问题，我们需要做的就是创造一个功能指令，能够把输出作为分析工具。

- calldata_0：功能签名哈希是fun(uint256,address)
- calldata_4: 求解程序找到偏移，必须要满足2**256 — keccak256(1))

这个由求解程序得到的偏移值可以使用。但是为了清楚说明，以下是它如何在Python中计算的代码。

我们用以下的功能命令结束。

为了确认这实际上可以工作，你可以在remix上部署Pwnable.sol，再通过UI运行这个功能指令。运行后，阅读主机内容应该会返回新地址。

总结

在这篇文字中，我演示了如何通过使用符号执行引擎和SAT解码器来正式地验证智能合约的正确性。这种分析可以证明代币的某些特性，并且能够检验一些很小的错误。

http://www.8btc.com/how-formal-verification-can-ensure-flawless-smart-contracts