智能合约自动化审计技术浅析 – 作者:猎豹区块链安全实验室-安全小百科

前言

经过THE DAO事件、币安被盗事件，智能合约的安全性越来越受到业内关注。本文根据猎豹区块链安全专家杨文玉9月5日在星球日报P.O.D大会上的分享录音整理而成，浅析当前智能合约的发展现状，以及智能合约自动化检测的一些方法。

一、智能合约发展现状

首先我们来一起看看现在智能合约发展的一个现状：在过去一个月当中，智能合约的数量每天还在以1317个的平均增长率高速稳定的增长着，这和我们所理解的“区块链现在处于寒冬的时期”不太一样，其实智能合约的增长率还是比较稳定的。

现在智能合约比较多的应用在一些基础设施、商业零售、游戏以及社交媒体和通讯领域中。

二、智能合约安全现状

从17年9月到18年6月，智能合约的漏洞频繁爆发，每次漏洞爆发都带来了大量的资金损失。这使得一些区块链开发者、智能合约的开发者或者一些用户对智能合约安全性产生高度的质疑，也阻碍了以太坊之后的一些发展。

除了基本的智能合作安全，现在DAPP的安全也是受到了极大的关注。比如说FOMO3D在兴起的时候，仅仅在第二天就出现了大量的山寨合约、山寨的游戏。在这些游戏中，开发者巧妙地更改了资金分配的逻辑，使得玩家在玩FOMO3D游戏的过程中，投入的资金其实大部分都是流向于这种山寨合约的开发者的，这对DAPP的发展有了极大的阻碍。

现在我们共同面临着一个问题——如何保证海量的智能合约的安全。

三、智能合约自动化审计方法

我们来回顾一下现在智能合约的情况。截止到昨天中午12点，据统计，现在共有193万个智能合约，并且一直保持着稳定的日增长率。现在的审计方法有人工的攻防审计以及自动化的审计。

在海量的智能合约中，最好的一种设想就是要降低人工审计的一些复杂度，从而更多的通过自动化审计来进行。

我们把自动化审计分为三个部分：

第一种就是特征代码的匹配，第二类就是基于形态化验证的自动化审计，最后一类是基于符号执行和符号抽象的自动化审计。

1、特征代码匹配

我们首先看这一项，特定代码匹配。大家从名字上来看应该就能理解到，其实它就是对恶意代码进行一些提取抽象，像我们之前做的代码静态检测，我们抽样成一种语义匹配，然后再去匹配它的静态源代码。

这种审计的方法的优点是显而易见的，比如说速度很快，因为它就是对原码进行一个字符串的匹配。第二是它能够迅速的响应新的漏洞，因为这种审计方法大部分是以插件形式开发，比如出现了一个新的漏洞，我们就可以快速提交一些新的匹配模式。

那么它的缺点在哪里呢？我们所理解的现在的区块链都应该是公开透明的，但实际情况并不是这样，我们大概做了一个统计，目前代码的开源率仅仅只占48.62%，

也就是在以太坊上其实有超过一半的智能合约是不开源的，只暴露它的一个OPCODE。

对于OPCODE的分析对于安全人员来说其实也是面临着巨大的挑战，有些人费了十分大的力气，去逆向OPCODE，这就导致了它的适用范围极为有限。

其次就是漏报率高。因为它的一些静态审计方法其实并不和传统的静态代码审计方法一致，传统的静态审计方法，比如说APP检测，我会调用库里面，确定稳定的一些函数，来对它进行审计，但智能合约里面它的一些函数、它一些特征等等，还是变化性比较多的，所以说它的漏报率会比较高。

2、基于形式化验证的自动化审计

第二个方法，我们来探讨一下现在比较火的，基于形式化验证的自动化审计。

形式化验证来审计智能合约安全，最早是在16年，由Hirai提供的，当时拿Isabelle高阶逻辑交互定理证明器，然后交EVM的一些OPCODE ，通过它的一个lem language转化成了一个形式化的model，然后通过形式化model的验证来去判断它代码中的逻辑是否存在问题。

而基于这项工作，之后由两个学家把形式化方法进行了进一步的改正，也就是说他们放弃了lem language这种比较低效的转换方式，采用了F-framework和K-framework将DVM转化为一个formal model，而F-framework就是NASA他们经常在航空航天领域当中做一些形式化漏洞验证的框架，而K-framework就是语意的一些整合框架。

3、基于符号执行、符号抽象的自动化审计

第三点，也是我今天想要着重跟大家交流的，以及现在最常用的方法，就是基于符号执行和符号抽象的一些自动化审计。

我们在分析一个智能合约的时候，我们首先要明确我们的分析对象是什么。也就像我们刚才在解释的那个特征匹配代码当中，我们知道其实现在EVM上合约代码大部分是不公开的。

我们就确认应该是一个EVM OPCODE，通过一些源码，编译，可以形成一个OPCODE，然后输入到我们自动化分析引擎。

在这种基于符号执行和符号抽象化的自动化审计框架里面，其实它有些共有的特性，就是它在OPCODE或者在输到这个引擎之后，都会转化成一个CFG，就是我们的一个Control flow graph，即控制流程图。

可以简单了解一下这个CFG是什么意思。CFG就是说他把合约代码里面的逻辑包装成每个块，然后有逻辑有分叉的时候，比如说有IF等等这种判断的时候，就把它分叉。

比如说左边这个assertion这个合约，我们首先是将input与256进行一个比较，那么在出现一个If的判断之后，我们需要对这个CFG进行一个分叉。

CFG Builder主要是对OPCODE这种智能合约代码，把它形成一个十分庞大完善的一个CFG，然后让程序员更好的去了解它里面执行的一些逻辑。再有CFG生成了之后，就是这样两种分析方法。

第一类就是基于符号执行的验证，这边比较有代表性的，可能大家都比较熟知的像Mythril、Oyente、Maian。还有一种就是，上个月他们刚刚公开的一个符号抽象分析的方法，也就是Securify。

下面主要分析一下Oyente以及Securify这两种系统的一个具体的架构以及实现方法。

Oyente符号执行验证

Oyente的逻辑是在CFGbuild形成之后，首先是一个EXPLORER，EXPLORER的意思就是说我会把代码当中的每一个流程都去验证一遍，进行一个之外的验证。

我们的验证就是是否有一个X，使得X不仅满足C1、C2、C3三个条件，并且Z=X+2，那么这时候我们可以判断他的状态是no还是yes，然后以此来验证整个逻辑的一个流程。

到了第二个code analysis，这一部分其实是这个Oyente最为核心的一个部分，就是它将刚刚输出的EXPLORSE这种路径把它转化，至始至终只包含Ether的一些路径，进行一些漏洞验证，而他目前只提供包括TOD、Timestamp dependence、Mishandled exceptions这三种验证，最后系统为了保证误报率和漏报率，采用了微软的Z3Bit-Vector Solver 开源的验证器，然后来进行整体架构的一个封装。

在刚刚我们讲述的过程当中，其实大家也应该了解到，在CFG转EXPLORER验证的时候，我们需要对它的循环的每次都进行一个验证，所以说这种分析方法特别耗时，并且也不一定成功。

比如说像parity的那个钱包代码，它的Oyente覆盖率仅仅达到20%，剩下80%的代码，是没有办法去跟踪的，所以这就是Oyente目前存在一个巨大的问题。

Securify符号抽象分析

在这个问题的基础上，像Securify他们就提供了另外一种方法，它们认为现在合约代码其实是特别容易解耦合的，不像我们传统的代码一样，它的耦合性特别高，但像合约代码里面，就有transfer等等一些比较固定解耦合的一些结构和模块，我们并不是需要对整个合约的逻辑进行的校验，可能我们就是对合约解耦合的各个模块进行校验分析，因此可以提高它的自动化程度。

这张图也就是他们整个在验证的一个流程：

它们把contract bytecode转化成一种他们自定义的一种语义语言，然后通过自定义的语义语言，它们之后有一个验证模块，这个验证模块就特别像我们之前说的那种模式匹配，就是把一些漏洞转化成一种它验证语言的模式匹配的框架，然后去验证它这个语意在此是否满足他这个比较，最终会生成一个安全报告。

这里也给出了一个parity的例子，通过自动化审计的方法，最终可以输出钱包的owner其实是可以被修改的。

再具体一点，它是怎么做语义分析的呢？Securify分析这种合约代码，是从两个维度，第一个是逻辑，第二个是数据。

在逻辑方向的话，它定义了两种逻辑，第一个叫MayFollow，第二叫MustFollow。MayFollow的意思是说L2是有一条路径是跟在L1后面的，而MustFollow是说L2每一条路径都跟在L1后面。这两种区别定了它整个逻辑的一个框架。