更多精彩 >

成都链安科技CEO杨霞:80%的智能合约都存在安全漏洞

2018-08-23 10:54:27   来源:财链社    作者:李澍 熊吉 

摘要:链安科技创始人杨霞表示:基于区块链加密数字货币引发的安全问题,来源于区块链自身机制安全、生态安全和使用者安全三个方面。在区块链自身机制安全方面,智能合约的安全性至关重要。

捕获.PNG



杨霞 | 成都链安科技CEO,创始人,电子科技大学副教授,最早研究区块链形式化验证的专家;一直为航空航天、军事领域提供形式化验证服务,主持国家核高基、装发重大软件课题等近10项国家课题;CC国际安全标准成员、CCF区块链专委会委员。


记者 | 李澍

编辑 | 熊吉

  

腾讯安全日前发布的报告显示,与加密数字货币有关的黑客攻击事件,从 2013年到2018年上半年增加了约五倍,全年预计增加10倍左右。其中,仅今年上半年,黑客对加密数字货币的攻击,就已经造成了20亿美元的直接损失。


基于区块链加密数字货币引发的安全问题,来源于区块链自身机制安全、生态安全和使用者安全三个方面。在区块链自身机制安全方面,智能合约的安全性至关重要。


据链安方面的数据显示,2011年至2018年,由智能合约安全事件导致的经济损失达12.4亿美元。目前,由智能合约安全事件导致的经济损失已经超越交易所,位列第一。


智能合约作为执行合约条款的计算机交易协议,对所有用户都开放,导致了内部存在的安全漏洞也随之公开暴露在黑客面前。


而且,智能合约一旦上传即公开且不可更改,因此现在的区块链项目,对于安全性的需求更加迫切。因此,在智能合约正式开始运行之前进行安全审计就显得尤为重要。


链安科技创始人兼CEO杨霞表示,从目前研究来看,80%的智能合约都存在安全漏洞。在合约开发前、开发过程中和编写完成后,整个项目周期都要保证智能合约的安全性。


杨霞2.PNG


在合约开发前,开发者应进行智能合约相关漏洞风险知识学习,了解最新的智能合约安全漏洞,避免开发的合约中存在安全隐患。


在开发过程中,Remix-IDE、truffle等编译工具会对合约中不符合最新规范的代码提出告警,开发者需要对告警引起重视,强烈建议开发者更改自己的代码,以消除编译过程中的告警。


在合约编写完成后,需要对合约功能的完整性和安全性进行测试,确保合约逻辑实现与设计相符,确保无安全风险;最后,可以寻找专业的智能合约审计团队进行合约审计,最大程度地减少安全隐患。



01

智能合约形式化验证应用状况


 

2016年9月1日,万向区块链实验室肖风在为《区块链革命》作序时曾写道:“The Dao”事件提醒我们,应该有一个能对智能合约进行事先检验的科学方法,但这方面最先进的技术如形式化验证,目前还处于理论研究阶段。”可是如今形式化验证已经被正式用于智能合约的检验中了,这就是技术的进步。


形式化验证指的是用数学中的形式化方法对算法的性质进行证明或证伪。

据了解,一般来讲,方法有两种:


一种是模型检测,即把系统所有可能的状态列出来并一一进行检验,此种方法是全自动化的,但是只适合小型系统;


另一种是定理证明,即首先把系统代码标记成抽象数学模型,然后对定理进行证明,此种方法适合大型系统,但是需要首先人工将系统的运作方法转换成验证系统可以理解的语言。


杨霞3.PNG


目前区块链产业中与形式化验证相关的产品可以分为三类:  VaaS平台,公链和语言。


杨霞4.PNG


目前,主要从事智能合约形式化认证的区块链安全公司主要有7家,分别是成都链安科技、Imandra、Certik、The Matrix、Securify.ch、Runtime Verification和Tezos。其中,从事VaaS形式化验证平台研发的有四家,分别是:成都链安科技、Certik、Securify.ch和Runtime Verification。


其中,链安的特色在于:提供多个区块链平台验证工具,而不是单一地为以太坊或者EOS提供智能合约形式化验证。


杨霞5.PNG


杨霞是2016年才开始接触区块链的,正赶上了著名的以太坊The Dao事件,在此之前,杨霞老师一直专注于为航空航天、军事领域提供形式化验证服务。


“其实那个时候真的没有太在意。不过我有一个朋友在搞区块链,他跟我说你搞形式化验证,能不能去验证一下智能合约的安全,比如针对Dao系统的安全事件。”杨霞回忆道,“我觉得挺有趣的就去试了一下。那时候我们还没有自动化的工具,只能靠人工进行代码的形式化描述,然后去证明。最后发现,形式化验证方法应用于智能合约安全审计效果不错。”


杨霞6.PNG


也许当时选择将形式化验证应用于区块链智能合约的审计是一个偶然的机遇,但是,通过杨霞和她的团队经过一年半左右的潜心研究研发出了自动化的智能合约安全验证平台VaaS。


目前,链安的VaaS平台支持EOS和以太坊的智能合约的安全审计,VaaS也是全球第一个支持EOS的智能合约验证平台。



02


形式化方法像一套完备的法律


被问到如何向技术小白解释形式化认证,杨霞表示“形式化方法就像一套完备的法律,规定了每个角色能做什么和不能做什么,并对角色之间的关系进行界定。类似于社会系统架构对不同角色进行分类,在承认个体天性的同时,使系统的复杂程度降低了多个维度。”


形式化验证通过数学建模的方式,对合约进行验证,发现合约的未知的潜在的风险。


因为是用数学证明的方式去发现问题,所以首先需要一个函数的详细功能规范,形式化验证就依据这个功能规范去证明实际的代码是不是和需求一致,如果是函数的规范足够完整并且能够清楚无歧义的表达,那么是可以发现针对这个被验证的函数之前没有发现的问题。


形式化的抽象可以从复杂的事物中抽离出本质。举个简单的例子,一个构造复杂的中式凉亭,经过形式化的方法抽象过后,可能只是一个分层的三角形,这就相当于一个精简的解读。


杨霞7.PNG

在验证安全之后,通过使用可执行模型,将较高级别的抽象模型转换为较低级别的代码。形式化方法使智能合约的生成和执行有了规范性约束,保证了合约的可信性,使智能合约的生产过程和执行效果得到了保障。


 据杨霞表示,目前,理论上讲,形式化认证可以找出所有已知的和未知的智能合约安全漏洞。而实际操作中,形式化工具可以查出80%的常规漏洞,对于部分结合业务逻辑的漏洞,还需要人工复核。



03


智能合约小白级漏洞居多


区块链行业的安全漏洞是不断涌现的,尤其是涉及到“钱”的安全漏洞,可以使人们的数字资产瞬时归零。目前,随着漏洞不断被挖出,很多数字资产投资者也陷入到了恐慌之中。


杨霞老师表示,就智能合约来讲,80%都存在安全问题。


就目前看来,智能合约中还是小白级的错误居多,包括一些造成巨额财产损失的漏洞。


举个例子,2018年4 月 22 日 13 时左右BEC智能合约被爆出的整数溢出漏洞,黑客能无限印币,在一次交易中,也就那么几秒钟的事情,黑客就“无中生有”地给两个账户转了天文数字般的BEC币,而原账户一分BEC币都没损失。一行代码就造成了60多亿人民币的损失。


整数溢出就像是水轮车。往里面加水,加满之后,继续加水,水轮车将会失衡并转动,此时水将会被全部倒出来,并重新盛水。当变量累加到超过自身容量范围时,将会溢出,归零。而黑客也是利用了这一点,把运算前的数值作为转账金额,把运算后溢出的0作为检测条件,从而实现绕过。


这是一个很简单的逻辑,但是后果却很严重。


同样,之前爆出来的以太坊平台的漏洞,短地址攻击,以及拒绝服务攻击等等的漏洞的逻辑也都很简单,但是这些漏洞都造成了人们数字资产的巨大损失。


其实,这些漏洞在智能合约正式开始运行之前,都是可以通过形式化验证的方式找出来的,并加以修复的。


杨霞8.PNG


链安采用数学的证明方式将代码形式化描述为公式,并对其进行逻辑漏洞和安全漏洞证明,基于此原理,实现了自动化的验证工具,能够方便、快速地验证出代码的功能正确性和安全属性。


杨霞老师表示,目前,成都链安科技的优势集中体现在三个方面:


第一,我们专注只做智能合约的安全。


第二,我们在技术上有优势,我们采用了严格的形式化验证的方法,为智能合约提供更加完备的安全审计。


第三,我们率先研发了自动化的智能合约安全验证工具VaaS,在智能合约的审计过程中,我们通过自动化工具VaaS和人工结合的方法比全人工的安全审计方式更准确、更高效。


对于未来区块链安全的走向,杨霞老师表示,安全是一个持续完善的过程,没有绝对的安全,越是复杂的软件系统,出现安全事件的概率越高。


为了避免安全事件的发生,最好的办法就是提高软件开发人员的安全意识,并对智能合约在部署之前进行全面的安全审计。


我们要理智地看待区块链技术的漏洞,区块链作为一个新兴技术,出现安全事件是可以理解的,不能因噎废食。












猜你喜欢

智能合约和传统合约的区别

资讯区块链智能合约传统合约

智能合约和传统合约有很多相似之处,传统合约又称为法律约束准则。它们都对参与者的权利和义务进行明确,违...

2018-10-08

从供应链金融看区块链应用落地的关键

资讯供应链金融区块链智能合约

为什么区块链技术发展至今还没有发展出一个结合实体经济的有效的落地应用的项目呢?下面我们从一个关于区块...

2018-09-22

当谈到区块链安全,我们一般会谈论什么?

资讯区块链智能合约区块链安全

宇宙就是一座黑暗森林,每个文明都是带枪的猎人,像幽灵般潜行于林间,轻轻拨开挡路的树枝,竭力不让脚步发...

2018-09-13

智能合约查询平台上线 安全与否一查即知

区块链智能合约

在区块链世界里,智能合约的存在是为了规定交易双方的权利和义务,并把行使这些权利和义务的过程广播到整个...

2018-09-06

珍爱生命,远离狂人!起底狂人发迹史,揭露毒瘤真面目!

资讯区块链刘佳

所有人都知道币圈是个零和游戏,不可能所有人都赚钱,也就意味着,你赚到的钱都是别人亏出来的,那现在你百...

2018-08-22

“虚拟经济”上市潮起:比特币“矿机”生产商闯荡资本江湖

资讯区块链虚拟经济

与大多数科技企业选择今年上市类似,随着宏观环境及行业变化,加之监管的趋严,“矿机”三巨头的上市也被认...

2018-08-22

链改下的交融共识

资讯区块链链改

各城市节点、企业节点、个人节点都纷纷加入链改,并达成对链改的广泛共识。在共建、共治、共享的基础上,各...

2018-08-22

什么是虚拟货币、数字货币和加密货币?三者如何区分?

资讯区块链数字货币

加密货币是基于某种加密算法创建的数字货币,所以称为加密数字货币更好理解。加密货币并非由任何中心化机构...

2018-08-22

曹辉宁:我不信仰比特币,我信仰科学、逻辑和数据

资讯区块链

“区块链首先要解决的是物质需求,互联网、区块链是一样的,逻辑一致,相互映射。” Usechain创始...

2018-08-21

方军:机器比人更需要通证(Token)

资讯区块链

在讨论数字世界中表示价值的通证(Token)时,我们常会拿它跟法定货币作比较,这会带来一个疑问:在很...

2018-08-21

巴克莱银行有意开设加密货币交易平台

区块链加密货币巴克莱银行

据知情人士透露,国际投行巴克莱(Barclays)一直在评估是否有可能开设一个加密货币交易平台。

2018-08-21

不谈远景,我们现在该怎么看区块链?

区块链区块链人才区块链生态技术

BCCon全球区块链生态技术大会,于2018年8月18-19日在北京国际会议中心顺利举行。

2018-08-21

2018亚洲海上区块链论坛:探索区块链真实的现在与未来

互联网资讯区块链区块链媒体

时间走到2018年年中,区块链已不再是极客们圈地自娱的存在,而是更直接的触达到了人们的视野中

2018-08-21

OK资本竞选EOS超级节点的六大优势

资讯区块链OK资本EOS节点

OK Blockchain Capital(简称OK资本) 为全球领先区块链集团 OK Group ...

2018-08-21

财链社(www.bcpress.com)专业的全球区块链财经媒体与社群,链接区块链、物联网、大数据、人工智能,致力于成为最有深度的区块链全产业链分析家,为区块链创业者及投资者提供最好的产品和服务。

链马思享会第四期:公信宝黄敏强,如何应对数据经济困局?

在信息安全问题日益严峻的今天,作为普通互联网用户,该如何保护自己的隐私?

INE智联生态COO白眉独家|区块链4321黄金投资法则

不是所有的区块链项目都在落地,INE智联生态一直在落地!——IntelliShare does ...

INE智联生态COO白眉独家|区块链4321黄金投资法则

不是所有的区块链项目都在落地,INE智联生态一直在落地!——IntelliShare does ...

马云:并不是数字化就会变得冷淡 技术让城市变得更暖

10月11日,杭州市打造全国数字经济第一城动员大会在浙江杭州云栖小镇国际会展中心举行。

央行姚前&孙浩:数字稳定代币的试验与启示

虚拟货币无法有效履行计价单位、交易媒介和价值储藏三大货币基本职能,客观上阻碍了其自身的应用进程。因此...

一起寻找“全球链改优秀项目”!

一起寻找“全球链改优秀项目”!

2018年9月10日,由中国通信工业协会区块链专业委员会、区块链改革全国联席会议作为指导,全球链改节...

HelloEOS 区块链全国行活动“EOS 和他的朋友们”正在进行

HelloEOS 区块链全国行活动“EOS 和他的朋友们”正在进行

HelloEOS 区块链全国行活动“EOS 和他的朋友们”正在进行,第六站厦门将在本周六(9月8日)...

区动智慧,链接未来-区块链如何赋能实体经济

区动智慧,链接未来-区块链如何赋能实体经济

自区块链概念流入国内,吸引大量人才进入到这个行业,随着区块链掀起的火热风潮,它被视为本世纪最大的风口...

区块链峰会受监管政策屡屡叫停,920这场峰会却办得热火朝天

区块链峰会受监管政策屡屡叫停,920这场峰会却办得热火朝天

“2018国际数字经济博览会”将于9月20日-22日在石家庄国际会展中心隆重举办。本次峰会邀请到了诸...

嘉楠耘智推出7nm矿机新品,算力翻倍

嘉楠耘智推出7nm矿机新品,算力翻倍

据中关村在线消息,目前首批由台积电代工生产的7nm芯片已完成交货。