智能合约安全之形式化验证研究报告|ONE.TOP评级

随着平台级应用的普遍化，智能合约涉及的金额呈指数级别增长，智能合约的安全问题也成为投资者和开发者共同关注的焦点。今年以来有数个基于ERC-20的ICO项目因为智能合约代码出现漏洞而遭到黑客攻击，导致投资者巨额的损失。为了防止类似事件的发生，交易所、钱包、项目方等都在智能合约安全上加大投入，同时围绕着智能合约安全的周边生态成为目前投资的热点。

——————————————————

作者：

ONE.TOP  洪妙丛

节点研究中心  蔡晨曦 武怡 郎瀚威

支持机构（排名不分先后）

金塔行情、星球日报、金色财经、babi财经、节点财经

（本报告由ONE.TOPX节点研究中心联合发布）

智能合约安全方面的措施总体来说分为以上几个大类，合约开发模板、合约审计、智能合约语言设计和赏金猎人机制。

1）合约开发模板如OpenZeppelin、Etherparty等为标准化的合约提供经过多次实战验证的标准化模板，在节约时间同时保证合约安全性。

2）合约审计的方法又分为人工审计和机器辅助审计

3）机器辅助审计又分为规则验证、语义验证和形式化验证，而形式化验证是本文关注的重点。

引用自consensys 唐奕 《公链安全》

智能合约语言设计中，许多公链平台开始采用Haskell或OCaml一类的函数式语言，因为函数式语言更为便于编写形式化验证方面的开发者库和工具。赏金猎人机制，相对于前几项措施，更多是部署合约后发现漏洞的弥补机制。

形式化验证指的是用数学中的形式化方法对算法的性质进行证明或证伪。方法有两种：

一种是模型检验，即把系统所有可能的状态列出并进行一一检验，此种方法全自动化但只适合小型系统；

另一种是演绎验证，首先把系统代码标记成抽象数学模型，然后对定理进行证明，此种方法适合大型系统，但是需要首先人工将系统的运作方法转换成验证系统可以理解的语言。

目前为止，形式化验证主要应用在军工、航天等对系统安全非常高的领域，在消费级软件领域几乎没有应用。由于传统互联网应用与区块链应用的运行环境有着本质的不同，其开发流程也应当相应地进行调整，其中最关键点在于安全验证环节的投入比例。

在传统互联网应用中，由于普遍采用中心化服务器+客户端的模型，如果应用出现安全隐患只需要对服务器端代码进行修改就可以轻松排雷，并且服务器端可以对用户数据进行回滚以挽回用户损失。因此，传统互联网应用开发的过程较为注重快速迭代，以牺牲安全性换取效率和功能上的快速升级。

在区块链应用中，由于区块链的不可篡改性，智能合约一旦上线并出现安全隐患，对用户造成的损失是巨大且不可挽回的。一旦出现黑客事件，需要整个社区的共识才能回滚交易，所以每次遭受攻击都回滚交易也是不现实的。因此，区块链应用开发的过程需要用大量的测试和检验以获取足够的安全性，而反过来牺牲迭代的速度。

由于区块链开发人员的稀缺，远远无法赶上智能合约数量的增长，人工审计智能合约是成本非常高昂的，因此机器辅助验证是目前的必然趋势。规则、语义验证的实现，相对较为容易，技术门槛也较低，但是只能进行一些浅层的纠错，不能深入程式的逻辑。因此，只有形式化验证方法有希望真正提高智能合约审计的自动化程度。

目前区块链产业中与形式化验证相关的产品可以分为三类: Vaas平台，公链，和语言。

3.1 Vaas平台

Vaas平台是直接面向开发者提供形式化验证服务的平台。目前Vaas类项目包括CertiKzecurify.ch、Runtime Verification等项目。目前，CertiK仍在募资阶段，链安科技据称已经有研发成功及获得专利的产品，Securify.ch的测试版已经上线，而Runtime Verification已经在商业运营。

与其它几个项目不同，RuntimeVerification是基于EVM虚拟机二进制码进行形式化验证，而非针对智能合约本身用的高级语言，因此在安全性上又更进一步，避免了因编译器编译过程中可能产生的漏洞。

3.2 语言

语言类产品一般为函数式语言的子语言，提供与智能合约形式化验证相关的开发者库和工具，目前有Imandra和Tezos等项目。

其中，Imandra发布了一套开源的以太坊虚拟机用ImandraML语言标记的模型，并且专注于交易所等金融应用场景的形式化验证，用以确保金融交易的合法合规，据称相关技术已经用于华尔街顶级投行的交易系统。

3.3 公链

直接包含形式化验证引擎的公链产品目前只有The Matrix项目，特征是基于AI辅助的形式化验证及动态约束的检查。AI是否对于形式化验证的自动化带来帮助在技术上仍是个未知数，因此这个项目也将成为这个领域的试金石。

5.1 Certik

 Certik是一个是形式化验证框架，经过certik验证的智能合同、DApp以及区块链将会被附上证书形式的标志，来展示其正确性和安全性。Certik平台提供的主要功能包括以下部分。 

智能标签框架

CertiK平台应用深度学习技术来构建智能标签框架，有了这个框架，大多数共享逻辑和属性代码（前置条件，后置条件，不变量等）都可以被自动标记，从而使得程序的逻辑，语义更加清晰和规范，这样验证的工作量就可以大大减少。

基于层的分解

这种技术揭示了分层设计模式的见解，并使得将复杂的证明任务分解为更小的任务成为可能，并在适当的抽象层面验证它们中的每一个。

可插拔的验证引擎

提供开放式的协议，更先进算法的证明引擎可以自由插入这个系统。

机器可检验的证明对象

构建机械式的证明对象（或者反例），这些证明对象可以快速的被任何人检验，同时作为验证程序的证书（机械式证明对象可直接作为证书，赏金猎人提供的证明对象，需要检察官进行人工检验后才能作为证书。注：赏金猎人和检察官后文会进行描述。）

认证的DAPP库

为集成开发环境提供了一系列认证库和插件，以便开发出质量更高的dapp，但是会花费一些CTK。

定制化的认证服务

如果有高可靠性要求，可以提供定制化的认证服务，由验证领域的专家提供帮助并出具综合报告。

Certik平台围绕bug的检测和修复建立了一个去中心化的生态，该生态由五个角色构成，分别是客户、赏金猎人、检查官、社区贡献者以及开发使用者，该生态工运行模式如下图所示。

该系统可以分为机械化部分和人工部分。客户在certik平台上提交dapp或者程序系统，平台自动为其添加智能标签，并自动进行分解，形成小模块的证明任务，这个环节客户需要消耗一定量的CTK。

分解完小模块后，系统由两种方式进行验证，简单的证明任务可以由一些自动验证器(例如SMT解算器)解决。除了平台内部自带的验证器（证明引擎），CertiK平台提供开放协议，社区贡献者可以将带有更高级的求解算法的证明引擎自由地插入到该系统中，并获得一些CTK奖励。赏金猎人可以随机使用他们的引擎，并进行评估，优秀的引擎将被社区研究和推广。

另一种验证方式针对较为复杂的证明任务。赏金猎人接到该任务后，构建一个证明对象并进行广播，接着检查官对证明对象进行检测，当证明对象验证通过后，会被贴上证书的标签，赏金猎人和检查官分别获得CTK奖励。

所有分解的证明任务被验证后，CertiK平台的后端将返回详细而全面的评估报告。

开发使用者可以使用所有CertiK平台的认证库和IDE插件， 构建自己的DApp /系统，这需要花费一定的CTK。

以下是certik的操作界面

检测完毕后，CertiK 会提供这份智能合约的安全系数，并告诉你哪一块程序存在着错误，并提供详细的解决方案

5.2 链安科技

提供几种验证服务：

•   第一个，安全审计

•   第二个，开发、审计一条龙

•   第三个，合约开发

其中安全审计模块针对的漏洞包括代码编程规范漏洞、代码逻辑漏洞、函数调用漏洞、整型溢出漏洞、可重入攻击漏洞、执行顺序依赖漏洞、时间戳依赖漏洞、平台接口误用漏洞。

链安CEO通过一个例子从数学原理上对形式化验证进行了描述说明。以近期频发的溢出类安全漏洞属性检查为例，如检查代码

int8 c=a+b

是否存在溢出漏洞，下面展示对这行代码的功能正确性和安全属性的证明过程。

首先，对整数类型建模，定义形式化规则：

Int8.repr: Z -> int8

该规则通过截取纯数学整数（取值范围从无穷小到无穷大）的低8位数值得到一个8位长度的机器整数。然后写加法运算的形式化规范，如下：

{a:int8,b:int8} // 

设置代码执行的前提条件，保证a和b的类型是8位有符号机器整数;

{c = a + b;} // 

加法运算的源码程序；

{(int8.repr(a+b)) /\ ((Int8.repr (a+b)) = (a+b))} ; // 

设置代码正确执行的后置条件。

其中，(int8.repr(a+b))描述，是为了证明代码的功能正确性是否满足，即需要证明源代码是对a和b进行求和而不是求差或任何其他运算逻辑，并且将运算结果转换为int8类型。此外，需要对是否溢出的安全属性进行证明，因此添加后置条件：

((Int8.repr (a+b)) = (a+b))

因为一旦

a+b>int8.max_singed 

或

a+b

都将导致

(Int8.repr (a+b)) ≠ (a+b)

最后，根据前置条件证明代码的执行是否满足上述后置条件。如果产生一个不可证明结果，说明程序功能不正确，或者存在溢出安全漏洞。然后根据证明结果，对源程序进行分析修改，然后再重新证明，直到证明通过为止。链安采用这种数学的证明方式将代码形式化描述为公式，并对其进行逻辑漏洞和安全漏洞证明，基于此原理，实现了自动化的验证工具，能够方便、快速地验证出代码的功能正确性和安全属性。

5.3 runtime verification

RuntimeVerification Inc.是一家初创公司，通过使用自己研发的runtime验证技术致力于提高汽车，飞机，航天器和区块链领域的软件系统的安全性，可靠性和正确性。从2001年开始，runtime verification就成为NASA的研究科学家。

Runtime验证技术依赖于程序执行不应违反某些属性的原理。其中一些属性，如并发程序中缺少数据竞争，具有通用性，可以自动检查。 其他属性，如专用库的规格，是针对特定应用程序或用途定制的。Runtime验证技术可以自动检查通用属性，不需要开发输入，并且可以检查开发人员用形式化方式表达的任何定制属性。

在区块链方面，runtime公司主要对智能合约进行形式化验证工作，验证步骤包括：

（1）形式化

根据智能合约所有者提供的非形式化规则，对智能合约的高级业务逻辑进行形式化。

（2）确认

形式化后的高级业务逻辑需要由智能合约的所有者确认，可能需要经过多轮讨论和修改，才能确保它能正确捕捉合同的预期行为。

（3）提炼

通过多个步骤将形式化后的规则完善到虚拟机级别，以捕获虚拟机特定的细节。最终的虚拟机级别规则的作用是确保在字节码级别没有意外发生，也就是说，只有在执行字节码时才会发生高级规则中指定的内容。

（4）编译和测试

使用与部署合同相同的编译器版本，将智能合约从其高级代码编译为生成的虚拟机低级代码。

（5）验证

最后，对智能合约的虚拟机字节码与虚拟机的规则进行形式化验证，通过这样的方式不用依赖编译器的正确性。同时，runtime使用自己研发的K-framework结构演绎验证程序， 以达到严格推理虚拟机字节码而不遗漏任何虚拟机怪癖的效果。

6.1The DAO

2016年6月17日，一名黑客在编码上发现了漏洞，使得他可以从The Dao上抽走资金。在攻击的头几个小时，360万的以太被转出，在当时价值相当于七千万美元，今天则达到了21亿美元。黑客达成了他想要的破坏，退出了攻击。

在此漏洞中，攻击者能够“请求”智能合同( DAO )多次返回以太，且都是在智能合约更新它的余额前进行的。两个主要问题使它成为可能：一是在创建DAO智能合约时，编码人员没有考虑到递归调用的可能性；二是智能合约首先发送ETH资金，然后再更新内部token余额。

重要的是要了解这个bug不是来自以太坊本身，而是来自基于以太坊上的构建应用程序。为DAO编写的代码有多个缺陷，递归调用的漏洞就是其中之一。

另外一种理解它的方式是比较。以太坊比作是互联网，基于以太坊的应用比作是网站。也就是说，如果网站不运行，不意味着整个互联网出问题。它只能说明网站有问题。

黑客出于未知的原因停止从TheDAO抽取资金，尽管他可以继续这么做。以太坊社区和团队很快就控制了局面，并提出了多项应对攻击的建议。

然而，这些资金被存入一个账户，有一个28天锁定期，黑客无法转走。为了退还损失的钱，以太坊通过硬分叉把被黑资金退还到原所有者的账户上。退还汇率是1 ETH兑100 DAO ，与首次公开发行时的汇率相同。

毫无意外，黑客攻击意味着DAO的终结。很多以太坊用户质疑硬分叉违反区块链的基本信条。更糟糕的是，2016年9月5日，Poloniex交易所下架了DAO token，Kraken在2016年12月也下架了DAO token。

与美国证券交易委员会(SEC)2017年7月25日发布的报告相比，以上的这些问题都相形见绌。它提到：

“由一个名为“DAO”的“虚拟”组织提供和出售的代币是证券，因此受联邦证券法的约束。报告确认，发行基于区块链技术的证券发行者必须登记此类证券的发行和销售，除非有有效的豁免。参与未注册发行的证券的人也可能要对违反证券法的行为负责。”

换句话说，TheDAO的发行与首次公开发行(IPO)一样，受到同样监管原则的约束。按照SEC观点，DAO违反了联邦证券法，所有投资者也一样。

6.2 EDU

区块链项目EDU智能合约中存在漏洞。在一个名为transferFrom 函数中，缺少 Safemath 验证，利用溢出攻击可以让攻击者从任何一个 EDU 余额不为 0 的账号内向另外一个账号转出 任意数量的EDU Token。

由于目前EDU在火币pro上线，黑客利用漏洞累积向火币转入了超过20亿枚EDU。这也导致了EDU的价格崩盘。

7.1 Sentinel Protocol

韩国团队，基于ICON的第二个项目。项目目的是要创建一个去中心化的声誉系统，通过集体智能和人工智能相结合，将所有数字货币的粘片，黑客信息，可疑钱包地址等各种信息记录在区块链上。

7.2 Atonomi

要成为世界上第一个分布式物联网安全协议。

Atonomi利用区块链上的特性与经济激励，利用Token注册和验证评估系统，构建出一个物联网设备的认证与信誉数据库，保证每一台加入网络的设备，都拥有良好的信誉。同时，应用母公司Centri的技术（Centri是传统互联网的安全公司，拥有多项安全方面的技术专利，并与很多互联网大公司是合作伙伴）给设备加密，确保数据隐私并阻止它被黑客利用来连接到别的物联网设备。同时Atonomi的Token也像IOTA一样支持设备之间的微支付需要。

7.3 Gladius

严格意义来讲，Gladius并不是一个保护区块链的项目，而是一个利用区块链技术，来保护传统互联网的项目。

Gladius是利用存储和流量的经济激励，来创建基于区块链的分布式CDN，从而实现DDoS攻击的分散保护，同时创建一个大型流量池，处理不断出现的DDOS请求，提供比传统DDOS防护更加经济和高效的方式。

Gladius的桌面客户端允许用户租用计算机空余的带宽，并为提供者奖励代币，代币可以购买区块链服务，也可以用于开发，有点变向挖矿的意思。

7.4 Quantstamp

正如一家公司的财务报表需要审计一样，智能合约，同样需要审计，有了审计，这些类似漏洞发生的概率，可以被大幅度降低。

简单说来，Quantstamp就是这样一个区块链智能合约的审计类项目，让智能合约变得更加安全。当然了，和像四大会计事务这样的中心化组织不一样，咱们是去中心化的。

7.5 POLYSWARM

Polyswarm 第一个去中心化的杀毒软件市场

去中心化正是区块链的看家本领，Polyswarm是世界上第一个尝试用区块链来改变这个市场的。他们设计的系统里有4种角色。

用户（EndUsers）报告可能染毒的文件信息，并在平台上悬赏，得到及时而准确的安全信息。

安全专家（Experts）通过分析病毒信息来决定这是否是一个病毒来赚取奖励。

    由于智能合约形式化验证目前尚处于起步阶段，目前项目大多还没有落地。展望相关行业需求，相关的投资逻辑如下。

8.1 金融领域细分首先落地

目前为止，造成严重后果的漏洞大多来自钱包、ICO募资等金融领域应用的合约，而这类合约逻辑较为标准化，相对较容易用形式化验证的方式进行查验。因此，专注于金融领域的形式化验证产品更有潜力。

8.2 函数式语言长期来看是趋势

许多新的公链项目，如Aeternity、Tezos等都采取了函数式语言作为智能合约的编程语言，目的在于方便形式化验证工具的开发。因此，在选择公链项目上，函数式语言是首选。

本文章不代表火讯财经立场。