智能合约自动化审计技术浅析

媒介

颠末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这两种系统的一个详细的架构以及实现措施。

[1] [2]下一页

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后面。这两种差别定了它全部逻辑的一个框架。

第一个便是它的一个数据,它怎么定义合约里面的数据变更?分了三种,第一种是MayDepOn,便是两个身分,一个叫Y、一个叫T,T变Y可能变也可能不变。

第二个便是Eq,便是说Y是由T来抉择的

第三个便是大年夜家把DetBy和Y和T是逐一对应的,只要T变Y就肯定要变了。

这里面就用加倍形象的措施,我们想象一下,MayDepOn便是,变量是T,在一段光阴傍边Y可能是一个值,然后有的说T变Y可能不变,第三个DetBy便是说一对一的关系,就比如说我们知道哈希,哈希假如T变,Y就肯定要变。

经由过程逻辑和数据这两个维度进行了一些验证,终极验证模块的话,现在供给了大年夜概六七个智能合约破绽的验证性的说话,而且这种说话都因此插件化的形式来写的,其他的安然开拓者可以赓续去富厚这个破绽的验证说话,终极我们在对自动化审计进行一个评估的时刻,我们着实是要从它的自动化程度,漏报率、误报率来评估这件工作的。

像我们现在知道的一些数据就可以注解出来,着实像Mythril跟Oyente,它里面存在大年夜量的误报,比如说它检测出来的数据照样必要人工进行二次确认,这个事情着实是异常繁琐,而Securify这种措施可能误报率会低落。

这也是两种对照现在对照盛行的符号履行和抽象的自动化审计措施。

四、总结回首

着末我们回首一下,现在做的智能合约审计的话可能分为三种,:特性代码匹配、形式化验证以及符号抽象。

回首全部解释的历程傍边,我们可以清楚地知道,现在自动化审计的措施着实是出于一个很不成熟的阶段。

它们主要面临三大年夜问题:

第一个便是误报率高,着实它并不能做到完全自动化,它还必要人工的一些介入。

第二个便是它的自动化着实程度对照低,还必要赓续有feedback去去审计。

第三便是审计光阴对照长,比如说像Mythril,匀称在60秒,Oyente大年夜概在30秒,而Securify大年夜概在20秒。

上一页[1] [2]

赞(0) 打赏
分享到: 更多 (0)
免责申明:本站所有资料均来自于网络,版权归原创者所有!本站不提供任何保证,不保证真实性,并不承担任何法律责任

评论 抢沙发

  • 昵称 (必填)
  • 邮箱 (必填)
  • 网址

阿里云优惠网 更专业 更优惠

阿里云优惠券阿里云大礼包