安全专家杨霞：区块链安全如何步入“一键检验”时代？

​文 | 常明星   编辑 | 毕彤彤   来源 | PANews

“条件漏洞、逻辑判断错误、代币授权错误、整型溢出漏洞、拒绝服务攻击等数十个常见漏洞普遍存在于智能合约中。”Beosin（成都链安科技）的一份分析报告写道，目前80%的智能合约存在安全问题。而这些智能合约漏洞带来的最直观的危害就是经济的莫名损失，包括造成代币被盗、多次取款等。

2017年，多签名钱包的智能合约被爆出现了一个极其简单的漏洞，导致钱包被多次洗劫。第一次损失了3000万美元，第二次损失了1.5亿美金。今年四月，曾经高出美图5倍市值的美图关联区块链项目美链的代币BEC也因智能合约漏洞，一夜被盗64亿，市值几近归零。诸如此类的安全问题不胜枚举，区块链行业发展中的技术安全问题日益凸显。

“区块链行业想要真正站起来和走出去，时间和安全缺一不可。”Beosin联合创始人兼CEO杨霞在接受PANews专访时坦言。作为首家将形式化验证技术运用到智能合约代码安全检测中的安全公司，杨霞带领着Beosin团队为区块链的行业安全“保驾护航”。

形式化验证：用数学模型来检验代码 

形式化验证原本是比较小众的验证方式，通常被应用在军事、航空航天等领域，对关键的系统进行安全验证。杨霞表示，形式化验证并非很神秘，归根结底，它也是计算机系统安全防护的一种最严格、有效的方法。

对智能合约进行形式化验证时，首先会将智能合约的代码转换为数学公式，用数学的方式对代码进行形式化的描述，这个过程叫做形式化建模。建模之后，则可灵活地根据客户的需求，撰写数学定理，然后证明代码是否正确的满足用户定义的功能，从而确定智能合约代码是否存在安全隐患，或者是否符合某些功能要求。

杨霞介绍到，Beosin（成都链安科技公司）研发的VaaS自动形式化验证平台，已经将形式化验证的人工参与程度大幅度降低，一般的安全检测能够完全自动化完成，而对于一些非常复杂逻辑的代码，人工参与度也仅有20%左右。“目前对于常见的智能合约安全检测已基本通过VaaS自动化检测平台实现了全自动化，这样做的优势在于，一方面减少了人工操作带来的失误，提高了准确率，另一方面让简单的漏洞检测变得更高效。”她说。

自动化形式化验证的过程是怎样的？杨霞这样描述，只需将要检测的代码导入到VaaS检测工具中，然后点击“开始检测”，链安的VaaS自动化检测工具就会将合约代码中存在的漏洞以及其他问题“一网打尽”。

丢入代码、运行代码再到检测出问题，这种对用户来说及其方便的检测程序，似乎与传统意义上的代码测试并无明显区别。

对此，杨霞表示，传统的代码测试只能检验出代码中已表现出的漏洞，并且误报率非常高；而形式化验证是通过数学的角度证明代码是否存在这些安全漏洞，更加严格和准确，同时借助于部分人工参与还能检测出智能合约代码未表现出来的隐藏安全漏洞。她补充说，形式化验证还通过数学的方法为代码构建了一种检验模型，因此VaaS的安全检测的准确率可达到95%以上。

提到Beosin开发的VaaS智能合约自动形式化验证平台，杨霞认为，Beosin作为国内首家将形式化验证运用到智能合约漏洞检测的公司，其开发的VaaS检测平台凭借高效、精准的性能“技压群雄”。

在Beosin给出的一份VaaS平台与俄罗斯安全团队研发的SmartDec智能合约安全审计工具、瑞士团队研发的Securify以太坊智能合约形式化验证漏洞扫描工具，以及美国Quantstamp团队研发的QSP付费型自动化审计工具的《对比测试报告》中显示，无论是在产品的使用体验，还是在代码检测的准确度（达到95%以上）和速度等方面，Beosin的VaaS平台都比同类产品要成熟和强大的多。

揭秘Beosin：两位教授带队，成员90%为技术

Beosin在形式化验证上的优势，跟其创始阵容有着直接的关系。

创始人杨霞和郭文生分别为电子科技大学的博士后和博士，后留校任教，担任副教授。杨霞刚告诉PANews，她从事形式化验证、内核安全、移动设备安全等技术的研究长达18年。并长期为航空、航天、军事等行业提供形式化验证的服务，还为微软、华为、长虹等公司提供安全解决方案，主持了国家级重大安全类软件课题近10项。郭文生也同样如此，他同样在形式化验证的领域沉浸10多年，发表过相关论文30多篇，申请的专利数也达10多项。

“我和郭教授虽都从事形式化验证领域，但我们两人所研究的路线不同”，杨霞补充说，“其实郭文生教授最开始比较感兴趣的行业是人工智能，但我觉得区块链行业对我们来说，潜力更大，于是我说服他一起创立了成都链安科技有限公司，将我们在形式化验证研究的不同方法合为一体，从而研制出了同时支持ETH、EOS 、Fabric等多个区块链平台的VaaS智能合约自动形式化验证平台。并在短时间内就申请了4项专利”

2018年3月，发起成立链安科技其实是杨霞的第四次创业，作为一名连续创业者，她认为区块链行业在未来的“不可限量”，而且，就现阶段来说，这个行业比其他任何行业都更需要优秀的安全技术。

杨霞及技术团队与V神交流

发展至今，链安已拥有40余人的团队成员，其中90%都是专攻技术，并根据其业务范围，分为面向行业应用的DApp开发组、安全审计组（包括链平台、钱包、dapp、合约等安全审计）和VaaS平台工具开发组等。除此之外，链安科技还与海外的一些资源建立了合作关系，包括美国Idaho大学终身教授，同是从事形式化验证的Jim Alves-Foss和法国形式化验证团队等。

安全之后，看准应用开发落地

谈到Beosin的未来规划，杨霞表示，做技术的公司无论如何都要将研发安全技术产品放在首位。但未来Beosin的安全产品将面向整个区块链生态，而不只是智能合约。

Beosin不仅在技术安全领域有着扎实的功底，其在区块链技术开发方面也同样“功力深厚”。

Beosin目前的业务除了智能合约安全审计、还包括钱包开发和审计、VaaS平台定制化开发、安全的Dapp开发与审计一条龙、安全的智能合约开发审计一条龙、交易所和公链平台安全检测等全生态安全服务。

杨霞称，未来Beosin发展的第一步，就是将其安全产品对应到区块链生态的各个环节，而不止是专攻智能合约的安全检测方面。第二步，就是让区块链技术被更多的企业所应用，做好区块链落地应用的技术支持。

“Beosin会在未来开展一些面对行业技术落地应用的业务。因为Beosin接收到很多传统企业想要接触和应用区块链技术的需求。但是很多企业虽然区块链技术有很大的探索欲，但苦于没有技术雄厚的公司来对接。”杨霞也同样憧憬这她带领的Beosin团队在区块链应用落地方面，能有所作为。