2018年初，日本第二大虚拟货币在线交易所Coincheck遭受到黑客攻击，该案当时被称为“史上最大虚拟货币盗窃案”，据称损失超620亿日元（约合30多亿人民币）！
最近，“刷屏”的区块链成为炙手可热的技术，但这个人人皆知但技术却并没有想象中那么安全，甚至当系统存在漏洞时，只能眼睁睁看着被攻击。而成都这家公司研发的全球首个“一键式”智能合约自动形式化验证工具，可一键查验代码漏洞，其检测准确率超过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操作界面
“这个检测工具与我之前从事安全行业有很大关系，它就是基于形式化验证技术研发出来的。”杨霞从面向航空航天领域的安全关键系统的安全到如今区块链安全，在她看来并没有本质区别，只不过区块链的安全面临的挑战更大，形态更复杂，但其根本都是为系统做好安全防护工作。提高系统自身安全能力，建立完善的安全防御体系，是她最擅长的。
什么是形式化验证技术呢？
“简单来说，就是将各种可能出现的问题进行穷举。”据杨霞介绍，形式化验证技术产生于上世纪七八十年代，它主要针对测试不能穷举的情况，运用数学的手段证明代码的安全性和功能正确性。
“传统检测手段，无法把可能出现的情况一一列举进行测试，而形式化验证它是可以穷举的，它通过数学的手段，对代码建立数学模型，并证明是否存在任一可能的安全问题，最终尽可能让区块链系统的代码没有漏洞，以预防被黑客攻击。”杨霞说，这种技术虽然已经存在几十年，已经广泛应用于航空、航天、军事等安全关键领域。但就像人工智能一样，面对新的应用领域，它仍有很大的发展空间。
区块链安全风险贯穿始终
专家：区块链不是万能的，不必为了用而用
虽然有“一键式”验证技术，但区块链的安全问题仅仅是验证一下代码就可以完成吗？
成都链安办公区
区块链安全风险贯穿始终。如开发时期由于代码本身缺陷带来的各种漏洞会让上线后的系统存在致命的安全隐患。“以全球最知名的以太坊链平台为例，其智能合约代码具有不可更改性，一旦部署将无法修改。如果智能合约代码一旦有漏洞，就只能眼睁睁看着被攻击。”杨霞说，随着区块链应用进入我国国计民生相关的各个领域，而其关键程序智能合约存在漏洞将严重影响系统的运行，甚至导致项目失败，链上资产和数据全部丢失。
在运营阶段，黑客会通过DDoS攻击、漏洞入侵等方式降低交易平台的可用性，窃取账户，资产等。而若智能合约存在漏洞将严重影响整个项目，甚至导致项目失败。在推广时期除了网络攻击，平台还可能遭受薅羊毛等业务欺诈、山寨仿冒等钓鱼欺诈，让企业资产流失、声誉受损。
为此成都链安研发了面向区块链应用的安全态势感知系统，采用大数据和机器学习的方法，对区块链上交易进行安全监控，对安全事件提前预警、并实时报警，同时通过先进的区块链防火墙对安全事件及时阻断，保护系统安全运行和用户资产安全。
“目前，整个区块链行业还处于开发阶段，不确定因素较多，没有必要为了用而用。”作为安全方面的专家，杨霞认为，区块链可以加速人与人之间、人与企业之间、企业与企业之间的信任。在她看来，区块链适用于物流、保险、金融、法院、供应链等行业，并在一定程度上能大大促使这些行业的加速发展，但在一些不必要的行业，则有可能带来更多的风险，造成更多的麻烦。
红星新闻记者 闫宇恒 严丹 摄影记者 吕国应
编辑 刘宇鹏
