链安科技杨霞:被用于导弹控制的形式化验证,进军区块链安全区块链

qinjiayuan  | 08月1日, 2018 2018-08-01 22:15
分享到:
导读

自2009年中本聪发布了《Bitcoin:A Peer-to-Peer -Eletronic System》论文后,区块链的概念就逐渐在社会中普及开来。近年来随着社会各界...

自2009年中本聪发布了《Bitcoin:A Peer-to-Peer -Eletronic System》论文后,区块链的概念就逐渐在社会中普及开来。近年来随着社会各界关注度的日益提高,区块链技术的发展更是突飞猛进。

在早期,被称为区块链1.0的比特币,它的代码和结构体系是简单的,这也是它能健康运行直到现在的重要原因。而随着行业发展,越来越多的技术被运用于区块链技术。不仅被称为区块链2.0的以太坊,区块链3.0的EOS等主链依次上线,市面上种类繁多的项目更是让人目不暇接。

野蛮生长虽然对区块链技术的发展是一种好事,但与之相伴相生的区块链安全问题也日益严重。

远至以太坊DAO,mtgox被黑客攻击,近至NiceHash事件,Tether黑客事件。各种对区块链技术或者数字货币的安全漏洞事件层出不穷。根据区块链安全公司CipherTrace报告,仅仅2018年上半年,黑客就窃取了价值7.31亿美元的加密数字货币。

安全问题从来都是不可忽略的,每个行业的发展都需要一些专注于安全的公司。近日,耳朵财经(微信公众号ID:erduocaijing)采访了国内首家专注于区块链安全的公司—链安科技。

很多时候,一个新兴行业的发展需要来自其他成熟行业的支持,无论是技术也好、人才也好。

最近,区块链圈内新出现了一家专注于智能合约安全的公司,叫做链安,它是国内首家专门从事区块链安全的公司。由来自成都电子科技大学的杨霞教授和她的技术团队所创立,目前已经与国内十多家区块链行业的知名公司,如火币、OKex、KuCoin等建立了长期的战略合作。

链安科技的创始人杨霞,作为形式化验证的专家,曾经为大型航空航天项目的形式化验证服务,主持过国家核高基,装发重大软件等近10项国家重大课题,发表学术论文30多篇,申请20多项专利。

2016年以太坊发生了第一个安全漏洞事件。当时以太坊被爆出the DAO漏洞,这个漏洞使得攻击者可以将theDAO资产池中的以太币非法转移给自己。杨霞在区块链行业的一个朋友顿时想到了她在安全领域中建树颇丰,认为如果杨教授如果能来做区块链方面的安全研究一定能获得一些成功。

“目前从数据上看,市面上起码80%的智能合约都或多或少存在着安全问题”,杨霞说“往往几行代码的错误就会造成数十亿的损失,这带来的教训是十分惨痛的”。

杨霞对区块链技术当前的安全性是不满意的。

于是从2016年下半年开始,那么为了保证区块链代码的安全,杨霞就听从了朋友的建议。开始了对区块链的研究,将自己在形式化验证方面的成果,运用到了区块链方面。

这种形式化验证,相较传统审计代码方法,具有更高效,更安全的特点。它本身主要用于航空航天,军事安全等领域中,之前更多的实际应用是导弹控制,战斗机导航等对安全性和正确性要求比较高的系统之中。

形式化验证,简单的说,就是用数学工具进行验证的方法,把代码编成数学模型,从设计到实现整个流程,通过证明手段来证明代码是完备安全的,能够满足期待。

因此,将它运用在区块链智能合约中是非常合适的。这种先进的科技理念和技术指导,是其他行业对区块链发展的强大动力。

众所周知,和传统的互联网技术不同,智能合约一旦写定上链后,后续出现问题则是无法更改的。这是区块链技术的特点也是对区块链安全技术发展的挑战。

这对代码的测试就有了很高的要求,在杨霞看来,和传统测试不同的是,区块链项目的测试需要的科技含量更高。传统测试无论是白盒测试、黑盒测试,往往都需要穷尽bug。而限于人力,测试往往不能覆盖所有可能产生的问题,这种测试方式在区块链行业是很容易忽略致命的漏洞,一旦漏洞出现,又无法修复,带来的损失将会是巨大的。

针对智能合约的安全问题,链安科技研发的VaaS平台,采用了形式化验证的形式,用数学的手段来证明代码,给智能合约提供军事化级别的安全保护,杜绝逻辑漏洞和安全漏洞,确保系统安全性。

“减少人工干预,更多的工作被机器完成”也是智能合约安全需要被强调的。

VaaS所提供的服务,具有快速支持多平台的能力,近期VaaS的重点虽然是专注于为EOS提供全面的形式化验证服务,但是未来,VaaS平台也将逐步支持其他主流区块链平台的形式化验证工作。

在聊到区块链这个大行业整体的当前的创业氛围时,杨霞认为,虽然现在有不少人借用区块链技术来作恶,但这是一个社会问题。无论哪种技术在发展的时候都是无法避免的。区块链本身依然是一个很伟大的创新。

比如最近风靡的某个区块链游戏,在杨霞看来,这种类型的传销游戏并不是一种好的现象,对区块链的发展不会起到促进的作用。虽然它的本意是讽刺目前币圈的一些骗局。但是大家在看到它火了之后反而去争相模仿,这在信息传播急速的现代社会是会产生不良影响的项目。

当然除了这些利用人性,利用区块链为噱头的骗局之外,在区块链基础之上的一些技术的发展可以对整个行业是会起到促进作用,链安科技所提供的智能合约审计服务就是其中一个典范。

随着各种规范的完善,代码错误率降低,程序的漏洞减少,黑客攻击的成本增加难度加大。数字货币的价值最终也会越来越稳定,市场也会越来越成熟。

但这都是依靠在越来越多像链安这样,从技术服务角度,为区块链产业的发展贡献出自己一份力量的基础上。

 

区块 安全 技术 发展 代码
分享到:

1.TMT观察网遵循行业规范,任何转载的稿件都会明确标注作者和来源;
2.TMT观察网的原创文章,请转载时务必注明文章作者和"来源:TMT观察网",不尊重原创的行为TMT观察网或将追究责任;
3.作者投稿可能会经TMT观察网编辑修改或补充。


专题报道