猎豹区块链研究中心杨文玉：智能合约自动化审计存在误报率高、自动化程度低及审计时间长三大问题 | 星球日报P.O.D大会

编者按：本文来自36氪战略合作区块链媒体“Odaily星球日报”（公众号ID：o-daily，APP 下载）。

区块链这三个字近年经历了几番跌宕，从前沿的技术概念、风口上的热词，到被过度消费的符号。很多人相信，区块链是解决许多行业痛点的工具，有潜力成为下一个世代“超级商业载体”诞生的催化剂。

然而，传说中的史诗级变革还未来临，它就已被置于聚光灯之下。有心者从中渔利，趋利者盲目买单。而过早陷入舆论漩涡，对成长期的技术是伤害，也是试炼。  

今天的实际情况是，落地应用寥寥无几，技术和产业连接尚有距离，投机者的噪音盖过了真正关注技术与行业的“中坚声音”。Odaily星球日报联合顶级新商业媒体36Kr、顶尖技术领袖和学界菁英，共同探讨如何拥抱监管，推动行业去粗取精，将流量与话语权交给认真做事的人，用实力让区块链落地。

9 月 5 日，在由 Odaily星球日报主办、36Kr 集团战略协办的 P.O.D 大会安全论坛上，猎豹区块链研究中心安全专家杨文玉发表题为《智能合约自动化审计技术》的演讲。

杨文玉开场介绍了智能合约发展的现状。大部分人认为区块链现在是一个寒冬时期，但是据猎豹区块链研究中心统计，过去一个月中，智能合约每日新增数量为 1317 个。研究中心收录的项目中，区块链基础设施占 9.38%，游戏和 VR 4.44%，商业和零售 3.6%，社交媒体与通讯 3.4%。

在数量稳定增长的同时，智能合约还面临着安全问题。从 2017 年到 2018 年 6 月，智能合约漏洞频繁爆发，带来大量资金损失，也使得区块链甚至智能合约的一些开发者或者用户对智能合约的安全性产生质疑，也阻碍了以太坊之后的发展。

除此之外，Fomo3D 在兴起的时候，仅仅在第二天就出现了大量的山寨合约。山寨 Fomo3D 游戏开发者更改了积极分配的逻辑，导致投入的资金大部分都流向山寨合约开发者，也对 DApp 发展造成阻碍。

在这样的背景下，如何有效保障海量智能合约的安全？杨文玉认为，最好的方法是降低人工审计复杂度，采用智能合约自动化审计。

具体来讲，自动化审计方法主要分为三类：

• 第一种是特征代码匹配，就是对恶意代码进行提取、抽象，形成匹配模块对待检测源码进行检测。优点是速度快、迅速响应新漏洞，缺点则是使用范围有限、漏报率高。
  

• 第二种是基于形式化验证的自动化审计方法。最早是在 2016 年由 Hirai 提供，Grishchenko 和 Hildenbrandt 之后进行了改进，采用 F*framework 和 K framework，将 EVM 转化为一个 Formal  model。Formal 是航空航天领域常见的形式化验证框架，而 K framework 则是一个语义的转化框架。
  

• 最后一种是现在最常用的方法，基于符号执行和符号抽象自动化审计。分析智能合约时，通过编译源码，可以形成 EVM OPCODE，然后输入到自动化分析引擎，转化成 CFG，再利用这两种方法进行分析。比较典型的是 Oyente 和 Securify 系统，可以降低误报率和漏报率，但是分析方法繁琐并且耗时。
  

不过，杨文玉也指出，现在自动化审计方法处于一个很不成熟的阶段，主要面临三大问题：误报率高，自动化程度低、依赖人工二次审计，审计时间比较长。

以下为杨文玉演讲全文，enjoy：

谢谢大家，今天非常荣幸来参加这个会议，今天我所带来演讲主题就是我们一起来浅析一下当下智能合约自动化安全检测的技术，今天我的演讲可能分两位个部分，首先第一部分我们会一起来看一下现在以太坊上智能合约发展的现状，第二部分基于这个现状了解，再详细描述一下现在智能合约自动化涉及的一些方法。

首先我们一起看一下现在智能合约发展的一个现状，根据我们平台，可以知道在过去一个月当中，智能合约的数量每天还在以 1317 个的平均增长率高度稳定地增长着，可能和我们所理解的区块链现在是一个寒冬时期，所不太一样这种增长率还比较稳定的。其次我们通过一些 NLT 方法，把智能合约领域划分出来，除了一些敏感领域，现在智能合约比较多的应用在一些基础设施，商业零售，游戏以及社交媒体和通讯。这是一个智能合约大的现状，智能合约现在面临一个安全现状是什么样的，可能刚才两位嘉宾已经都进行了非常详细的描述，从 2017 到 2018 年 6 月，这种智能合约漏洞频繁爆发，每次都带来大量资金损失，也使得区块链甚至智能合约的一些开发者或者一些用户对智能合约这种安全性产生一些高度的质疑，也阻碍了以太坊之后的发展。

除此之外，我们还可以看到像刚才嘉宾讲到 Fomo3D 这件事情，除了基本智能合约安全，现在安全受到极大的关注，之前 Fomo3D 在兴起的时候，仅仅在第二天就出现了大量的山寨合约，山寨的 Fomo3D，在这种游戏当中，其实开发者更改了积极分配的逻辑，使得其实玩那个蜂窝游戏过程当中，投入的资金大部分都是流向山寨合约开发者，也对 DApp 发展造成阻碍。

现在面临一个问题是如何有效保障海量智能合约的安全，也是我们今天要讨论的问题，也是第二部分想跟大家分享一个现在智能合约自动化审计技术的发展。

再回顾一下，现在智能合约截止到昨天中午 12 点，以太坊总共有 193 万个合约，日增长率稳定增长，现在审计方法有人工审计，以及自动化审计。在海量智能合约当中，我们最好的方法就是降低人工审计复杂度，从而让更多通过自动化审计进行。我们把自动化审计分为三个部分。首先第一种是特征代码匹配，第二类是基于形势化验证的子都化审计方法，最后一种是基于符号执行和符号抽象自动化审计。

首先看特征代码匹配，从名字可以很清晰理解到，就是对恶意代码进行提取抽象，我们是一种语义匹配，匹配静态原代码，审计的方法优点是很显而易见的，比如说速度很快，因为对源码进行一个字符串匹配，第二个可以迅速进行新的漏洞，他审计出现一个新的漏洞，我们就可以快速提交一些新的匹配模式。他缺点在哪里，再来看一下，我们所理解的现在区块链都上应该是公开透明的，但实际情况并不是这样，我们大概做了一个统计，目前代码的开原率仅仅只占 48.62%，就是说在以太坊上，其实有超过一半合约是不开源的，只暴露 code，刚刚那个嘉宾也说，他们也费了十分大的力气去立项这个 code 这种限制就导致这种方法使用范围有限，传统的静态审计方法比如说 App 检测，会调用一个库里面确定唯一一些函数，对他进行审计，智能合约里面一些函数一些特征变化性比较多的，所以说漏洞率比较高。

第二个方法，我们就来探讨一下现在比较火的，基于形式化验证的自动化审计，形式化验证审计智能合约安全，最早是在 2016 年由 Hirai 提供的，他提出了一点，他当时拿出逻辑交互证明器，通过 Isabelde  lem-Language->Formal-model，通过形式化 model 验证，来判断代码逻辑是否存在问题，这项工作最后的两个把形式化方面进行进一步改造，他们放弃 Lem-language 也是比较低效的转化方式，他们采用了 F*framework 和 K framework，将 EVM 转化为一个 Formal  model，而 Formal 可能就是经常在航空航天领域当中做一些形式化验证的框架，而 K framework 则是一个语义的转化框架，这两个比较有代表性的技术研究，如果想更加深入了解可以参考下列的一些论文。

第三点就是今天想要着重跟大家交流，以及现在最常用的一些方法，就是基于符号执行和符号抽象的自动化审计，这种自动化审计现在看一下，我们在分析一个智能合约的时候，首先要明确分析对象是什么，像我们刚才在解释特征匹配代码当中，我们知道现在 EVM 上智能合约代码大部分是不公开的，我们现在分析对象就确认应该是 EVM  OPCODE，在通过一些源码，我们通过编译，可以形成 EVM OPCODE，输入到自动化分析引擎。在这种基于符号执行和符号抽象化自动化审计框架里面，有些共有的特性，OPCODE 在输入这个引擎当中，都会转化成一个 CFG，就是一个一个控制流程图，通过这个 CFG，可以简单了解一下这个 CFG 是什么意思，CFG 就是把合约代码里面逻辑包装成哪个快，在里面逻辑分叉的时候，左边那个合约形成一个十分庞大完善的 CFD，让程序员更好了解能够执行一些逻辑。

在有 CFG 生成之后，现在就出现两种分析方法，第一类就是基于符号执行的验证，这类比较有代表性，大家都比较熟知像 Mythril、Oyente、Maian，还有一种就是上个月刚刚公开的一个符号抽象分析的方法，就是 Securify，今天主要跟大家讲一下 Oyente 跟 Securify 这两种系统具体的架构以及实现方法，首先我们来看 Oyente，Oyente 的逻辑我们可以从左边看到，在 CFG 申请之后，首先是一个 explorer，会把代码当中每一个流程验证一边，进行一个形式化验证，就像这个我们验证是我们是否有一个 X，使得 X 不仅满足 C1、C2、C3 条件，这时候可以判断状态是 no 还是 yes，以此验证整个逻辑的流程。第二个 core analysis 这一部分其实是 Oyente 最为核心的一个部分，将刚刚输出的 explorer 这种路径，把它转化，只进行一些漏洞验证，目前只提供包括 TOD 和 Timestamp  dependence 和 Mishandled exceptions，这三种验证，最后这个系统又能保证误报率和漏报率，他采用微软的开源的验证器，进行整体的架构封装，在刚刚我们讲述过程中，大家也应该了解到，在 CFG 转 explorer 验证的时候，我们是需要对他的循环，每次都是一个验证，所以这种分析方法特别耗时，并且不一定成功。这就是 Oyente 目前存在一个巨大问题。

在这个问题基础上，像 Securify，他们就提供了另外一种方法，他们认为现在合约的代码其实是特别容易解耦合的，不像传统代码，耦合性特别高，像合约代码这个一些比较固定形式化的解耦合模块，我们并不是需要对整个合约逻辑进行一个交验，我们对合约解耦各个模块进行分析，以此提高自动化程度，左边这个图是整个验证流程，把 contract bytecode 通过定义域语言之后有一个验证模块，特别像之前说的模式匹配，把一些漏洞转化成验证语言模式匹配框架，验证这个语义是否磨合这个。最后也给出一个 report，通过这个自动化审计方法，最终可以输出钱包的管理者是可以被修改的。

再具体一点是怎么做语义分析，其实分析这种 explorer 代码是从两个维度，第一个是逻辑，第二个是数据，逻辑方式定义两种逻辑，第一个叫做 MayFollow，第二个叫做 MustFollow，MayFollow 的意思就是说，L2 必须是有一条路径跟在 L1 后面，而 MustFollow 是说 L2 每一条路径都跟在 L1 后面，这两种区别定义了整个逻辑的框架。

第二个是数据，怎么定义合约里面数据变化用了三种，第一个 MayDepOn，就是两个因素，一个叫做 Y，一个叫 T，T 变 ，Y 可能变也可能不变。第二个是 Eq，就是 Y 是由 T 决定的。第三个是 DetBy，Y 和 T 是一一对应的，只要 T 变 Y 肯定要变了，这里面用更加形象的方法来想象一下，其实 Maydepon 就像我们的 T 变量是 time，在一段时间中，Y 可能是一个值，T 变， Y 可能不变，第三个就是说一对一关系，就像我们算哈希，只要你 T 变，Y 肯定要变，通过逻辑和数据这两个维度，他们进行一些验证，最终验证模块现在提供了大概六、七个智能合约漏洞验证性的语言，这种语言都是以插件化来写的，其他的安全开发者可以在不断丰富漏洞的验证语言。

最终我们在对自动审计进行评估的时候，是从要自动化程度、漏报率、误报率提供这件事情，我们现在知道数据就可以绑定出来，检测出来数据还是需要人工进行二次确认，这个工作是十分繁琐的，经过这种方法可以是误报率会降低，这两种符号执行和符号抽象的自动化审计方法。

最后回顾一下，现在自动化审计方法分为三种，特征代码匹配，形式化验证以及符号执行、符号抽象。回顾整个浅析过程，我们可以清楚知道，现在自动化审计方法是在一个很不成熟的阶段，主要面临三大问题，第一个是误报率高，并不能做到完全自动化，还需要人工参与。第二个是自动化程度比较低，还需要不断去审计它，第三个审计时间比较长。

最后就是回顾一下我们整个分析，首先我们明晰一下智能合约发展现状，又检测自动化审计方法，左右各有我们技术交流群，有感兴趣小朋友欢迎加入，可以一起更加深入的讨论，这就是我今天所分享的内容，谢谢。