破解智能合约可靠性隐忧，全球首个“携带交互式形式化证明”的智能合约库发布

智能合约库提供更加可信可靠的安全保障手段，让数字货币智能合约不再漏洞频出，显著改善数字货币智能合约安全形势。

2018年7月7日，在深圳2018数字经济高峰论坛上，安比（SECBIT）实验室联合 ConsenSys中国发布了全球首个携带交互式形式化证明的智能合约库，为目前漏洞频出的数字货币智能合约开发工作提供更加可信可靠的安全保障手段，显著改善数字货币智能合约安全形势。

安比（SECBIT）实验室此次发布的智能合约库借助交互式定理证明工具 COQ，提供了对 ERC20 智能合约中的一些高阶逻辑特性的形式化证明。经过证明的 ERC20合约具有以下特性：不存在溢出漏洞、其账户余额总量满足和totalSupply一致、Token中的总量不变、合约转账无法影响非相关账户余额等。

“目前数字货币的智能合约存在大量问题，而业内缺乏大家认可并且可靠的保证。智能合约的形式化证明将弥补这一缺失，缓解智能合约开发者和数字货币投资者对安全的担忧，加强各方对数字货币的信心。”安比（SECBIT）实验室创始人郭宇博士说。

创立安比（SECBIT）实验室之前，郭宇曾在中国科技大学教学计算机科学多年，常年从事关键系统的代码形式化证明理论研究工作。郭宇表示，形式化证明大多数人可能并不熟知，简单来讲，形式化证明就是通过数理逻辑证明的方式，证明代码的实现在规范描述的前提下满足某些特性。

“就像数学中的定理一样，一旦证明出来，结论就是毋庸置疑的。”郭宇说。“形式化证明用于智能合约可以达到同样的效果。”郭宇介绍说，形式化证明是形式化验证技术的一种，形式化验证技术门槛通常比较高，成本投入大，目前也只是在芯片设计、航空航天、火箭、核电、高铁等对安全要求极高的领域，才会用到形式化验证理论技术。

随着区块链和数字货币行业迅猛发展，一个智能合约的背后动辄涉及数亿美元的数字资产，而一个智能合约的微小漏洞，就可能让投资者的资产蒙受巨大损失。正因为此，智能合约迫切需要引入更可信、更可靠的机制来确保智能合约的安全可靠性问题，而形式化证明再适合不过。

尽管形式化验证是保证智能合约安全极其有效的手段，但目前相关的研究还比较匮乏，也缺少相应的工具支撑。安比实验室发布的 ERC20 合约的形式化证明，一方面希望能够为大家筛选出一份安全的合约模板；另一方面也希望能够借此让更多的人了解并学习形式化验证，共同参与到智能合约的形式化验证领域中来。

这次安比（SECBIT）实验室发布的携带形式化证明的智能合约安全库，可以分为三个部分：ERC20智能合约源码、形式化合约规范的定义以及合约满足规范的证明、高层性质的定义以及合约满足高层性质的证明。

本次发布的形式化证明代码地址：
https://github.com/sec-bit/tokenlibs-with-proofs

其中，

合约源码：即被证明的合约代码；

（合约源码来源于ConsenSys官方Github仓库：https://github.com/ConsenSys/Tokens/blob/master/contracts/eip20）

合约规范：定义了每个合约函数的预期行为；

合约满足规范的证明：证明了合约的每个函数的确实现了规范中定义的行为；

高层性质：定义了合约的各个函数作为一个整体，在接受任意的外部调用序列是，仍然能够满足的性质；

高层性质证明：证明了合约的确能够满足上述的高层性质。

本次发布的智能合约完成了以下特性的证明：

transfer()和 transferFrom()操作不存在溢出漏洞

在合约中，任意执行完成一步后，合约中 totalSupply 的值与所有账户的余额的总和相等

合约执行完成 transfer()转账操作以后，token 总量不变

合约初始化完成后，token 总量不变

合约执行完成 transferFrom() 转账操作以后，token 总量不变

转账操作后，合约中仅余额转出和转入的账户发生改变，其它账户不变

郭宇表示，有了以上的证明，形式化验证可以在一定的边界条件内，保证代码的绝对安全可信，根本上杜绝了某一类漏洞问题。

目前，安比（SECBIT）实验室发布的只是ERC20 token 合约及对应的一些简单性质，初步展示了形式化验证如何应用在智能合约领域。随着智能合约的应用范围的扩大，业务逻辑复杂度进一步增加，智能合约将涉及到更深层次的经济学博弈论问题，借助形式化证明背后完备的数学理论和哲学思想，形式化证明必将给区块链技术社区带来更多的惊喜。

尽管形式化证明是保证智能合约安全极其有效的手段，但目前国内这一领域专业人才较少，相关的研究还比较匮乏，也缺少相应的工具支撑。安比（SECBIT）实验室成员依托形式化验证领域十余年的研究经验，致力于把该项技术更广泛应用于智能合约安全。

“未来我们可以利用形式化方法去证明智能合约更多的通用性质，规避常见漏洞和风险，如整数溢出，token 总量不变等。”郭宇说，还可以逐步使用形式化的方法去证明一些智能合约的高层性质，如复杂的业务逻辑的正确性，博弈论观点上的公平公正性等。

“希望此次智能合约库的发布，可以吸引更多的技术爱好者参与进来，共同为形式化验证和智能合约的发展贡献力量。”郭宇说。

“目前业界不少代码库的安全性都存在难以验证的问题，因此，大量基于这些代码库开发的项目也‘继承’了这些安全隐患，影响巨大。安比实验室通过形式化证明的方式验证了ConsenSys合约代码库的安全性，对推动以太坊和区块链行业发展有深远影响”，ConsenSys中国区负责人唐弈说。