区块链女侠杨霞：为区块链代码提供军事级的安全检测丨蚂蚁区块链大赛成都站火热报名

智能合约允许在没有第三方的情况下进行可信交易，这些交易可追踪且不可逆转。那么智能合约程序存在哪些安全问题？出了安全问题，怎么办？如何用形式化验证的方法给智能合约程序提供（军事级）的安全验证，提高智能合约代码的安全性？

5月30日晚间，蚂蚁区块链创新大赛安全合作伙伴、有着区块链安全领域“女侠”称号的成都链安科技创始人兼CEO杨霞，在大赛直播群中就以上问题分享了解决方案，同时也分享了如何与蚂蚁区块链BaaS平台共建安全生态。

数据显示，2011年至2018年发生的安全事件造成的资金损失高达42亿美元，其中由于智能合约安全事件造成的损失占据1/3，由此可以看出智能合约安全问题的严重性。而随着区块链落地应用的大量爆发，潜在的安全问题更是不容忽视。

以以太坊为例，智能合约安全漏洞就有数十大类，30多小类。

智能合约的初衷是建立人与人之间的信任基础，如果自身的安全性和功能的正确性得不到保障，这个程序就很难值得信任。如何有效解决智能合约的安全问题，是行业值得深入探讨的。

作为一家专门从事区块链安全的公司，成都链安科技采用形式化验证的方法对智能合约安全进行一键式安全检测。

形式化验证，是根据某个或某些形式规范或属性，使用数学的方法证明其正确或非正确。它是一个系统化的过程，将使用数学推理来验证设计意图（用户功能需求）在实现（智能合约）中是否得以正确贯彻。

此前，形式化验证通常被用于对航空、航天、军事控制系统的关键程序的功能正确性和安全性验证，以确保系统可以通过极其苛刻的安全级别认证。由于区块链系统涉及大量的资金交易，采用形式化验证技术为区块链系统的代码提供“军事级”的安全检测就显得至关重要了。

在对代码安全性检测方面，与形式化验证对立的是“测试”。

测试的弊端是没办法穷举，只能显示已经存在的bug，但永远不能证明bug一定不存在。形式化验证是通过数学推理的证明方法，能够保证一定不存在指定属性的安全问题，并且能够证明程序是否正确地满足功能需求和设计目标。

形式化验证通常分三个步骤：

第一步，对系统功能需求和设计建立形式化的规范； 第二步，对代码实现进行形式化的建模，包括对系统的状态进行形式化的描述，还有每个函数的功能要进行描述，并且给出每一个功能所需要满足的前后的条件； 第三步，通过定理辅助证明器，证明代码实现是否正确满足形式化规范，以此证明功能是否符合预期。

但实际上，这里边有大量的人工参与，效率是非常低的，同时成本也是非常高的。

据杨霞透露，此前她在给军事领域做形式化验证的时候是按照代码行数收费的，在给区块链系统做形式化验证的时候，刚开始用的是人工手段，验证一个600-700行的智能合约就花了一周左右的时间。

显然，这样做根本无法实现工程化的需要。为此，成都链安科技经过近两年的潜心研发，推出了自动形式化验证平台VaaS，能够把代码自动进行建模，自动推理证明。

VaaS在验证智能合约的时候，分两部分，一部分是安全属性验证，一部分是功能正确性验证。

对安全属性验证，首先把智能合约代码自动化进行建模，然后对常规智能合约的安全漏洞建立模型。

对功能正确性验证，必需要人工参与，目前业界还达不到脱离人工参与的水平。VaaS在对工程正确性验证的部分，先对用户的代码和功能的描述进行抽象，自动化建模。之后再通过形式化验证专家进行前置条件后置条件的定义，然后用辅助证明器去证明。

有了这两个基础之后，就能够实现一键式的自动化形式化验证。

据杨霞介绍，VaaS是目前国际上最领先的形式化验证产品，可以支持以太坊、Fabric、BCOS、蚂蚁BaaS等多个区块链平台，精确率可以达到95%以上。而且可以一键式自动化精确定位出代码的漏洞以及所在位置。

此外，成都链安科技还推出了鹰眼安全态势感知系统（Beosin Eagle Eye），采用大数据、人工智能的方法，为区块链上的数据和资产提供安全实时预警和监控，保护用户的资产安全。 另外推出了智能合约开发平台（Beosin IDE），为区块链平台定制化智能合约的开发环境。

可以看出，成都链安科技从区块链开发、安全检测到运行时的安全监控，构筑了一体化的完整防护体系。

凭借在区块链安全领域过硬的技术实力，成都链安科技赢得了大厂的青睐，蚂蚁区块链的专家禁不住盛赞：

“可以毫不夸张的说，你们的安全产品的确是全球范围内最好的！”

成都链安科技也顺利成为蚂蚁区块链创新大赛的安全合作伙伴，为蚂蚁BaaS平台定制智能合约自动化形式验证的平台，可以一键式检测常规安全问题，为蚂蚁BaaS平台的区块链应用程序提供深度的安全审计和服务。

据杨霞透露，这个新的平台预计会在6月份开发出来，并且入驻蚂蚁BaaS平台。

同时，在6月6日，成都链安科技参与协办蚂蚁区块链创新大赛成都站Road Show（报名链接：活动报名链接：https://www.huodongxing.com/event/3494458774400），欢迎各界对区块链感兴趣的朋友使用蚂蚁BaaS平台进行区块链的应用开发，可以扫描下面的二维码进群交流。

（钉钉扫码进入大赛群）