欢迎来到 黑吧安全网 聚焦网络安全前沿资讯,精华内容,交流技术心得!

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

来源:本站整理 作者:佚名 时间:2018-09-30 TAG: 我要投稿

前言
经过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]  下一页

【声明】:黑吧安全网(http://www.myhack58.com)登载此文出于传递更多信息之目的,并不代表本站赞同其观点和对其真实性负责,仅适于网络安全技术爱好者学习研究使用,学习中请遵循国家相关法律法规。如有问题请联系我们,联系邮箱admin@myhack58.com,我们会在最短的时间内进行处理。
  • 最新更新
    • 相关阅读
      • 本类热门
        • 最近下载