2018年初，日本第二大虚拟货币在线交易所Coincheck遭受到黑客攻击，该案当时被称为“史上最大虚拟货币盗窃案”，据称损失超620亿日元(约合30多亿元人民币)!最近，区块链成为炙手可热的技术，但这个人人皆知的技术却并没有想象中那么安全。而成都一家公司研发的全球首个“一键式”智能合约自动形式化验证工具，可一键查验代码漏洞，其检测准确率超过97%。

成都商报-红星新闻记者 闫宇恒 严丹 摄影记者 吕国应

投入

从区块链安全事件中嗅到商机

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

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

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

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

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

研发

形式化验证将可能问题进行穷举

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

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

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

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

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

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

专家提醒

区块链不是万能的

不必为了用而用

虽然有“一键式”验证技术，但你以为，区块链的安全问题仅仅是验证一下代码就可以完成的吗?

区块链安全风险贯穿始终。“以全球最知名的以太坊链平台为例，其智能合约代码具有不可更改性，一旦部署将无法修改。如果智能合约代码一旦有漏洞，就只能眼睁睁看着被攻击。”杨霞说，随着区块链应用进入我国国计民生相关的各个领域，而其关键程序智能合约存在漏洞将严重影响系统的运行，甚至导致项目失败，链上资产和数据全部丢失。

在运营阶段，黑客会通过DDoS攻击、漏洞入侵等方式降低交易平台的可用性，窃取账户，资产等。而若智能合约存在漏洞将严重影响整个项目，甚至导致项目失败。在推广时期除了网络攻击，平台还可能遭受薅羊毛等业务欺诈、山寨仿冒等钓鱼欺诈。

“目前，整个区块链行业还处于开发阶段，不确定因素较多，没有必要为了用而用。”杨霞认为，区块链适用于物流、保险、金融、法院、供应链等行业，并在一定程度上能大大促使这些行业的加速发展，但在一些不必要的行业，则有可能带来更多的风险，造成更多的麻烦。