请选择 进入手机版 | 继续访问电脑版

币仑财经-区块链社区媒体

【技术开放日】链安科技杨霞:智能合约安全问题及自动形式化验证平台VaaS

2018-10-15 13:43| 发布者: 币仑| 查看: 360| 评论: 0

摘要: 本文整理自2018上海区块链国际周-技术开放日演讲嘉宾电子科技大学副教授、成都链安科技创始人兼CEO杨霞的演讲内容。杨霞在演讲白帽安全团队就像辛勤的啄木鸟一样对每一棵树进行安全检查,看看有没有虫子。从事安全领 ...
本文整理自2018上海区块链国际周-技术开放日演讲嘉宾电子科技大学副教授、成都链安科技创始人兼CEO杨霞的演讲内容。

杨霞在演讲


白帽安全团队就像辛勤的啄木鸟一样对每一棵树进行安全检查,看看有没有虫子。从事安全领域的这18年,我都一直努力地让系统自身更"健康",专注做"盾"。在研究形式化验证方法之外,我还尝试过TEE。我是全球最早做TEE安全操作系统的团队之一,深度隔离的双Android系统也是我尝试保护移动终端隐私的系统解决方案。我还做过内核安全架构和用户权限控制等。而形式化验证,是我认为更有效的提高系统安全性的方法。


2016年,以太坊第一个漏洞“Dao”系统的漏洞,导致了硬分叉的安全问题,由此我们的目光转向区块链安全。我是最早将形式化验证方法应用于智能合约安全的研究者之一,在此之前我一直在给航空、航天、军事等领域提供形式化验证服务。形式化验证的方法,大家以前听的非常少,因为它是非常冷门也非常小众的研究领域,主要用于确保航空、航天、军事等尖端的安全控制系统的安全性。


链安科技是分布式资本旗下唯一从事区块链安全的公司。我们入选工信部《2018区块链白皮书》,我们研发了全球第一个同时支持EOS和以太坊智能合约形式化验证平台VaaS。我们也是首批进入Etherscan智能合约安全审计推荐名单的区块链安全公司,并且获得OKEX的“最佳安全审计合作伙伴”称号。近期我们也会发布Vaas2.0平台,提供合约源码到字节码的完备形式化验证,并且我们对合约常规漏洞检查的准确率达到95%以上。


说到区块链的安全问题,智能合约的作用和价值大家都非常清楚,为什么智能合约出的安全问题是很难弥补的呢?因为智能合约的不可篡改性使其一旦部署上链就不能修改。很多项目要求我们只出报告,因为他们觉得自己的项目没有安全问题。但是经过我们的严格审计,结果表明80%智能合约都存在安全问题。


已经上链的合约出现问题怎么办呢?只能重新部署一个新合约再做迁移。而有些项目方在部署上链之前就让专业的审计单位对合约进行安全审计,是非常明智的做法。我们在审计合约安全时,采用的“形式化”方式,用数学的方法证明合约是否存在或不存在安全漏洞,并且代码实现是否满足用户的期待。安全审计工作花不了多少钱,但是对项目方的品牌形象和资产保护却是非常有意义的。


BEC合约由于一行代码的漏洞导致64亿人民币一夜归零。还有最近比较火爆的游戏合约,也大多数存在安全问题。我们的VaaS平台,刚发现Gorgona游戏合约存在后门,Owner可卷走所有资产。总之,智能合约的安全问题不容乐观,所以需要引起大家的高度重视。


目前,智能合约安全事件已经导致了至少13亿美元的损失。如何解决安全问题?目前安全公司常见的几类方法,如动态分析、静态分析、形式化验证、人工漏洞复查、人工审核。


形式化验证是什么?形式化验证是根据某些规范、属性使用数学的方法证明“其”(软件系统、硬件系统)正确性。形式化验证是系统性的过程,将使用数学推理来验证设计意图是否符合用户期待的功能需求。如何使合约的程序正确地满足期待的目标同时没有安全问题?需要验证两个东西:1.安全属性的满足性;2.功能正确性。这两个满足了,那系统就更健康了,“虫子”就更少了。


如果要证明X系统,X可以是某个软件或硬件系统。证明X做的事情正好如用户期待,不多也不少。怎么做到呢?首先要对系统设计与实现分别进行形式化建模,然后再证明是其是否“正确”地满足用户的“期待”。


有人问这和测试有什么区别?测试只能测出来有哪些Bug,但是测完以后放心吗?不能,因为测试只能显示已有的Bug,不能显示Bug一定不存在。只能说测出来Bug知道它有这些,但还有一些不存在的Bug显示不出来。形式化验证是通过数学推理的方式保证一定不存在指定属性的安全问题、或者一定存在指定安全属性的问题,并且同时满足功能正确性。这套方法最早用在航空、航天等安全关键领域,国际标准(CC标准)的EL5之上都要求形式化验证,我个人也参与了一些CC安全标准的一些工作。


区块链系统是大量的资金交易系统,资金交易里关键程序一旦出了问题,后果是无法挽回的,所以形式化验证天生就适合于区块链安全保障。我们努力尝试,将形式化验证更加适合于工业应用、更加的自动化。因此,我们研发了一套面向智能合约的高度自动化的形式化验证平台,起名VaaS。希望通过这套验证平台将智能合约审计标准化、规范化。目前智能合约审计还缺少标准化的平台,在这一块儿还有很多工作要做,希望我们公司能够在这里面做更多的事情。


VaaS形式化验证为智能合约提供严格的“军事级“验证,防止代码的安全漏洞的同时,确保代码的功能正确性,让代码能够正确地实现用户的需求。为了达到此目标,我们研发了两套产品:1.“一键式”全自动化智能合约安全审计工具;2. 合约字节码的形式化验证方式。编译器可能会引入错误,如何防止编译器引入的错误呢?如何证明编译器自身是安全的?怎么放心编译器编译出来的代码是没有问题的?最好的做法就是面向字节码的形式化验证。


为了尽量地提供代码的自动化验证能力,我们对代码进行自动化建模,无需任何人工参与。去年我们已经做了一个高度自动化的形式化验证原型系统,今年我们将其实现产品化。但是对与某些复杂的逻辑功能验证,还是需要部分人工地参与。而传统人工建模的方式存在一个很大的问题,无论模型多么漂亮结果多么美好,代码稍微一改,模型全部要重新做。


我们VaaS产品的优势:安全属性、功能正确性全方位地验证,源码和字节码完备的形式化验证。我们也是全球第一个同时支持EOS、ETH的自动形式化验证平台。并且,在区块链程序设计便引入形式化验证的理念,从设计、开发多纬度的验证,保障智能合约等区块链关键程序的安全性。

形式化验证的依据是什么呢?分享一下我们常用的基本数理逻辑——霍尔逻辑。要证明代码C是否可行,定义在执行“C”之前的前置条件为P,执行“C”之后的后置条件为Q。前置条件“P”如果为真,那“Q”在执行“C”之后也应该为真,也就说说代码“C”不会把系统引入到一种不正确的状态,那么可以说明“C”是正确的。


以Transfer函数为例,这是在以太网里非常重要的转账函数。通过VaaS转化成形式化语言,这部分完全无需人工参与。对执行Transfer之前的系统状态进行形式化描述,如何判断执行之后的结果是否符合预期呢?需要对用户期待的目标进行形式化描述。以Transfer函数来讲,转账地址不为零,转帐数额不能超过转帐方拥有的数额等条件下,期待的目标是转账方balance减少余额和被转帐方增加的余额要一致。


目前,链安科技已经为超过30家的区块链公司提供安全服务,如本体、IoTeX、比原、布比、云象等。我们近期还做了安全漏洞的相关连载,每周一期讨论一个非常有趣的安全话题,目标是让大家写出更加安全的智能合约程序,保护用户的资产。为区块链做好安全的“盾”,“让区块链更安全”是我们的愿景!


鲜花

握手

雷人

路过

鸡蛋

最新评论

Powered by 币仑

© 2017-2018 币仑 Inc.

返回顶部