在过去的7个月,安比(SECBIT)实验室像一架装备一流、勇猛无敌的新型战机一样,在一次次”战役“中,迅速确立起了不容小觑、不可或缺的地位。这仅是故事的开端……
如果你向海外的区块链项目咨询,问他们所听说或者合作过的,国内靠谱的安全团队有谁,安比大概率是被最先提及的对象。
这家成立于今年3月的区块链安全团队,凭借对形式化验证的深度研究,以及在保障智能合约安全上的成熟运用,仅仅用了半年多时间,便在国内和海外获得了不错的知名度和口碑,并且是在老牌互联网安全公司触角逐步伸向区块链,新手安全团队不断入局的大环境下。
用《CoinVoice》特别采访到的,已经与安比合作近3个月的公链项目——Vite创始人刘春明的原话来说,“做安全的技术门槛非常高,尤其是形式化验证这块儿。因为我本身读研的时候也是做形式化验证研究,所以比较了解。安比这边,尤其是郭宇,他在专业领域是国内最顶尖的了,他的团队非常的专业。”
刘春明所提到的郭宇,正是安比的创始人。在创立安比之前,郭宇有很多身份,他是中科大博士、耶鲁大学访问学者、中科大副教授,研究形式化验证整整十三年。
在专访郭宇后的两天里,我脑中闪现过很多词来概括我对他的理解,但都觉得不够确切,最后,我想到了赤子之心。
一位苦苦钻研一项技术十几年,可那项技术只被应用在航天、核电等安全攸关领域的顶尖专家,偶然间发现,多年研究的技术,在一个有很大影响力的新行业,存在非常理想的应用场景,并且还有许多未知可以探索的时候,内心该是怎样的激动!
“那段时间,我心里好像一直有个声音和我说,这件事你不干一定会后悔。”技术不应该只造福一群人,而应该造福全人类。
这种“不干一定会后悔”的信念和赤子之心,映射在创业上,是极高的热情、战斗力和格局。
安比的同事说,郭宇常常会就一个技术问题和大家通宵讨论,在安比团队成立的7个月里,他们已经推出了5个开源工具和引擎,有20个正在内部打磨,将分阶段推出。达成战略合作,以及审计过的区块链项目已有50余家。今年10月,著名以太坊安全团队Diligence-ConsenSys,在柏林会议上郑重宣布,安比将作为他们主要技术合作方,与其协作打造智能合约安全平台 Mythril.ai。
除了利用形式化验证,帮助智能合约规避漏洞,抵抗攻击外,他们还在忙于开发合约语言安全编译器。让开发者在部署编译的时候,就可以发现问题,避免写出错误的程序,降低项目方在安全上的投入成本。治病于未发之时。
对于现在的安比来说,他们完全有资格和实力生出野心,谋划在未来的商业竞争中,夺得第一的席位,但郭宇不想安比成为巨无霸。他想把安比打造成一个重要的“器官”,和其他团队一起,让区块链生态越来越安全,成长得越来越好。
仔细琢磨郭宇下面所说的话,你会发现他和乔布斯有那么一点像,仅仅用商人来归类他们,似乎不太合适。
|野望
我们想成为一个非常重要的器官,在一个生物体内,当巨无霸不是什么好事。
《CoinVoice》:听你的朋友说,你很喜欢穿一件T恤,上面印着code is cheap, show
me the proof。
郭宇:这句话是talking is cheap, show me the code的升级版,也是我的一种理念。在区块链行业,不仅要实践(不只是嘴皮子功夫),而且要证明安全。
《CoinVoice》:但有人认为,耗费太多精力和财力,在证明智能合约代码安全、没有Bug上,必要性不是特别大。因为只要是复杂的代码,就一定会出错。
郭宇:智能合约与你看到的很多互联网系统软件代码不一样,后者发现Bug了,修改就可以了。但智能合约一旦被部署到区块链上就不能再修改,所以它本身一定不能出错。
真正的区块链可信要做到两个维度,第一个可信是智能合约在执行过程中,没有任何一个个体能够干扰,第二是这个程序本身要是正确的。如果这二者都能做到,那才是一个非常完美的可信的基础。
《CoinVoice》:安比为什么选择“形式化验证”这种方式,来证明智能合约安全与否?形式化验证在此之前只被应用在航天、核电等安全攸关的领域。
郭宇:我研究形式化验证已经十三年了,它是一个很小众的研究方向,技术门槛非常高。形式化验证的对象是程序,它要解决的问题,是怎么保证软件里没有bug。即规避错误、对抗攻击。
传统上,大家写了程序,如何保证程序没有问题?其实办法并不多,最好的办法就是拿来用一用、跑一跑,如果跑得正常,就没有问题,这是一个很朴素、很简单,而且大家日常都在用的办法——测试。
但对于一个程序来说,哪怕是非常短的程序,它可能出现的组合情况,也会像天文数字一样,你不可能在有限的资源下重组程序所有的可能性。大部分软件测试,都只是测试了大部分情况,总会漏掉一些情况。而人很难想得到的地方,反而特别容易出问题。这就是为什么软件避免不了有Bug。
形式化验证不是用测试的方式测,而是用写程序的逻辑来推理。它的基础理论是数学逻辑和数理逻辑,我刚才也说了,软件这种状态、空间是一个天文数字,推理是从逻辑的方式,并不是一个一个很傻的试,是一片一片,分了好几个部分。可以保证把所有情况百分百覆盖的特别好,这是用形式化验证一个特别关键的地方。
当然,程序分很多种,手机里面也是程序,我们电脑里面也有很多设备,但并不是所有的程序都适合,或者有必要用形式化验证。
《CoinVoice》:为什么智能合约非常适合,而且有必要用形式化验证?
郭宇:第一、智能合约特别重要,它实现了一个信任的点。在区块链系统里面,一旦哪个很信任的东西不受信任了,或者是出了问题,这个系统就相当于不会被人再用了。像智能合约发行Token数字资产,如果出了问题,这个项目可能一文不值,所以无论用什么办法,都需要保证它没有问题。
第二、智能合约逻辑相对比较复杂,现在简单的合约一两百行,复杂的有几千行,智能合约做的事越来越复杂,参与方也特别多。一个合约或者是一个去中心化应用,每一个参与方都有参与的业务逻辑。当很多的参与逻辑搅在一起的时候,就是一个非常复杂的系统,越复杂的系统就越容易出问题。
第三、智能合约从合约的设计层面来看,比较适合用形式化验证。为什么?因为它的复杂性都来自于它的逻辑复杂性,而逻辑复杂性就意味着这个状态空间会比较大,不太适合用传统测试的手段去测,反而特别适合用形式化验证。
《CoinVoice》:如果哪一天,安比成为一个让用户放心的标志。大家认为只要是你们检测过的项目,一定不会出现智能合约安全问题。那安比就成功了。
郭宇:这里我需要纠正一下,我创立安比的初衷不是要成立一个新的权威,这不符合区块链精神。区块链精神就不应该信任任何一个权威或区块链节点。所以说,我们的初衷,是打破这种中心化的权威。
传统的代码审计和安全服务,是需要权威的,它需要一个权威的品牌来背书。但你要知道,这种权威性不可能永远存在,只要出一次事故,就会受到很大威胁。比如某些专家很牛,可专家也会有意和无意的出错,一旦把安全假设放到一个人身上,是很危险的。
我们现在用的这种形式化验证和形式化证明,就是解决这个东西,我们不想依赖于一个权威来说它没有问题,比如说我这个合约是没有问题的,我不能说打个勾就可以了,或者是安比验证没有问题。
我们应该怎么做?打个勾之后,给出一系列证据。证明就是用数学的逻辑,这种非常严格的语言写出来的。任何人你只要学过这个语言,都可以检查这个证明对不对。一旦这个证明是对的,你就可以相信这个结论。证据本身自己就有说服力。
《CoinVoice》:所以你对安比最长远的企盼是?
郭宇:我是一个有区块链信仰的人,区块链改变了生产关系、管理模式,把很多人聚合在一起。我觉得安比可以成为给区块链生态安全做出贡献的团队,我们希望跟很多产品紧密地配合,大家一起让区块链生态变得非常安全,让这个生态非常健康有序地慢慢成长起来。
《CoinVoice》:难道安比不想成长为巨无霸?
郭宇:我们想成为一个非常重要的器官,把我们最擅长的东西拿出来解决问题。在一个生物体内,当巨无霸不是什么好事情。
《CoinVoice》 :在互联网安全领域,没有跑出巨头,你觉得在区块链领域能吗?
郭宇:有可能。
《CoinVoice》:为什么?
郭宇:跟传统安全相比,区块链安全需求更迫切、更强烈、规模更大,而且它一上来面向的就是全球市场。任何团队都有希望迅速成长,至于能长多大的体量,很难预测。
《CoinVoice》:虽然面向的市场很大,但现在已经有一些项目快活不下去了。
郭宇:你要看到,区块链技术本身发展还是很快的。现在和2016年相比,在认知维度、技术维度,几乎发生了翻天覆地的变化。我觉得一切才刚刚开始。
这个行业变化特别快,给安全团队和区块链项目提出了很高要求。在各种迅速变化的市场和迅速变化的技术面前,如何调整、如何找到自己适合的位置,需要坚持,也需要灵活,这个还是挺有挑战的。
《CoinVoice》:有没有什么方法论,使区块链公司能够适应这种快速变化?
郭总:区块链技术,你把它单个拆开看,都没有那么难,单拆开密码学看,就是一个椭圆曲线,数字签名,那只是教科书上的一章;像区块链里面一些公式协议,像挖矿,也挺简单的,但是区块链妙就妙在,把很多很简单的概念融合在一起,融合之后,就没那么简单了。
所以,我的方法论简单来说,从内在看,你要对整个区块链技术也好,各方面技术也好,都需要去学,学完之后再从宏观角度思考。这样的话,就可以找到这里面快速热点切换的规律。
我们团队很少有人专职做这事,专职做那个事,很多事大家都能干。因为这样,才能对区块链有一个非常全面的认识,不能说这个人只关注程序安全,那个人只关注密码安全,这不行的。
|路线
“治病于未发之时,治病于微起之时。”
《CoinVoice》:从今年3月算起,安比成立也有大半年了,取得了哪些成绩?
郭宇:成绩谈不上,我简单说一下。首先在理论层面,我们总结出了智能合约安全三大问题:第一、常见的漏洞:整数溢出漏洞、业务逻辑漏洞;第二、不规范问题;第三、权限问题。并对这些问题进行了详细分析。
其次,我们开发出了一系列漏洞扫描工具和引擎。已经开源的有5个,还有20个工具我们内部正在打磨。今年7、8月,我们还接受以太坊社区比较知名的 安全团队——Diligence-ConsenSys的邀请,成为他们关键技术合作伙伴,共同协作开发一个很大的智能合约安全平台。
除此之外,我们与路印 、PCHAIN、Dora、Themis、Vite、Ultrain等众多项目达成了战略合作。至于审计过的项目已经有数十家,在此我不一一举例了。
我们还证明了像ERC20,ERC721一些模板代码,把数学证明和整个证明过程也放在了网上,我们是把成果第一时间把这些东西开源出来的团队,这些形式化证明代码也是第一个开源的研究成果 。
《CoinVoice》:你们和ConsenSys联合发布“ERC20 合约形式化证明源码模板库“的事情,我也有听说。但我不明白你们这样做的目的是什么。
郭宇:之前行业里,一直有人在提形式化验证,网上也有很多文章文字,说形式化验证多么好,但是始终没有团队愿意开放出来。国外团队有一两家是稍微放出来一点东西,但不完整。
我们觉得很必须开放出来,给大家看一看,这个形式化验证到底长什么样,是怎么做的,这是第一。当时跟ConsenSys合作发布是因为我们验证的代码,本身就是他们发布的ERC20的标准合约,我们在他们的代码基础上证他们的代码。所以,这个证明过程是完整的。当然,ERC20的合约比较简单,所以证明并不复杂,虽然不复杂,但是也有很高的门槛,对于一个程序员来说,他肯花一段时间来学习,学习完也能看懂,也会改进。
第二、我们认为ERC20是以太坊上相对非常重要的一类合约,这类合约别看很简单,也漏洞百出,我们希望合约开发者,如果他们愿意,也用形式化验证证明一下,模板拿过来直接用就可以了,安全就可以了。
有意思的是,我们做了这件事情之后,有不少做相关研究的留学生联系我们,同时也有一些国外知名团队找到我们,想要和我们合作。
这个是我挺意外的事,真正感觉到区块链跟传统的商业社会不太一样,传统的商业社会更多是竞争,但是区块链生态里面,更多是合作。大家很容易就达成一种默契,达成同一个目标。
《CoinVoice》:除了已经颇具进展的漏洞扫描工具开发和形式化证明,安比还在哪些方面拥有成熟的能力?
郭宇:我们在区块链技术上覆盖很广,很多方面都有涉猎。像密码学协议,我们做过很多相关的研究工作,像智能合约的安全语言,我们在做的过程当中发现,在区块链技术里面,有些东西只要做一些小的改进,是明显可以改善很多情况的。
所以我们就总结了很多改进现有区块链技术的点,在一些新的公链的开发过程中,我们可以把这些经验和技术输出到新的生态里面去。智能合约语言是我的专长,研究相关理论很多年,我们现在是帮一些公链改进一些关键部件、关键核心的一些东西,像智能合约虚拟机、智能合约语言,让它变得更安全。程序员不会写出来一堆Bug的合约,直接从语言层面就让它写出来就是安全的合约。
《CoinVoice》:这比帮他们挑漏洞、改错误的价值好像更大一些,让他们一开始就少犯错或者是不犯错。
郭宇:对,古话说得好,治病于未发之时,治病于微起之时。直接帮开发者写出来没有问题的合约,或者是有问题的合约很容易被发现。这样的话,项目方不需要在安全上投入太多,安全成本在降低。
|事件
生态的多样性导致工具开发有时间成本。
《CoinVoice》:2018年4月23日,美链BEC的智能合约出现整数溢出的重大漏洞,黑客通过合约的批量转账方法无限生成代币,当日,BEC的价值几乎归零。后续是否还有类似的Token合约漏洞发生?开发者应该注意些什么?
郭宇:4、5月份之后漏洞发生是越来越频繁了,而不是越来越少了,只是从媒体上看的少了。从根本上来讲,开发者最应该注意的是提高安全意识,在一些开发者眼里,写代码就是写代码,但是写区块链代码背后所承载的经济价值,跟传统的开发是不可同日而语的。
《CoinVoice》:假如说我是一名开发者,我有这个安全意识,有没有什么具体的办法避免美链BEC这类问题的产生?
郭宇:第一、找专家。找专业的团队来协助你一起检查有可能存在的安全隐患。
第三、平时多积累一些安全常识,知道合约哪些地方比较容易出问题,多学习,多跟一下最新的情况。智能合约漏洞层出不穷,有各种新型的漏洞被发现,所以开发者的知识结构要不断地更新。平时多关注我们的公众号(安比实验室SECBIT),或者是技术类的媒体。平时多看,看完之后,都会记在脑子里,自己写的时候,就会比较小心了。
第三、网上有很多免费的开源漏洞扫描工具,可以扫一遍,虽然它的准确率可能不太高,但是不管怎么样,用起来还是比人工好一些。
《CoinVoice》:智能合约的漏洞扫描工具相较于其他工具有什么特殊性?难点在哪儿?
郭宇:首先是合约很复杂,出问题的点比较多,因为它是在区块链上跑的,区块链本身是很复杂的平台,参与方有矿工、有节点,涉及到共识协议。所以,这个工具也没有那么好写。
加之,智能合约发展的太快了,很多新兴的、有实力的团队也在开发新的语言、新的技术,工具的开发远远没有跟上合约本身技术的发展,会形成一个滞后期。
现在整个区块链生态没有一个东西可以一统天下,哪怕以太坊现在做得比较大的,但是未来是不是能够一家独大,也不好说。所以,生态的多样性导致工具开发有时间成本。
《CoinVoice》:安比自己推出的智能合约漏洞扫描工具叫什么?
郭宇:阿德莱德,是澳大利亚一个城市的名字。我们团队的一个小伙伴正好在澳大利亚度假的时候,完成的这个工具的第一版。
《CoinVoice》:近期看到安比陆续发布了多篇与Fomo3D有关的文章,揭露并分析游戏的机制漏洞和原因,你如何判断合约游戏的发展趋势?
郭宇:越来越复杂化。现在的游戏越来越复杂,像最近有解谜类的,还有一些博彩类的,还有像游戏资产、管理的游戏也比较多,我相信未来会有很多很有想象力的团队,做出非常有意思的游戏出来,而且游戏代码都很长。因为要好玩,好玩就不可能简单。
《CoinVoice》:安比在智能合约游戏发展过程中,计划做些什么?
郭宇:游戏当中的逻辑漏洞是安比比较关注的点。因为游戏很有可能有后门,或者是不小心有了后门,这个东西不属于安全漏洞。只有真正理解游戏规则,你才能知道这个游戏怎么有问题,所以我们后面更关注的是游戏在逻辑上的漏洞。
它也是安全问题,但是不是一个常见的安全,像随机数漏洞这些,你只有对这个游戏理解很深入的时候,你才能知道,这个地方原来可以不用打怪就可以升级
| 自我
虽然你现在看见面前有一个巨大的坑,你在蹦,但是坑的那头是非常美好的,你就会愿意去蹦,也愿意爬出来。
《CoinVoice》:很多专家转型做创业者的时候,好像都需要一个适应的过程。
郭宇:这个感受挺深的,一开始,刚刚开始肯定是有一个不适应的过程,慢慢适应,接受现实,勇敢面对,就是这样一个过程。
《CoinVoice》:你觉得如何才能让团队充满战斗力、向心力?
郭宇:目标感非常重要。无论是之前做科研,还是现在开公司,都会经历坎坷,是一个起伏的过程,虽然你现在看见面前有一个巨大的坑,你在蹦,但是坑的那头是非常美好的,你就会愿意去蹦,也愿意爬出来。每个团队都会遇到困难的时期,只要目标在前面,你就觉得这个不算什么,你就会忘记身上的伤痛。
一个团队团结的重要原因,是每个人都愿意贡献自己的力量,这个目标就在那里,虽然路不是直的,需要走很多的路,不是那么容易,不是一天两天到达的,需要很多付出,但是只要目标在那里,都不是问题。
《CoinVoice》:除了工作以外,现在业余时间都会做些什么事情?
郭宇:没有业余时间。外界的环境变化也非常快,在变化非常快速的时代能够想清楚,是非常重要的事,所以我无时无刻都在思考。
《CoinVoice》:你有没有很钦佩的人?
郭宇:很多。
《CoinVoice》:第一时间反应出来的是谁?
郭宇:乔布斯。我在2017年的时候,把《乔布斯传》读了一遍,是无意读的,正好手头有本电子书,就翻了一下,看完之后非常感慨,他是目标非常清晰的人。
从他小时候,或者是创业开始,这个目标就定下来了。以前的电脑只有学校、企业才有,它是庞然大物,不是人日常生活当中的东西,他就是要把电脑做成电话一样,放在每个人的桌子上,这个目标始终没有变。他一直在尽力的想办法,去达到他的目标,即使中间经历那么多挫折,目标也始终没有变。
《CoinVoice》:除了《乔布斯传》外,还其它比较喜欢的书吗?
郭宇:我是一个好奇心比较强的人,看书非常杂。经常会问各行各业的朋友推荐书给我。他们推荐给我的书,不管是什么,我都会看。因为一般朋友推荐的,都是真的挺好、挺有深度的。我当时看不懂,看完之后聊一聊,从专业的角度再看看,更高屋建瓴地透析,马上对哪个领域就会有全新的认识,每次都挺激动的。
《CoinVoice》:所以你对团队也是这样要求的,让他们在很多领域都有所涉猎。
郭宇:对,我们团队的人都有这种特质,什么不会就马上迅速地学,不用成资深专家,但是自己也得懂。你反复做这个动作的时候,就不会对很多未知领域充满恐惧,反而会非常兴奋,在未知领域里面探索获得的新知识,会让他在原有的方向上获得更多的启发。
《CoinVoice》:有没有在哪一刻曾后悔创业?
郭宇:遇到困难的时候,我是会问自己。为什么创业呢?真的是好奇怪。我非常怀念之前没有创业的时候,也怀念在学校教书的时光,做科研的时光,我也特别怀念在公司熬夜干活的时光,都会怀念。
但是,如果让我回到以前,我还是会义无反顾地选择创业,而且会更早的出来创业,解决那些真正有价值的问题让人更充实!
网友评论