CertiK首席科学家:黑客永远只会对系统中更弱的一环进行攻击

栏目: 编程工具 · 发布时间: 5年前

随着加密数字货币市值的增长,区块链进入大众视野,但同时,区块链上的数字资产,也吸引了黑客的注意,把区块链当成了提款机。据 BCSEC 统计,自 2011 年到 2018 年 7 月,全球范围内因区块链安全事件造成的损失近 30 亿美元。HowMuch 在今年 6 月份,整理了区块链行业发展的这几年里,加密数字货币遭遇到的主要的黑客攻击及相应的损失金额。

CertiK首席科学家:黑客永远只会对系统中更弱的一环进行攻击

Odaily星球日报此前曾发布的《2018年区块链技术安全服务行业报告》,分析了交易所、智能合约、钱包、矿池这些业务场景对应的区块链技术安全问题。从风险事故的频发比例来看,交易平台占到 34%,智能合约占 20%。

市场的需求刺激了区块链安全公司随之的应运而生,目前来看,更侧重于智能合约安全的公司有 CertiK、 Quantstamp、Zeppelin、Runtime Verification、Solidified、Securify.ch、链安科技等;专于私钥安全存储的有库神、碧盾;要着眼于区块链整个生态系统安全的,有派盾 PeckShield、慢雾科技等。此外,还有从社区化角度切入安全领域的安全链 SECC。

其中,Odaily星球日报曾报道过的 CertiK,要通过形式化验证技术,为智能合约和区块链生态提供安全保护。

CertiK 的首席科学家 Vilhelm Sjöberg 表示,“在安全领域,黑客永远只会找系统中更弱的那一环进行攻击”。那么如何确保每个环节都很安全,就变得格外重要,但是要实现的话又有难度。

形式化验证,是根据某个或某些形式规范或属性,使用数学的方法证明其正确性或非正确性。在安全方面,如果用传统的测试方法,无法穷举所有的可能性,但是从数学的角度来看,形式化验证可以验证系统的每个环节的安全性。

据报道,目前主要运用形式化验证技术的公司,除了 CertiK,还有 Securify.ch、Runtime Verification、Tezos、The Matrix、成都链安科技等。现阶段各家公司的定位主要分三类:  VaaS 平台、公链和语言。

CertiK首席科学家:黑客永远只会对系统中更弱的一环进行攻击

图片来源:财链社

CertiK 从形式化验证这个技术方向出发,研发了深度规范、分层结构等具体技术。具体到其业务上,CertiK 通过分层结构技术,把一个要验证的复杂系统进行分层,然后通过深度规范技术,来验证是否每一层都符合正确的规范。

这次,关于智能合约为什么经常被曝漏洞,为什么形式化验证在互联网时代没有商业前景,CertiK 的技术壁垒所在,如何理解分层结构,区块链安全领域面临的最大的挑战等,Odaily星球日报采访了 CertiK 的首席科学家 Vilhelm Sjöberg 。

以下为采访原文,有删减:

Odaily星球日报: 近一年来看,智能合约经常被曝出漏洞,有人说是因为智能合约太灵活,还有人说是因为代码 copy 现象严重,您怎么看?

Vilhelm Sjöberg: 智能合约经常被曝漏洞,主要是两点原因:一个原因是代码出 bug 这个事儿是不可避免的,在互联网时代可以通过快速迭代来修复,但智能合约在部署后是无法更新的,上线的代码就需要是完美的。另一个是攻击智能合约漏洞获得的价值回报(token)高,所以会有很多人盯着你的代码找错误。 

Odaily星球日报: 相比于智能合约,对区块链底层基础设施进行验证的难度有多大?

Vilhelm Sjöberg: 区块链的底层基础设施要比智能合约本身复杂,其复杂程度主要体现在两方面:计算的复杂度(也就是代码的复杂度)、运行环境(也就是多线程)的复杂度。在证明程序正确性的时候,如果一旦这两方面复杂,那么要证明的问题就会变得复杂。而 CertiK 是目前唯一可以对复杂的计算、运行环境进行证明的公司,这是我们的价值点所在。此前对于复杂代码的多线程验证,在业界是被认为不可能实现的,前几年被我们成功进行了验证。

Odaily星球日报: 为什么形式化验证这项技术,在互联网行业或者说区块链技术变热之前,并没有多少商业前景?

Vilhelm Sjöberg: 互联网时代,虽然程序很复杂,但是对于形式化验证技术来说,并没有多少市场。如果程序有 bug,比如微信有 bug,这对用户而言并没有多少损失,而且中心化服务器端也可以将数据回滚来挽回损失。

形式化验证这项技术适合代码价值很高、不是特别复杂的程序,区块链就是用有限的代码数量来控制价值很大的东西(token)。

还可以再举个例子来明这一点,比如对安全性要求最高的或许是无人驾驶车,但是从黑客的角度来看的话,与其攻击无人驾驶车,不如攻击智能合约、钱包,得到的价值更大。

Odaily星球日报: 目前,行业里有其它安全公司在使用形式化验证技术,CertiK 在这个方向的技术壁垒是什么?

Vilhelm Sjöberg: 验证复杂度是一个很难的事情,以前一直被业界认为是不可能的。邵中教授至少花了 3 年时间,才第一个真正解决了在多线程的环境下,如何证明一个复杂系统的正确性,所以说,CertiK 本身具有先发优势。

我们通过深度规范技术,来验证了自己研发的 CertiKOS 防黑客操作系统,后来美国国防部请谷歌团队对 CertiKOS 防黑客操作系统进行攻击,但是攻击了一个月都没有成功。

此外,我们最近开发了第一代高性能智能合约自动检测引擎 CertiK AutoScanEngine(CASE),用户上传智能合约后,该引擎可以自动进行扫描并定位出漏洞。整个过程实现了最大化机器验证,对人力的依赖非常少。

Odaily星球日报: CertiK 于 2015 年提出了分层结构理论,如何理解分层结构?

Vilhelm Sjöberg: 举个例子,比如我们使用一个数字,计算机的内存是有限的,不可能表示出任何数,计算机每次碰到一个数字的时候,都需要考虑到这个数字的这样几点:数字的精度、数字的范围,有没有溢出(overflow)。如果你每次用数字时,需要重新来验证,是个没有多少意义的事情。所以,不如把整个数字的证明做成一个 layer(层)。比如整数本身在代码里是如何表征的,我们把它证明正确,直接做成一层。以后每次用整数的地方,就直接调用这一层。

具体到每一层究竟是如何的,我简单举例来说明:第一层,可能是证明整数是否在 range(范围)内的。第二层,可能是来证明加减乘除的准确性。第三层,可能就是证明乘方/开方。当然,后面还会有很多层。通过建这种模型,就可以节省大量的计算。

所以说这个技术在经验方面很重要,我们团队之前已经研发出很多层,其他人如果也想做形式化验证,需要从头开始研发,而我们已经可以基于此前的研究,来构建更多商业逻辑上的东西。

Odaily星球日报: CertiK 的商业化模式中,除了提供中心化验证服务,还有一个是去中心化的安全验证系统,这两部分如何协调?而且去中心化的安全验证系统具体指的是什么?

Vilhelm Sjöberg: 中心化验证服务主要是由我们自己先把一个复杂的系统进行分层,然后再把每一层的计算分给社区来执行,也就是交给去中心化的安全验证系统。

去中心化的安全验证系统的目标主要两个:一个是借助更多的计算资源,相比于 POW 这种没有意义的计算,我们的目标是把计算变得有意义。用户提供算力,计算出了一个证明方法,然后这个知识大家可以共享。而且整个验证过程是透明的,用户可以接入区块链,来看到整个验证过程。

另一个是希望借助整个社区的证明能力,构建一个去中心化的关于形式化证明程序方法的知识库。比如说你知道对某个程序的证明方法,但我可能是不知道的,通过借助通证经济,可以让这个证明方法被共享出来。如果是我直接花钱买了你的证明方法,这个知识实际上并没有被共享。

对于社区用户来说,我们目前在开发一整套的 工具 以降低用户门槛。社区用户可以有多个角色,你可以进来提交需要验证的程序,也可以分享计算资源,还可以定期对引擎本身进行评估等等。

Odaily星球日报: 在区块链安全领域,CertiK 对于未来的发展规划以及目前的合作进度如何?

Vilhelm Sjöberg: 智能合约这方面目前需求最大,CertiK 以智能合约为切入口,逐渐侧重于对区块链基础设施的安全,从而布局整个区块链生态系统的安全问题。

区块链基础设施的安全问题很重要,比如 Payment Channel(支付通道),如果底层的VM或者其它链本身的支付通道有问题,那么智能合约必然会有安全问题。

在合作方面,CertiK 目前主要与公链、交易所展开了合作:

公链方面,CertiK 和 NEO、星云链、Qtum量子链、本体、ICON、Waves 等项目有合作,主要负责对公链的 VM 进行安全审核。此外,我们目前也在争取与以太坊的合作。

交易所方面,CertiK 和火币、OKex、Gate、KuCoin、FCoin 等有合作,主要负责交易所上币项目的安全审计,之后还会针对交易所对安全的需求点来提供服务。此外,币安还是 CertiK 的种子轮投资者。

Odaily星球日报: 您觉得区块链安全行业面临的最大的挑战是什么?

Vilhelm Sjöberg: 最大的挑战在于工程、研究方面。工程的实现需要一个强大的团队;研究方面还有一些问题没有解决,比如有些语言的特性很复杂;开发人员依赖的工具本身(如编译器),其安全性有时也会有问题;又比如说我们目前正在运用形式化验证,来研究哪一种共识机制是最好的,是在数学上最公平的、合理的、最安全的。

Odaily星球日报: 您如何看待区块链技术面临的量子计算攻击?

Vilhelm Sjöberg: 技术方面,量子计算不会完全毁掉现在所有的加密算法,比如 POW,但是量子计算会通过更多的计算,来降低攻破它的难度。而且另一方面,研究人员也在研究,如果量子计算一旦出现,我们用什么方法来保证公钥、私钥的安全性。 其实,对于区块链来说,在技术方面并没有多少威胁,更多的可能还是政策方面。


以上就是本文的全部内容,希望对大家的学习有所帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

你的灯亮着吗?

你的灯亮着吗?

高斯 (Donald C. Gause)、温伯格 (Gerald M.Weinberg) / 俞月圆 / 人民邮电出版社 / 2014-1-1 / CNY 25.00

本书以别具一格的视角和幽默风趣的语言讨论了解决问题时有可能遇到的多种困难,并就如何训练思维能力指点迷津。本书分六个主题,每个主题都由若干生动有趣和发人深省的小故事组成,巧妙地引导读者先确认真正的问题,然后明确问题该由谁解决,再确定问题的根源,最后决定到底想不想解决这个问题。 本书适合所有业界人士以及想要探索问题解决之道的虚心读者细细品味。一起来看看 《你的灯亮着吗?》 这本书的介绍吧!

XML 在线格式化
XML 在线格式化

在线 XML 格式化压缩工具

RGB CMYK 转换工具
RGB CMYK 转换工具

RGB CMYK 互转工具

HEX CMYK 转换工具
HEX CMYK 转换工具

HEX CMYK 互转工具