号称Libra最大创新的Move与Solidity、DeepSEA有何区别?

CertiK
企业专栏
热度: 68491
6 月 18 日,Facebook 发布 Libra 项目白皮书,旨在建立一个简单的全球性货币且为数十亿人赋能的金融基础设施。

6 月 18 日,Facebook 发布 Libra 项目白皮书,旨在建立一个简单的全球性货币且为数十亿人赋能的金融基础设施。

Facebook Libra 在全球被普遍关注,金融监管者、从业者和学者纷纷从不同角度进行解读。还有很多人从哲学、政治学或是经济学等角度分析 Libra。正如一千个人眼中有一千个哈姆雷特,一千个人心中也有一千种货币观点。

我们作为一个技术驱动的公司,更关注这次 Libra 发布的智能合约语言 Move,这个被很多人都誉为 Libra 最大的创新,Move 和以太坊的 Solidity、以及可验证智能合约的 DeepSEA 语言到底有哪些区别呢?

众所周知,基于以太坊的编程语言 Solidity 是目前区块链领域中最常用的开发语言之一。

即使 Solidity 在安全性方面存在一定的缺陷,并在近几年发生了不少类似合约溢出的安全事件,并导致用户大量损失。但由于其良好的适应性和可扩展性,已被广大开发者和社区用户所积极采用。

CertiK

而这次 Libra 携 Move 强势归来,便是主打的安全牌。基于 Rust 和 100%静态类型验证的全新思路,从底层内存和智能合约编程的代码层面,来提高了安全性,以期避免发生在以太坊的安全事件。这也是这次 Libra 发布后,不少人都认为,Move 语言才是 Libra 最大的创新

CertiK

但可能我们不太了解的是,由美国区块链安全公司 CertiK、耶鲁大学实验室和哥伦比亚大学实验室共同研发的编程语言 DeepSEA 的研发也将于近期开发完成。

该语言利用植入其编程语言本身的形式化验证技术,自动创建数学原理来证明源代码的安全性,并获得了以太坊基金会、IBM Blockchain和量子链基金会的科研奖金。DeepSEA 语言在主打安全性的同时,也在寻求兼容除 EVM 之外的更多虚拟机,实现信息和资产的跨链共享。

今天来自 CertiK 的安全专家团队对 Move、Solidity、DeepSEA 进行了分析比较,解释这三种编程语言之间的差异,并详细说明其中的优缺点和复杂性。

Solidity 

以太坊成功地在应用场景中引入了智能合约的概念:

当比特币将储存在区块链上的数据类型进行编码时,以太坊的用户就可以上传任意一个程序来定制该系统。与比特币相比,以太坊最大的不同点是:它可以支持更加强大的脚本语言,允许开发者在上面开发任意应用,实现任意智能合约,就是基于这个图灵完备编程语言——Solidity 用以执行这些智能合约

在 Solidity 上发行一个应用程序其实十分的简单,它可以让用户创建一个自己的 Token(也可称为“代币”),用户可以自行持有或者将其转移至任何以太坊的账户上,也就是我们常说的发币程序。

简而言之,实现这个功能的方法只需要上传一个储存表格的程序,表中需要显示每个用户持有多少代币,并列出一些功能即可。

比如将一个账户上的代币转移至另一账户上的代码如下:

CertiK

但是,在实际运行过程中,Solidity 的使用并没有我们想象的那么顺利。比如经常出现的整数溢出漏洞会导致 Token 无限增发、重入风险会导致智能合约遭受到类似DAO 攻击的严重损失等。

2018年4月,就有黑客利用以太坊 ERC-20 智能合约中整数溢出漏洞攻击 BEC(美链的代币“美蜜”)智能合约,成功向两个地址转出了天量级别的 BEC 代币,导致市场上大量增发的 BEC 被抛售。此事使得当日 BEC 的价值几乎归零,64 亿人民币瞬间蒸发

另一个 Solidity 可能存在的错误是在编译器中仍存在一些漏洞,这些漏洞可能会导致智能合约存在巨大的安全风险。通常程序员只查看程序的源代码,如果编译器有一个bug导致它打出的字节是错误的,这样的错误非常难以防范,即便经过了完善的人工测试和静态分析也仍然不可避免。

整体而言Solidity 是一个功能强大并且非常灵活的编程语言——但是仍旧存在安全风险。Solidity 不提供任何证明代码(或者以太坊虚拟机中的编译码)安全性的功能。因此由第三方提供智能合约代码审计、或者第三方的形式化验证是证明代码正确的最有效的方式。目前基于以太坊的智能合约应用广泛,Solidity 的安全性是值得我们重视的。

 Move 

Libra 的智能合约编程语言 Move,通过 Rust 语言固有的安全机制和 Move 语言 100%的静态类型验证等措施来达到提高安全的能力。但是经过 CertiK 的安全专家团队研究发现,与 Solidity 相比,Move 拥有以下三个重要的不同之处:

首先Move 通过省略某些特征——动态调度和一般指针——来限制语言的表达,而对语言灵活性的大规模限制可能会引发重入错误。Move的设计者表示,这些限制会让编写 Move 的形式化验证工具更加简单,但是目前这些工具并不存在,Facebook 团队表示已经充分认识到形式化验证的优势和重要性。

一个人口味最好杂一点,耳音要好一些,能多听懂几种方言。口味单调一点,耳音差一点,也不要紧,最要紧的是对生活的兴趣要广一点。

“我们将创建一种逻辑规范语言和自动形式化验证工具,利用 Move 的验证友好设计(参见第 3.4 节)。

验证工具链将有检查特定程序功能正确性的属性,这些属性超出了 Move 字节码验证器执行的安全保证(参⻅见 5.2 节)。”

——Facebook 团 队 

其次Move 支持“资源类型”(受线性类型系统启发)。模块可以定义特定类型的数据为“资源”,这意味着模块外部的任何代码都不能查看该类型值的内容:它们只能在变量之间移动并传递给函数,这虽然能够帮助 Move的开发人员确保资源得到保存,但它们还不足以确保功能的正确性——Move 设计者也同意这一点,并认为最终他们将需要使用形式化验证。

第三, 关于执行的问题:Move 的编译器会生成类型化的字节码,同时,有一个可以检查输出类型是否正确的“字节码验证器”。需要说明的是,这种“验证器”与形式化验证无关,它仅是对输出类型进行一次完整性的检查。当然,仍然可能会存在它创建类型正确但内容错误的编译器 bug。

综上而言,Libra 的 Move 语言额外添加了一层规范,可以避免很多 Solidity 的漏洞,然而这些安全性和正确性的保障仍旧是单独存在的壁垒加持。

 DeepSEA 

DeepSEA是一个将安全性放在首位的函数式编程语言,使用形式化验证对源代码进行安全保护。允许用户在高抽象的层面上对代码进行推理,实现无缝验证代码安全性的过程。

DeepSEA 编译器能够为每个程序自动输出两个重要信息:

1. 一个可执行的字节码。

2. 一个可以加载到 Coq 中的程序模型。

作为Coq的本机编程语言。由于Coq是一个完全通用的定理证明环境,因此可以与任何类型的人工编写规范相关联,除了安全性之外,也具备灵活性和兼容性。

图为将 DeepSEA 语言写到 EVM 编译器中的例子:

CertiK

与 Solidity 相比,DeepSEA 语言与 Move 类似,在程序模型上会有所限制。目前来看,在第一个版本中还未引用,所以开发团队将会用与Move 使用相同的“树状结构储存”结构(每个位置都可以在单个路径下访问),它具有与 Move 谈及的相同的“验证友好设计”

DeepSEA系统的另一个主要优势是其编译器本身是由Coq编写的,并已证明其正确性。这意味着它在基础上就与其他的系统不同。我们可以确保高级语言的语义将会保留在字节码中。这与仅检查输出类型是否正确的 Move 不同,DeepSEA 检查输出的内容是否正确(它可以满足 Coq 模型可证明的所有属性)。

DeepSEA 的设计理念是为了提供一个高于其他语言能够提供的保护层。在区块链世界中,系统具有去中心化、可自我执行、永久、开源等特性,这让哪怕是最微小的错误都有可能导致巨大且严重的问题。作为一个新时代的编程语言,DeepSEA 的开发团队运用过去的经验和知识,致力于为创造一个更加安全和可信赖的区块链生态铺路

虽然 Move 语言比标准编程稍稍先进一些,提供了“验证友好”的设计。但它仍旧需要创造额外的工具,这与继承了形式化验证语言本身的 DeepSEA 不同,DeepSEA 语言允许开发者在一个交互式辅助证明工具(Coq)的环境下开发自己的智能合约。

未来  

综上所述,我们发现在智能合约编程语言这个底层技术支撑中,不同的安全实现方式,将会给我们的应用带来不同的安全保障。Solidity的动态灵活、应用广泛却安全性不够;Move语言的安全性提升但是还没有做到全方位的安全保障机制;DeepSEA 的安全机制相对领先,但是还没有在足够多的应用上使用。

随着区块链生态环境的不断成熟,新的编程语言开始浮现,和过去几年间所发生的安全问题相抗衡。Solidity 作为先行者,拥有了巨大的采用度和公众熟悉度等优势,Move 和 DeepSEA 等新语言也紧随其后,取其精华,去其糟粕,学习其一路走来的经验,避免历史上的错误重演。

随着这三个语言的先后问世,智能合约开发者拥有了更大程度的选择自由的同时,在安全的前提下,未来的区块链世界将会变得更加丰富多彩。这值得每一个人拭目以待。

关于 CertiK

CertiK公司于2017年底成立于纽约和硅谷,2019年初成立北京办公室,我们是由来自耶鲁大学和哥伦比亚大学的科研团队携数十年研究成果成立,通过形式化验证科技为智能合约和区块链应用及协议提供代码安全解决方案。团队迄今已经成功守护了价值近45亿美元的数字资产免受黑客攻击。

General Information: info@certik.org

Audit & Partnerships: bd@certik.org

Website: certik.org

Twitter: @certik.org

Telegram: t.me/certik.org

Medium:medium.com/certik

币乎: bihu.com/people/1093109

声明:本文为入驻“火星号”作者作品,不代表火星财经官方立场。
转载请联系网页底部:内容合作栏目,邮件进行授权。授权后转载时请注明出处、作者和本文链接。 未经许可擅自转载本站文章,将追究相关法律责任,侵权必究。
提示:投资有风险,入市须谨慎,本资讯不作为投资理财建议。
免责声明:作为区块链信息平台,本站所提供的资讯信息不代表任何投资暗示,本站所发布文章仅代表个人观点,与火星财经官方立场无关。鉴于中国尚未出台数字资产相关政策及法规,请中国大陆用户谨慎进行数字货币投资。
语音技术由科大讯飞提供
推广
最近更新
本文来源:CertiK
原文标题:
24H热门新闻
暂无内容

评论0