成都链安科技CEO杨霞：80%的智能合约都存在安全漏洞

（原标题：成都链安科技CEO杨霞：80%的智能合约都存在安全漏洞）

腾讯安全日前发布的报告显示，与加密数字货币有关的黑客攻击事件，从 2013年到2018年上半年增加了约五倍，全年预计增加10倍左右。其中，仅今年上半年，黑客对加密数字货币的攻击，就已经造成了20亿美元的直接损失。

基于区块链加密数字货币引发的安全问题，来源于区块链自身机制安全、生态安全和使用者安全三个方面。在区块链自身机制安全方面，智能合约的安全性至关重要。

据链安方面的数据显示，2011年至2018年，由智能合约安全事件导致的经济损失达12.4亿美元。目前，由智能合约安全事件导致的经济损失已经超越交易所，位列第一。

智能合约作为执行合约条款的计算机交易协议，对所有用户都开放，导致了内部存在的安全漏洞也随之公开暴露在黑客面前。

而且，智能合约一旦上传即公开且不可更改，因此现在的区块链项目，对于安全性的需求更加迫切。因此，在智能合约正式开始运行之前进行安全审计就显得尤为重要。

链安科技创始人兼CEO杨霞表示，从目前研究来看，80%的智能合约都存在安全漏洞。在合约开发前、开发过程中和编写完成后，整个项目周期都要保证智能合约的安全性。

在合约开发前，开发者应进行智能合约相关漏洞风险知识学习，了解最新的智能合约安全漏洞，避免开发的合约中存在安全隐患。

在开发过程中，Remix-IDE、truffle等编译工具会对合约中不符合最新规范的代码提出告警，开发者需要对告警引起重视，强烈建议开发者更改自己的代码，以消除编译过程中的告警。

在合约编写完成后，需要对合约功能的完整性和安全性进行测试，确保合约逻辑实现与设计相符，确保无安全风险；最后，可以寻找专业的智能合约审计团队进行合约审计，最大程度地减少安全隐患。

01 智能合约形式化验证应用状况

2016年9月1日，万向区块链实验室肖风在为《区块链革新》作序时曾写道：“The Dao”事件提醒我们，应该有一个能对智能合约进行事先检验的科学方法，但这方面最先进的技术如形式化验证，目前还处于理论研究阶段。”可是如今形式化验证已经被正式用于智能合约的检验中了，这就是技术的进步。

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

据了解，一般来讲，方法有两种：

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

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

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

目前，主要从事智能合约形式化认证的区块链安全公司主要有7家，分别是成都链安科技、Imandra、Certik、The Matrix、Securify.ch、Runtime Verification和Tezos。其中，从事VaaS形式化验证平台研发的有四家，分别是：成都链安科技、Certik、Securify.ch和Runtime Verification。

其中，链安的特色在于：提供多个区块链平台验证工具，而不是单一地为以太坊或者EOS提供智能合约形式化验证。

杨霞是2016年才开始接触区块链的，正赶上了著名的以太坊The Dao事件，在此之前，杨霞老师一直专注于为航空航天、军事领域提供形式化验证服务。

“其实那个时候真的没有太在意。不过我有一个朋友在搞区块链，他跟我说你搞形式化验证，能不能去验证一下智能合约的安全，比如针对Dao系统的安全事件。”杨霞回忆道，“我觉得挺有趣的就去试了一下。那时候我们还没有自动化的工具，只能靠人工进行代码的形式化描述，然后去证明。最后发现，形式化验证方法应用于智能合约安全审计效果不错。”

也许当时选择将形式化验证应用于区块链智能合约的审计是一个偶然的机遇，但是，通过杨霞和她的团队经过一年半左右的潜心研究研发出了自动化的智能合约安全验证平台VaaS。

目前，链安的VaaS平台支持EOS和以太坊的智能合约的安全审计，VaaS也是全球第一个支持EOS的智能合约验证平台。

02 形式化方法像一套完备的法律

被问到如何向技术小白解释形式化认证，杨霞表示“形式化方法就像一套完备的法律，规定了每个角色能做什么和不能做什么，并对角色之间的关系进行界定。类似于社会系统架构对不同角色进行分类，在承认个体天性的同时，使系统的复杂程度降低了多个维度。”

形式化验证通过数学建模的方式，对合约进行验证，发现合约的未知的潜在的风险。

因为是用数学证明的方式去发现问题，所以首先需要一个函数的详细功能规范，形式化验证就依据这个功能规范去证明实际的代码是不是和需求一致，如果是函数的规范足够完整并且能够清楚无歧义的表达，那么是可以发现针对这个被验证的函数之前没有发现的问题。

形式化的抽象可以从复杂的事物中抽离出本质。举个简单的例子，一个构造复杂的中式凉亭，经过形式化的方法抽象过后，可能只是一个分层的三角形，这就相当于一个精简的解读。

在验证安全之后，通过使用可执行模型，将较高级别的抽象模型转换为较低级别的代码。形式化方法使智能合约的生成和执行有了规范性约束，保证了合约的可信性，使智能合约的生产过程和执行效果得到了保障。

据杨霞表示，目前，理论上讲，形式化认证可以找出所有已知的和未知的智能合约安全漏洞。而实际操作中，形式化工具可以查出80%的常规漏洞，对于部分结合业务逻辑的漏洞，还需要人工复核。

03 智能合约小白级漏洞居多

区块链行业的安全漏洞是不断涌现的，尤其是涉及到“钱”的安全漏洞，可以使人们的数字资产瞬时归零。目前，随着漏洞不断被挖出，很多数字资产投资者也陷入到了恐慌之中。

杨霞老师表示，就智能合约来讲，80%都存在安全问题。

就目前看来，智能合约中还是小白级的错误居多，包括一些造成巨额财产损失的漏洞。

举个例子，2018年4 月 22 日 13 时左右BEC智能合约被爆出的整数溢出漏洞，黑客能无限印币，在一次交易中，也就那么几秒钟的事情，黑客就“无中生有”地给两个账户转了天文数字般的BEC币，而原账户一分BEC币都没损失。一行代码就造成了60多亿人民币的损失。

整数溢出就像是水轮车。往里面加水，加满之后，继续加水，水轮车将会失衡并转动，此时水将会被全部倒出来，并重新盛水。当变量累加到超过自身容量范围时，将会溢出，归零。而黑客也是利用了这一点，把运算前的数值作为转账金额，把运算后溢出的0作为检测条件，从而实现绕过。

这是一个很简单的逻辑，但是后果却很严重。

同样，之前爆出来的以太坊平台的漏洞，短地址攻击，以及拒绝服务攻击等等的漏洞的逻辑也都很简单，但是这些漏洞都造成了人们数字资产的巨大损失。

其实，这些漏洞在智能合约正式开始运行之前，都是可以通过形式化验证的方式找出来的，并加以修复的。

链安采用数学的证明方式将代码形式化描述为公式，并对其进行逻辑漏洞和安全漏洞证明，基于此原理，实现了自动化的验证工具，能够方便、快速地验证出代码的功能正确性和安全属性。

杨霞老师表示，目前，成都链安科技的优势集中体现在三个方面：

第一，我们专注只做智能合约的安全。

第二，我们在技术上有优势，我们采用了严格的形式化验证的方法，为智能合约提供更加完备的安全审计。

第三，我们率先研发了自动化的智能合约安全验证工具VaaS，在智能合约的审计过程中，我们通过自动化工具VaaS和人工结合的方法比全人工的安全审计方式更准确、更高效。

对于未来区块链安全的走向，杨霞老师表示，安全是一个持续完善的过程，没有绝对的安全，越是复杂的软件系统，出现安全事件的概率越高。

为了避免安全事件的发生，最好的办法就是提高软件开发人员的安全意识，并对智能合约在部署之前进行全面的安全审计。

我们要理智地看待区块链技术的漏洞，区块链作为一个新兴技术，出现安全事件是可以理解的，不能因噎废食。