最近，“刷屏”的区块链成为炙手可热的技术，但这个人人皆知但技术却并没有想象中那么安全，甚至当系统存在漏洞时，只能眼睁睁看着被攻击。而成都这家公司研发的全球首个“一键式”智能合约自动形式化验证工具，可一键查验代码漏洞，其检测准确率超过来97%。

成都链安

全球首个“一键式”自动形式化验证工具在成都诞生

今年9月，链财经发布数据显示，2011-2019年累计安全损失高达80多亿美元，仅2019年1-8月份，由区块链安全事件引起的损失便高达33亿美元。

区块链安全事件爆发率逐年增高，案值也不断增大。如今，国家已经将区块链列为重点发展的技术之一，未来区块链技术将有可能应用于供应链金融，政务系统，司法系统，物联网等领域，区块链系统的安全问题也将更加突出，区块链安全更应给予足够的重视。

“我们要看到区块链发展的机遇，同样也要重视区块链的安全问题。”杨霞作为一名已经在安全行业干了18年的专业人士，她对于区块链的安全更为关注。

杨霞

2016年，区块链上出现首个智能合约安全漏洞，导致5200万美元的损失。该事件触动了杨霞，杨霞敏锐的感觉到，智能合约安全问题不解决未来将严重影响区块链技术的发展，她同样也在这之中嗅到来商机，“当时全球都没有多少企业在做区块链安全。”

随后杨霞开始投入到区块链安全的研究中。“因为任何一个区块链应用程序都将包含多个智能合约程序。于是，我开始尝试将擅长的形式化验证技术解决智能合约的安全。”杨霞说，通过2年多的努力，最终在2018年6月，全球首个“一键式”智能合约自动形式化验证工具在成都诞生。

形式化验证就是将每一种可能都“例举”

2018年3月，杨霞作为创始人，在成都注册了一家专门从事区块链安全的企业-成都链安科技有限公司。

公司在成立后不久，便推出了全球第一款针对区块链的安全检测工具Beosin-VaaS。据了解，Beosin-VaaS是全球首个同时支持微众BCOS、ETH、EOS、Fabric、ONT等多个链平台的“一键式”智能合约自动形式化验证工具，该验证工具首次实现了面向智能合约的自动代码安全检测，可精确定位风险代码位置并给出修改建议，检测准确率超过97%，全球已有2万多开发者使用了VaaS平台。

Vass操作界面

“这个检测工具与我之前从事安全行业有很大关系，它就是基于形式化验证技术研发出来的。”杨霞从面向航空航天领域的安全关键系统的安全到如今区块链安全，在她看来并没有本质区别，只不过区块链的安全面临的挑战更大，形态更复杂，但其根本都是为系统做好安全防护工作。提高系统自身安全能力，建立完善的安全防御体系，是她最擅长的。

什么是形式化验证技术呢？

“简单来说，就是将各种可能出现的问题进行穷举。”据杨霞介绍，形式化验证技术产生于上世纪七八十年代，它主要针对测试不能穷举的情况，运用数学的手段证明代码的安全性和功能正确性。

“传统检测手段，无法把可能出现的情况一一列举进行测试，而形式化验证它是可以穷举的，它通过数学的手段，对代码建立数学模型，并证明是否存在任一可能的安全问题，最终尽可能让区块链系统的代码没有漏洞，以预防被黑客攻击。”杨霞说，这种技术虽然已经存在几十年，已经广泛应用于航空、航天、军事等安全关键领域。但就像人工智能一样，面对新的应用领域，它仍有很大的发展空间。

区块链安全风险贯穿始终

专家：区块链不是万能的，不必为了用而用
文章转载自腾讯网