智能合约自动化审计有哪些类型?主要优缺点有什么?

智能合约可以说就是传统合约的数字化版本,其本质是一段运行在区块链网络中的代码,合约在满足其源代码中写入的条件时,自行执行,它允许在没有第三方的情况下进行可信交易,这些交易可追踪且不可逆转。

智能合约使很多不同类型的程序和操作得以自动化,极大程度推动了区块链技术的发展,但也正因为在区块链应用中,区块链的不可篡改性,智能合约也是不可更改的,智能合约如果出现安全隐患,对用户造成的损失也将是是巨大且不可挽回的。

例如智能合约中有代币存在,一旦合约存在的漏洞被利用,就可能导致丢失大量加密货币、扰乱金融秩序等极为严重的后果。

然而在代码的设计和开发过程中,不可避免出现漏洞,这意味着智能合约不可避免的会出现安全漏洞。

事实也正是如此,随着区块链技术地发展应用,越来越多地人关注到区块链技术,智能合约数量越来越多,合约涉及的金额也飞速增长,同时智能合约的安全也逐渐暴露出存在的问题。

在此背景下,单纯的从第三方的人工角度审计来说,可能已经跟不上合约发展了,所以自动化审批现在也是大家比较关注的。

目前,自动化审计大约分成三种类型:基于特征码代码的匹配、基于形式化验证自动化检测和基于符号执行、符合抽象的自动化审批。

1、特征代码匹配

特征代码匹配就是对恶意代码进行提取、抽象,形成匹配模块对待检测源码进行检测。

这种审计的方法的优点是显而易见的,比如说速度很快,因为它就是对源码进行一个字符串的匹配。

而且,它能够迅速的响应新的漏洞,因为这种审计方法大部分是以插件形式开发,比如出现了一个新的漏洞,我们就可以快速提交一些新的匹配模式。

但它的缺点也很明确,我们所理解的现在的区块链都应该是公开透明的,但实际情况并不是这样,根据相关的数据,目前代码的开源率仅仅只占48.62%。

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

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

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

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

形式化验证来审计智能合约安全,最早是在 2016 年由 Hirai 提供,Grishchenko 和 Hildenbrandt 之后进行了改进,采用 F*framework 和 K framework,将 EVM 转化为一个 Formal model。

Formal 是航空航天领域常见的形式化验证框架,而 K framework 则是一个语义的转化框架。

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

分析智能合约时,通过编译源码,可以形成 EVM OPCODE,然后输入到自动化分析引擎,转化成 CFG,再利用这两种方法进行分析。

《智能合约自动化审计有哪些类型?主要优缺点有什么?》

《智能合约自动化审计有哪些类型?主要优缺点有什么?》

《智能合约自动化审计有哪些类型?主要优缺点有什么?》

比较典型的是 Oyente 和 Securify 系统,可以降低误报率和漏报率,但是分析方法繁琐并且耗时。

我们回顾这三种方法可以发现,目前自动化审计的方法还处于一个发展的阶段,目前他们主要面临三个大的问题:

第一、它的自动化其实程度比较低,还需要不断有feedback去去审计;

第二、误报率高,其实它并不能做到完全自动化,它还需要人工的一些参与;

第三、就是审计时间比较长,比如说像Mythril,平均在60秒,Oyente大概在30秒,而Securify大概在20秒。

点赞