智能合约使很多不同类型的程序和操作得以自动化，极大程度推动了区块链技能的发展，但也正由于在区块链运用中，区块链的不可修改性，智能合约也是不可变动的，智能合约如果涌现安全隐患，对用户造成的丢失也将是是巨大且不可挽回的。

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

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

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

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

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

1、特色代码匹配

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

这种审计的方法的优点是显而易见的，比如说速率很快，由于它便是对源码进行一个字符串的匹配。

而且，它能够迅速的相应新的漏洞，由于这种审计方法大部分因此插件形式开拓，比如涌现了一个新的漏洞，我们就可以快速提交一些新的匹配模式。

但它的缺陷也很明确，我们所理解的现在的区块链都该当是公开透明的，但实际情形并不是这样，根据干系的数据，目前代码的开源率仅仅只占48.62%。

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

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

还有便是漏报率高，由于它的一些静态审计方法实在并反面传统的静态代码审计方法同等，传统的静态审计方法，比如说APP检测，我会调用库里面，确定稳定的一些函数，来对它进行审计，但智能合约里面它的一些函数、它一些特色等等，还是变革性比较多的，以是说它的漏报率会比较高。

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

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

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

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

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

比较范例的是 Oyente 和 Securify 系统，可以降落误报率和漏报率，但是剖析方法繁琐并且耗时。

我们回顾这三种方法可以创造，目前自动化审计的方法还处于一个发展的阶段，目前他们紧张面临三个大的问题：

第一、它的自动化实在程度比较低，还须要不断有feedback去去审计；

第二、误报率高，实在它并不能做到完备自动化，它还须要人工的一些参与；

第三、便是审计韶光比较长，比如说像Mythril，均匀在60秒，Oyente大概在30秒，而Securify大概在20秒。