链得得直播 | SECBIT郭宇:智能合约审计的趋势是自动化和复杂化

链得得&安比 安比技术社区 2018-09-01 15:18

8月31日晚,SECBIT安比实验师创始人郭宇及其团队做客链得得《无眠吐槽大会》,与群友们探讨合约安全问题和“漏洞”中的机会,并就智能合约安全现状、应用、关键技术、解决方案、智能合约游戏漏洞以及区块链安全的商业模式等进行了全方位的分享。

Image


郭宇精彩观点汇总
1、 以太坊上大量的合约存在各种花样的整数溢出漏洞,有些可以直接导致 token 归零;
2、 目前智能合约中存在最普遍的安全问题是整数溢出漏洞;
3、 最棘手的智能合约问题业务逻辑漏洞,业务逻辑漏洞难以用机器自动发现,也较容易逃脱安全专家的审查;
4、 合约审计的趋势是,越来越复杂,越来越自动化;
5、 慎用“不流行的合约协议”;
6、 区块链态势感知系统主要依赖几个关键技术,即快速多维度地检索历史交易、恶意交易模式识别和合约代码相似度分析;
7、 未来可能出现巨无霸式的区块链安全公司,但垄断可能性不大;
8、 大部分智能合约安全问题具有一定的共性,研究结果可做移植;
9、 由于合约代码无法更改,已部署的 Fomo3D 模仿游戏合约中的漏洞无法挽救,不建议普通玩家投入资金。
10、针对复杂合约的审计需求会越来越大,短期内无法自动化或者免费。


以下是链得得“吐槽大会”之吐槽郭宇实录

         


主持人(仇杨涛):我先做一下自我介绍,我是链得得金融记者杨涛,主要跟踪报道全球上市公司的区块链布局和探索,欢迎大家提供新闻线索,我也十分乐意与大家一同去探索、发现“链”的价值。

主持人: 1.链得得怼友@zhfeng: 为什么用形式化验证解决智能合约安全问题?通过形式化验证的方式能不能得到“完美”的智能合约?

郭宇:形式化验证理论上可以解决所有的智能合约问题,但是实际上只能解决一部分的安全问题。形式化验证并不是银弹。

智能合约安全问题涉及的问题比较复杂,涉及到区块链共识协议,智能合约语言,智能合约编译器,智能合约gas机制等等。形式化验证比较擅长解决智能合约中由于业务逻辑而引入的bug。形式化验证也能很好地解决整数溢出这类问题,现在以太坊上大量的合约存在各种花样的整数溢出漏洞,有些可以直接导致 token 归零。

形式化验证这个术语中有个词 “验证”, 验证是比较 A 与 B是否一致。这么来看,如果要对智能合约的安全性进行验证,那么就需要能够精确地定义什么是“安全”。不幸的是,有些安全特性非常难以定义,比如涉及到区块链共识协议层面的问题。所以我说理论上是能解决安全问题,但是实际应用中,有些“安全”难以定义。

Fomo3D 最后的大奖被黑客利用技巧夺走,这种安全问题则是由于区块链共识协议导致的,目前很难用形式化验证来解决。通过形式化验证可以得到一个在安全假设下面的“完美”合约,但是这些安全假设可能包括:基于合约编译器的正确性,合约虚拟机没有bug 这些前提。这些前提其实并不是很可靠,历史上合约编译器出过不少的bug。

所以,智能合约的安全性是一个综合性问题,形式化验证适用于解决某些问题,但不是全部。

主持人: 2. 链得得怼友@寇静: 由于智能合约的不可篡改性,也就表明合约上线前的审计工作尤为重要,包括隐私泄露、代币转入转出、合约故障处理等在内的风险成为最关心的,目前智能合约存在最普遍的安全问题是什么?同时又有哪些问题最棘手?

郭宇:1> 目前智能合约中存在最普遍的安全问题是 整数溢出漏洞。我们通过工具扫描以太坊上所有的智能合约,发现各种花样的整数溢出漏洞,最著名的案例就是4月份的美链BEC安全漏洞,整数运算在合约中出现的频次非常高,包括整数之间的比较操作。

但是由于以太坊智能合约语言在设计之初并没有对整数溢出这个问题充分考虑,而大多数的程序员在传统的编程语言中,也没有对整数溢出这个问题足够重视,但是在智能合约语言中,整数溢出问题则可能是致命的。

实际上,在智能合约语言层面来彻底杜绝整数溢出问题并不是难事,只是现在以太坊不太容易对整个合约语言设施进行升级。目前有很多新的公链在开发中,对于这些新公链来说,修正以太坊智能合约系统的一些常见安全问题是一个比较大的机遇。

2> 常见的很多智能合约漏洞是比较容易发现的安全漏洞,比如整数溢出。检测这类问题并不难,棘手的智能合约问题是那些和业务逻辑相关的漏洞。智能合约业务逻辑漏洞是难以用机器来自动发现的,也比较容易逃脱安全审计专家的审查。审计者需要多业务逻辑有非常深入的理解,对于一些金融类合约业务,可能复杂度更高,专业性更强,也更难以被人工审计。

主持人: 3.链得得怼友@ CarlesZhang:安比实验室定位是智能合约安全问题,目前已经解决了哪些安全问题?

郭宇:我们针对不同的智能合约问题提供了不同的解决方案,也开发了不同的工具。安比实验室曾向以太坊社区报告了 ERC827 合约标准存在着严重的安全隐患,现在ERC827还处在撤销修订讨论的过程中。

我们也发现了一些公开的,曾经是被认为是“权威”的诸如 ERC20,ERC223的部分开源代码存在着安全漏洞。安比实验室开发了一套完整的针对整数溢出漏洞检测的工具,基本上对于合约的整数溢出漏洞检出率达到97%。另外安比实验室也开源了一个针对以太坊智能合约源代码的检测引擎——adelaide,能够对智能合约源代码的一些必要安全规范进行检查。

我们为公链提供一套新的安全智能合约语言方案、包括与之对应的编译器及虚拟机,能够彻底杜绝一些类型的安全问题。目前我们已经和多家公链有相关安全解决方案的合作。

主持人: 4.链得得怼友@ CarlesZhang: 安比提供的代码审计现在已经有哪些项目接受了?

郭宇:代码审计是我们工作的一部分,包括智能合约代码,钱包代码,公链等等,目前我们审计过的合约代码比较多,不能一一列举了。

我们合约审计工作最初主要集中在一些 token 合约上,后来逐步转移到一些复杂的金融类Dapp合约上,随着审计的合约越来越多,我们逐步在开发一部分辅助工具,把审计过程变得自动化。总的来说,合约审计的趋势是,越来越复杂,越来越自动化。

主持人: 5.常见ERC标准有ERC20, ERC721和ERC825等,安全公司如何在协议革新和安全迭代上保持同步?

郭宇:我认为,保持合约安全审计工作的更新和同步并不是一个很难的事情,目前来看,流行的合约协议都不复杂。但是对于一些不流行的合约协议,我们的建议是尽量少采用

主持人追问:如果安全系数为10分的,您所说的“不流行的合约协议”,安全性可以打到几分?

郭宇:合约协议的安全问题分为两个部分,合约协议的安全性与合约实现的安全性。对于一些不流行的合约协议,可能有些问题未考虑成熟,或者欠缺高质量的实现代码。比如ERC223的一个非常流行的代码实现就存在严重安全漏洞。

所以我们对合约开发者的建议是,对于看起来很美的改进型合约协议,请慎重。对于这类安全性,目前没办法定量分析。我们只是建议说,如果开发者选用非流行协议,请多多留意代码的质量,深入理解合约协议的语义,避免踩坑。

主持人: 6.链得得怼友@币燃plus: 比较出名的几家在做智能合约审计的安全厂商:知道创宇、慢雾科技、链安科技,包括360也开始参与智能合约安全审计中,怎么评价他们?

郭宇:除了这几家有名的安全公司之外,还有许许多多提供合约安全审计服务的公司或者团队。目前合约审计市场竞争比较激烈,但是缺少统一的审计规范,包括审计流程上的规范与审计内容上的规范。目前主流的审计方法还是人工审计,但是一些有技术实力的团队已经在进行半自动化的审计,审计成本正在快速下降。

随着安全开发意识的普及,越来越多的智能合约开发爱好者对于安全性有了比较高的认识,比如我们的安比实验室技术社区中,就有大量的合约安全性问题讨论。

我们安比实验室与绝大部分的安全审计服务不一样的地方在于,我们开发了一套采用形式化证明的方法来对合约进行审计和验证,这种方法能够杜绝合约的业务逻辑缺陷与安全漏洞,适用于一些对合约正确性要求极高的金融类智能合约,或DApp。

目前来看,简单的Token 智能合约审计门槛并不高,真正体现实力的是对于复杂智能合约的安全审计。

主持人: 7.链得得怼友@EL:区块链态势感知一般分为哪几块,可以监控哪些因素,需要用到什么技术?做到什么程度了,是不是仍存在一些问题?

郭宇:目前区块链态势感知还处于比较早期的阶段。区块链态势感知与传统的网络安全态势感知不一样的地方在于,区块链态势感知的数据源相对更有限,比如交易信息;另外也可以通过部署一些特殊的全节点,来从网络层获得更多的信息,但是目前来看能取得信息也相当有限。所以目前如何通过交易信息来分析一些常见的模式,分析出哪些交易有可能是异常交易,或者恶意交易,是一个颇有挑战的问题。目前区块链态势感知系统主要依赖几个关键技术:

第一个关键技术是如何能够快速多维度地检索历史交易,如何快速构建世界状态树(world state trie),以便于对账户地址做深度关联分析;

第二个关键技术是如何能够恶意交易模式进行识别,这需要人工智能的一些技术,并能最快地发现监测到可疑行为。

另外我们在分析fomo3d过程中,还发现了一个技术也比较有用,就是合约代码相似度分析,相似的合约代码能带来额外的一些有价值信息,比如合约地址之间的关联性,相似合约的交易关联性。区块链态势感知目前还有很多的工作值得去探索,处于早期阶段。

主持人: 8.链得得怼友@Vic: 你们是不是会通过发现漏洞来发起黑客攻击,既当白帽又当黑帽,这样来钱快?

郭宇:首先我们团队没有做过,也没有想过这么做,作为一个职业的安全团队,我们更珍惜自己的名誉,我们能够帮忙解决社区的问题,得到很多人的认可,我们会非常有成就感。

主持人: 9.链得得怼友@李岳恒@TokenUP首席产品经理: 区块链已经发生了很多安全问题,在未来,区块链安全领域能否形成类似360的存在?

郭宇:这个问题比较复杂,第一个,360是最早提出免费杀毒概念的公司,并且通过免费的模式迅速占领市场。我记得当年360安全卫士问世后不久,我放假回家就不用再帮亲戚朋友杀病毒重装系统了。未来随着基础安全服务成本的下降, 一些基础的安全服务是否有可能完全免费,或者大范围普及? 我觉得是非常有可能的。

第二层含义:未来是否有可能出现像360这种巨无霸式的区块链安全公司?我感觉区块链行业才刚刚开始,并且一上来就是全球化,未来在某些细分领域的安全市场可能会出现爆发式增长。未来的这个安全市场体量可能完全超过现有的市场,所以真的有可能出现巨无霸式的区块链安全公司。

这个问题还能从第三个层面来看:未来是否会出现一个垄断性,有能力解决所有安全问题的全能业务公司?我认为这个可能性并不大,因为区块链技术发展太快了,未来安全问题会层出不穷,所以我觉得任何一个小团队,无论何时进入安全领域,都有找到自己的机会。

主持人: 10.在安全领域如何衍生出新的商业模式?

郭宇:这个不好预测,360当年的免费杀毒商业模式也是在不断试错,逐步形成的。这个需要大家一起探索,区块链本来就是一种生产关系的变革,所以改变商业模式是区块链行业的特长,让我们拭目以待吧。

主持人: 11.链得得怼友@ EL: 目前有多样的区块链、智能合约,而这些合约是由各种不同程序语言编写的,有C++,solidity,javascript等等,那保证智能合约安全是不是可以粗略的分两条路而走,一个是广义的可以针对所有智能合约安全问题,比如态势感知、bug bounty等等,再一个就是分而治之,针对每种程序语言或者每种区块链平台的执行环境设计不同的解决方案?

郭宇:这位网友总结的非常到位。我非常同意EL的看法。补充一下,我觉得还可以从行业业务这个角度来看:抛开智能合约语言,抛开智能合约安全服务类型,针对不同行业,会有不同的安全服务重点,比如金融行业,和游戏行业,对于安全服务的侧重点都可能不太一样。区块链安全,智能合约安全,我觉得目前的问题只是很小的一部分。也许3年以后回头看,区块链安全服务会发生非常大的转变,是和现在完全不同的内容和模式。

主持人: 12.链得得怼友@ EL: 最近一篇由ETH研究的Securify,其中提到的安全模式仅针对solidity语言来说的,发的是安全会议的顶级paper——CCS,但是我觉得于solidity本身而言其安全模式不一定全,针对更多种其他的智能合约模式(比如EOS的C++程序)也不一定适用,所以这种安全模式的设计是不是在不同环境下的合约有所区别,分别研究呢?

郭宇:目前一些不同公链平台上,智能合约的语义模型差别还是比较大的。智能合约的安全模式,我认识只是一种近似的安全定义,并且securify的这种全自动的智能合约检测方式,很难避免误报与漏报的情况,所以我们也很难说什么是“完全的”安全模式,也许我们永远定义不出来。但是securify 只要能将检测准确率控制在一定的范围内,会是一个比较强大的工具。

针对不同的智能合约,由于底层字节码或者源语言的语义的差别,不太可能做出统一的工具,最好的方式还是针对特定合约平台的检测工具。不过从另外一方面将,纵然合约平台存在一定的差异,但是大部分的安全问题仍然具有一定的共性,一些研究结果是可以做移植的。

甚至有一些公链采用函数式的合约编程语言,有些安全检测方式是仍然适用的。这个问题太专业了 我就不展开讲了。

主持人: 13. 一周前你们在一款类似于Fomo3D的游戏Last Winner中发现黑客利用游戏随机数盗取了1200万人民币。这种漏洞是否在所有类Fomo3D游戏中都会存在?玩家只能永远主动去当受害者吗?

郭宇:修复随机数漏洞就可以了。所有直接拷贝 Fomo3D 源码的游戏都存在同样的漏洞,普通玩家的利益确实会受到较大威胁。对于已经部署的 Fomo3D 模仿游戏,由于合约代码无法更改,这些游戏合约中的漏洞会一直存在并且无法挽救,我们是强烈建议,普通玩家不要投入资金在这类游戏中。

我先呼吁一下,对于仍在开发阶段的游戏,实际上有多种方案可以解决这些漏洞,我们呼吁游戏开发方重视这些安全问题,Fomo3D的随机数产生过程存在比较严重的漏洞,现在是有比较简单的随机数漏洞修补方案的。我们后续会专门整理讨论安全随机数方案。

主持人: 14. 随机数一直是区块链平台的短板,以太坊和EOS均未提供随机数接口,对于以公平为主的游戏来讲,随机数生成至关重要。但是黑客却可以生成大量随机数,在小概率的获奖环节中获得巨大优势。所以,如何破解“随机数“难题,让玩家公平参与游戏?

郭宇:黑客的嗅觉非常灵敏。目前以太坊和EOS平台在没有很好解决隐私问题之前,是很难提供密码学安全的随机数的,但是如果退一步,给特定业务场景提供一些比较公平的“随机数”是有不少现有方案的,比如commit-reveal 方式的随机数方案,randao,oraclize,commit and claim 等。


自由吐槽环节

链得得怼友heige:怎么看待免费的合约审计 或者 合约审计最后的商业出路在哪里?

赵坤@SECBIT:有了360免费模式,现在大家都很容易想到做免费模式,但是免费之后怎么赢利,却是一个大问题。现在审计业务竞争很激烈,免费不是没有可能。

链得得怼友heige:目前已有部分团队对外发布了免费的检测平台或者工具。

赵坤@SECBIT:免费的工具目前看有一定的效果,但是不能取代安全审计,很多问题还是需要人工来解决。目前的审计还都是收费的,还是有大量的人工投入在里面。现在大家的安全意识在不断提高,不一定每次审计都能发现问题哦。但是这种分化是否能出现,也要走一步看一步

郭宇:审计自动化程度在提高,这是不可避免的趋势。审计成本下降,审计门槛降低,这个不可逆转。但是免费是否是一个可以长期持续的商业模式,我还没有找到答案。我感觉未来可能会出现针对不同类型的客户提供不同级别的安全服务。

其实智能合约审计只是区块链安全里面很小的一部分,目前也不是我们的重点。智能合约的安全不一定通过审计来解决,审计是所有方法里面比较低效的。这是针对erc20 token合约吧?

erc20合约复杂度比较低,这个市场可能已经是红海了,但是针对复杂合约的审计,目前还是非常值得去探索的,而且这部分需求未来会越来越大。这部分对于安全审计的要求更高, 我认为短期内无法自动化或者免费。

链得得怼友heige:如果这个事情交易所干了呢?

郭宇:现在交易所就在干啊。

赵坤@SECBIT:比如我们可以加强智能合约语言和编译器的安全性,可以在早期避免90%以上的智能合约安全问题。

链得得怼友heige:重点在哪里 ?

赵坤@SECBIT:重点是全方位的安全,早期方案,以及后期防护都包括。

链得得怼友heige:哪里都是重点啊 。

赵坤@SECBIT:安全没短板,都是重点,任何一个方面没做好,都可能带来严重后果

链得得怼友蔡栋:跟链安对比,请问SECBIT有哪些明显优势和劣势?

郭宇:我们和链安杨老师团队都有高校科研背景,都在力图将形式化验证理论应用到智能合约安全方面,但是目前我们和杨老师团队走的路线略有不同,杨老师团队目前侧重点在于合约审计服务VaaS上,而我们目前的侧重点在合约底层基础以及合约形式化证明上。

链得得怼友@小迷妹:有没有想过借助区块链实现财务自由?

赵坤@SECBIT:我们是区块链的坚定信仰者,财务会不会自由不知道,技术肯定是自由的

链得得怼友怼友@ping:你觉得目前区块链安全行业处于哪个发展阶段?最大的安全隐患是哪些?

郭宇:目前区块链行业还处于早期阶段,很多人来把现在的区块链技术比作比92年的互联网技术,所以区块链安全技术也是出于非常早期的阶段。

赵坤@SECBIT:区块链安全还处于非常早期,从非技术因素上来讲,最重要的是大家对安全的重视。

链得得怼友:智能合约足够智能吗?在AI技术没有重大突破的情况下,程序员用条件和循环语句写出来的代码到底有多智能?或者说智能仅仅指的是是根据预先设定的条件自动执行?

郭宇:智能合约的smart 应该不是人工智能的那个智能,感觉目前智能合约与AI还没有半毛钱关系,至于未来有没有关系,还需要大家的努力啊。

主持人:感谢大家近三个小时的陪伴,感谢安比(SECBIT)实验室的郭宇总、赵坤总。郭博士严谨的逻辑和专业能力完美契合,

一个蓬勃发展的市场,安全永不缺位,感谢这些为区块链发展去打造安全环境的技术极客们,本期链得得“吐槽大会”到此结束。

往期回顾

Image Fomo3D 千万大奖获得者“特殊攻击技巧”最全揭露


Image 智能合约史上最大规模攻击手法曝光,盘点黑客团伙作案细节


Image 构造形式化证明,解决智能合约安全问题——你的合约亟待证明


Image 安⽐(SECBIT)实验室携⼿路印(Loopring)共同发布智能合约风险列表




以上数据由安比(SECBIT)实验室提供,安比实验室致力于解决区块链全生态的安全问题,共建共识、可信、有序的区块链经济体。合作交流请联系 info@secbit.io

Image


安比(SECBIT)实验室

info@secbit.io


Scan to Follow