• app_navCreated with Sketch.app_navCreated with Sketch.

    App

    扫码下载APP

  • tougao_navCreated with Sketch.tougao_navCreated with Sketch.

    投稿

  • Sign in_navCreated with Sketch.Sign in_navCreated with Sketch.

    登录

  • register_navCreated with Sketch.register_navCreated with Sketch.

    注册

电子科技大学副教授杨霞: 区块链安全问题及解决方案
赫伯 10-11 18:064430

在10月10日举办的区块链安全论坛上,电子科技大学副教授、链安科技CEO杨霞发表了题为《区块链安全问题及解决方案》的演讲。

电子科技大学副教授,链安科技CEO 杨霞

以下为演讲全文:

谢谢大家,我今天就抛砖引玉向大家做个汇报,把我个人作为电子科大这个角色,同时作为成都链安科技创始人的角色,我们在区块链这方面的研究情况给大家做个汇报。

这是成都链安科技自成立以来的一点成绩,就跳过去不说了,今天重点分享技术。

行业痛点,刚刚张主任也讲了很多,我们从2011-2018年,这8年时间内区块链所面临的安全事件,所造成的损失,是非常惨痛的。主要看了一下在交易平台的安全,就是我们所说的交易所的安全,还有智能合约的安全。

从张主任刚刚一个数据看智能合约的安全达到了32%,这个数字还是蛮吓人的。我个人的话我们前期重点是在做智能合约的安全,也研究了第一个就是面向智能合约的形式化验证的平台,现在我们正在做全生态的安全。

智能合约的安全这些问题有一些比较经典的,第一个安全问题也就是2016年6月西DAO系统安全漏洞,也是这个安全漏洞把我引入到区块链安全来的。之后又发生了Parity钱包还有2018年4月BEC代币,后面就是EDU和BAI。最后我再说一下Bitfinex交易所多重签名的安全漏洞,盗得12万BTC,这就是比特币黄金BTG遭受黑客51%攻击。这就是安全问题,从合约安全、交易所安全,机制本身的安全还是有很多事情要做。区块链还算比较早期,我们如何解决这些问题,安全从业人员一直在努力的探索。同时我们认为对智能合约来讲,目前缺乏开发和审计的标准,本身好多事情可以实现防止,但是为什么没有做到防止让它事后被攻击了,如果我们事先让它安全可靠了,是不是就没有漏洞可以攻击了,所以我们认为事先预防很重要。

围绕这些安全问题我们有什么解决方案?我说一下我个人的想法。区块链分四层,也是大家的共识。

存储层到协议层到扩展层到应用层,这么多层每一层安全做好的话,整个系统也就更加安全。首先来看应用层来讲,应用层DAPP去中心化的区块链应用,我们要做到它的安全只是做是不够的,我认为在开发的时候或者设计阶段就要作为安全设计再开发,在这个过程中,我们安全的DAPP就更加安全,也就是让DAPP自身更安全,漏洞更小,所以我们就是从设计开发的时候就要引入安全的理念,这样的话程序才能保障。

从扩展层来看合约,扩展层最重要的就是合约,对于合约来讲,合约自身的特点就是一旦上链是不可修改,我们这个安全问题要事先防止,实际上写出来都是代码,搞技术人眼里就是代码,怎么做到代码地安全,也是从合约的设计,合约的开发过程中处于安全理念。即使设计的时候没有考虑就做完了,做完了以后还要做安全审计,代码审计,代码审计有各种方案,还有一些其他的性能测试等等这些方法。

协议安全对共识机制、安全算法等设计、源码实现的功能正确性进行验证。有些是属于腾深问题不是说我们这个代码审核是有问题的,前段时间大家知道它最后是黑客设置到最大值,这个也是属于机制本身的问题,这些问题都是我们从机制本身的改造和机制本身的验证来完成的,这就是一把双刃剑,安全和功能往往就是矛盾的,就看你是求什么,求功能还是求安全,所以我们做安全的人经常就是在功能和安全之间两个纠结权衡。这些我们认为在各层,加上VaaS平台基于各层都有安全解决方案。我们认为需要研制一个经过形式化验证的区块链可信的“微内核”,因为区块链这个平台对我们而言,因为我们原来是做安全关键领域的,我们现在正在做一个事情就是研制一个经过形式化验证的区块链可信“微内核”,建立可信赖的区块链TCB。

重点来讲我们的合约这块,合约这是我认为比较好的方法,我们研究出来一件事的自动智能合约形式化验证平台,快速、精确自动检查智能合约存在的10大类27小类安全问题。我们在做合约设计的问题这些会经过独特的排查,看看是否存在这些问题,如果存在这些问题就要修改,我们可以事现防止这个问题出现。我们希望通过基于VaaS平台,将智能合约审计标准化、流程规范化,因为之前合约审计还是缺乏一个统一的规范和标准,各家都按照各家自己的做法,没有一个统一的方法做。另外就是流程规范化,流程没有一个统一的标准或者标准化的平台,所以这块我们觉得也是需要做好。

对交易所安全这块有这样一些方法来做,比如对交易所代码审计,还有网点测试,还有安全加固、风险亿评估,还有应急响应、合约审计、安全钱包。

当然也离不开钱包,这个会对币的事就不提,我们就是谈技术,因为我个人我做了18年的安全,对安全芯片这块我们还是有很多研究,我认为用SE芯片来做是没问题的,同时因为钱包里面还有代码,代码自身安全性也是需要保护的,所以需要在代码进行验证,这样可以让我们的钱包从软硬件的方法都做好。热钱包来讲,采用加密技术还有软硬件结合,因为是在手机上,手机上还是有很多安全方案的,我们采用了软硬件结合的隐私保护方案,保护热钱包的信息,同时现在做热钱包的工具,像智能合约已经做得非常完整了,我们准确率可以达到98%,现在我们正在做的面向热钱包的形式化验证工具,自动检测钱包程序安全,防止代码缺陷。

下面我们看一下形式化验证,如何用形式化验证方法来提高区块链的安全性。形式化验证是用数学的方法证明软件或者硬件系统它的正确性或者它的安全性,也就是说用数学逻辑的手段去推导,把代码变成数学的符号,用推导的方式证明它是否一定满足这个事情,或者它一定满足我的功能要求。所以这就是它是符合期待的,符合期待的意思就是不能有多的功能,也不能有少的功能,正好符合我想要的功能。

我们形式化验证通常有这两大类,第一类就是符号模型检测,简称符号执行,和满足性判定技术SMT实现对软件的测试和验证,判定程序路径是否存在安全缺陷,这有个问题就是在于如果代码特别大,空间会爆炸,这是它存在的问题。第二是交互式订立证明技术,使用系统描述、逻辑定理、推理规则获取形式化证据的一套体系。如Isabelle、Coq等。

业界有两派,有一派用半自动化的验证,也就是靠人工把代码进行形式化建模,这种方式对人的依赖非常高,本来形式化验证人才非常欠缺,所以这块人才非常紧缺。在这块来讲用半自动方式很难做到工业级,因此我们就是一直探索从2016年开始一直在探索面对区块链的高度策划的合约形式化验证平台。优点是无须人工参与建模,以提高自动化能力和验证效率。

因此我们推了两套工具:一是一键式全自动合约安全验证工具ASV,一种是高度自动化的合约功能验证工具ABV基于字节码。对智能合约进行军事级的自动形式化验证,防止代码安全漏洞,功能正确性。所以通过这样的我们希望能够做到把我们的验证做到自动化,减少人的参与。

这是我们的VaaS区块链生态安全系统,这些年无论是哪个品牌的智能合约,DAPP还是钱包还是底层区块链平台,这些对于我们来讲都是程序、都是代码,把这些代码导入到我们的验证平台,通过我们代码的自动建模,属性的、功能的自动建模,加上核心的创业引擎还有安全的安全规则苦库、模型库,形成审计报告、安全的ADPP、钱包、安全的区块链平台,安全的合约。

其中有一道功能是可以自动化完成,比如以合约为例,合约代码的建模完成是自动的,对常规漏洞的我们可以一键式自动检查,对功能的可以进行人工参与,对代码的全部做自动化验证,所以我们是功能、正确性、安全性全方位验证。

这是我的产品的优势,首个同时支持EOS、ETH的智能合约形式化验证平台、产品国际领先、国内第一。这是我们的一个展示,给大家分享一下,这是我们的第二版,这一版我们可以对合约的十大类20多个小类的安全问题一键式自动化查出来,准确率达到48%,误报率也非常低。近期我们会把这个平台开放一小部分功能出来,让大家免费的试用,如果有同志觉得对你的合约安全性不太放心,可以把代码打入我们这个工具,然后就一点开始审计他就可以给你定位你存在什么样的问题,并且精确定位到这个问题的位置。当你鼠标放在这儿的时候它会给你解释这是个什么问题。这个就是名字要保持一致。比如这是我们一个案例的合约,这是我们在审计代码过程中发现一个真实的合约,曾经有一个合约他找一个公司说没问题,然后拿到我们平台上就检测出他有很大的问题。

对发现的问题我们对他进行修改,再进行第二次验证,直到它变得安全通过为止。我们把平台放出来过后欢迎大家试用,大家注册就可以试用了,现在整个平台正在进行内部的测试。对发现的问题我们进行修改,修改完之后再进行第二次审计。这地方就是考虑到存在溢出漏洞,对于像这种我们是属于逻辑性的问题,我们这儿就根据它实施的溢出漏洞这个信息,我们加上把代码进行修改。这是一个转账的记录,这后面是设置验证条件,前置后置条件,来检查我们的功能是否满足。人工只需要参与这样的小部分的功能就可以了,写这样的断言就OK了,人工参与度非常低,大概10-20%。

这是一个事例,因为你自己清楚你的功能是什么,你设置断言就可以检查功能逻辑是否正确。

另外我们还做了字节码的验证工具,我为什么要做这个事,因为我们的源码是通过编译器编成字节码,可能编译器会出现错误,如何防治编译器出现错误这就是我们的工作,我们无须人工的参与,因为对源码建模就已经够难了,再对字节码进行建模实际上对于好多人来讲是非常痛苦的事情,因此我们就多了这样一个工具,能够一键式自动化的建模。而且这个建模过程严格按照以太坊的黄页,符合EVM的原理。这是我们Transfer from函数的字节码和EVM规则的形式化模型

最后是游戏合约安全分析,首发的智能合约十多个安全漏洞是我们发现的,对这里面有部分的问题,比如God.Game这个游戏,VaaS平台“一键式”自动化工具,发现该合约可被利用的安全漏洞。而且这个尤其还有问题是什么?我们发现他还存在两个后门,这个后门怎么回事大家知道,我就不方便说了,自己判断。现在区块链游戏一定要小心,我是不玩这些游戏,不敢玩。这是这个事件的分析,细节就不说了,他只输入了0.9个就盗除了这么多个。

游戏合约的有个风险汇总主要存在这几个方面:溢出漏洞、合约拥有者权限、随机数生成漏洞,还有竞态条件以及类似概念的利用。

这就是一些类型,这是以太坊的一个游戏,还有FoMo3D long漏洞。因为我不是为了做宣传,因为我们的公众号里面会每周出一个区块链安全的事件的分析,我们出的这是第13期了,这个出来的目的是便于大家写出更安全的合约,其实你们在合约的时候要注意什么样的问题,有哪些地方有坑,如何迈过这些坑,是为了帮助写出更安全的合约。谢谢大家!

相关推荐
“翻脸恒大”贾跃亭、“业余选手”张小龙
互联网企业不要争当“首富” ,而是要争当“首负”,积极纳税和创造就业,为社会谋福利。企业家要对得起社会责任和信任。
拍卖行佳士得将通过区块链记录艺术品销售
据Coindesk 10月12日报道,总部位于伦敦的佳士得正求助于区块链技术,以确保其艺术品销售和相关来源的数据安全。
8年损失12亿美元 对于智能合约漏洞 你了解多少?
10月13-14日,由DoraHacks主办的区块链安全Hackathon在北京举办,赛前,来自长亭科技、猎豹科技、链安科技等多个区块链安全公司的嘉宾围绕智能合约的安全问题带来了主题分享。