Facebook 的 Libra 带来的最大创新:智能合约语言 Move

作者 | 郭立芳
出品|白话区块链(ID:hellobtc)
6 月 18 日,Facebook 高调公布了 Libra 白皮书,在全球范围内引发热议,Libra 还发布了技术白皮书,详细介绍了其新开发的智能合约语言 Move 。
Move 横空出世, 尤为吸人眼球。有人评价,这才是智能合约语言应有的模样,被很多人誉为 Libra 最大的创新。
简单地讲,比特币是对货币的编程,以太坊是对应用的编程,而 Libra 是对资产的编程,Move 就是对这门资产编程的语言。
所以,要搞懂 Move,先弄清楚什么是 Libra。
01 什么是 Libra ?
Libra 在英文中是“天秤座”的意思,天秤座象征着平衡与公正。根据 Facebook 公布的项目白皮书,Libra是“货币”和与其对应的金融基础设施的综合体,形象地讲,可以被看作同时具有支付宝和跨境支付的功能,未来的 Libra 可能具有国内支付、跨境支付、货币、证券和金融服务等一系列功能。
Libra 白皮书的技术方案中,采用的智能合约语言就是 Move ,是为操作数字资产而生的智能合约语言。李笑来对 Facebook 的 Move 语言的评价,却与众不同:Facebook 又犯傻,用得着专门设计个 Move 语言吗?
设计 Move 语言真的是多此一举吗?
现实世界的资产数字化过程中面临着两方面的困难:稀缺性和权限控制。
所谓稀缺性就是不允许用户随意复制资源;权限控制通俗地讲,就是你只能花自己的钱,不能花别人的钱,这在已有的区块链编程语言中得不到良好的支持,一旦出现问题,对于资产将是灾难性的,需要通过创建一个新的智能合约语言来解决此类问题。
这个智能合约语言之所以叫 Move ,表示区块链上的币从一个账户转移到另一个账户时,也就是实现资产的 Move,即移动,而不是简单的 Copy,这样做的好处是,杜绝了像以太坊之前出现的各种合约记账的错误与漏洞。
还有人联想,可能与 Facebook  的格言 Move Fast and Break Thing 对应,达到了一语双关的效果。
02 Move 语言有什么特点?
Move 语言的主要设计目标是灵活性、安全性和可验证性。
1、安全可靠
概括地说,Move 作为一种新的编程语言,作用是为 Libra 区块链提供安全可编程的基础。提交给 Libra 区块链的每个交易,都使用以 Move 编写的交易脚本进行编码。
简单来说,Move 有三大功能:发行数字货币、Token 和数字资产; 灵活处理区块链交易; 验证器管理。
区块链项目的智能合约语言,安全性是第一位的,不然,你被黑客攻击了 ,就等于把资产拱手送人,还拿走不谢,甚至会害用户家破人亡,所以,Move 设计的核心诉求就是安全性 。
在 Move 语言中,所有的合约执行路径都能在编译的时候确定,然后可以进行非常充分地分析、验证。Move 合约在运行前,都会被一个验证器进行校验,这个验证器可以检查出各种类型错误,而且合约执行的时候,还一边运行,一边被检查,所以,Move 合约相对安全。
2、记账不容易出错
传统的编程语言,包括以太坊智能合约语言中,对于数字资产的记账方式,是有可能出错的,因为它们就好比你们单位墙上的标语,人人都可以念,导致记账是有可能重复的。比如,过去几年里的各种记账漏洞搞得大家对智能合约的未来丧失信心。
而Move 合约采用资源类型,数字资产只能被消耗,不允许复制资源,目的是防止意外重复和丢失。就像你手上的蛋糕,吃掉一块,就少一块,这样一来,数字资产就像资源一样,不能被复制,不能凭空消失。例如某个公司搞营销活动,就可以在 Libra 中通过 Move 合约产生和验证优惠券的资产,还可以使用和转让。
3、成本更低
在 Move 语言中,一个 Token 可以被想象成一个箱子,像资源一样进行传递,且不会暴露箱子内部的任何细节,这使得运行成本更低。
03 Move 和以太坊的 Solidity 语言有哪些区别?
以太坊的 Solidity 语言,功能强大并且非常灵活,具有良好的适应性和扩展性,但它的硬伤是存在安全风险。安全问题是虚拟数字货币的基本要求,也是最大的痛点。
Move 语言,主打安全牌,针对以太坊智能合约中容易出安全漏洞的语言进行了大量的修改,额外添加了一层保护,可以避免很多 Solidity 的漏洞。
Move 语言比以太坊的智能合约语言严密,可以在编译的时候发现编程的低级错误,而不是拖到运行期才爆出漏洞,这样保证智能合约在执行中不会发生低级错误。
Move 语言会阻止代表其他用户发布数据,因此用户需要确认所发布的所有内容,使他们能够完全控制选择共享的信息。
04 小结
虽然,Move 看起来还不够细腻和成熟,但 Facebook 敢于创新,独家设计出真正适合金融应用的智能合约语言,甚至可能会成为区块链的“编程范式”的一个良好的开始。
Move 让智能合约开发者拥有了更大的选择自由,在安全的前提下,未来的区块链世界将会变得更加丰富多彩,值得每一个人拭目以待。

Facebook 的 Libra 带来的最大创新:智能合约语言 Move

作者 | 郭立芳
出品|白话区块链(ID:hellobtc)

6 月 18 日,Facebook 高调公布了 Libra 白皮书,在全球范围内引发热议,Libra 还发布了技术白皮书,详细介绍了其新开发的智能合约语言 Move 。
Move 横空出世, 尤为吸人眼球。有人评价,这才是智能合约语言应有的模样,被很多人誉为 Libra 最大的创新。
简单地讲,比特币是对货币的编程,以太坊是对应用的编程,而 Libra 是对资产的编程,Move 就是对这门资产编程的语言。
所以,要搞懂 Move,先弄清楚什么是 Libra 。

01 什么是 Libra ?

Libra 在英文中是“天秤座”的意思,天秤座象征着平衡与公正。根据 Facebook 公布的项目白皮书,Libra 是“货币”和与其对应的金融基础设施的综合体,形象地讲,可以被看作同时具有支付宝和跨境支付的功能,未来的 Libra 可能具有国内支付、跨境支付、货币、证券和金融服务等一系列功能。
Libra 白皮书的技术方案中,采用的智能合约语言就是 Move ,是为操作数字资产而生的智能合约语言。李笑来对 Facebook 的 Move 语言的评价,却与众不同:Facebook 又犯傻,用得着专门设计个 Move 语言吗?

设计 Move 语言真的是多此一举吗?

现实世界的资产数字化过程中面临着两方面的困难:稀缺性和权限控制。
所谓稀缺性就是不允许用户随意复制资源;权限控制通俗地讲,就是你只能花自己的钱,不能花别人的钱,这在已有的区块链编程语言中得不到良好的支持,一旦出现问题,对于资产将是灾难性的,需要通过创建一个新的智能合约语言来解决此类问题。
这个智能合约语言之所以叫 Move ,表示区块链上的币从一个账户转移到另一个账户时,也就是实现资产的 Move ,即移动,而不是简单的 Copy,这样做的好处是,杜绝了像以太坊之前出现的各种合约记账的错误与漏洞。

还有人联想,可能与 Facebook 的格言 Move Fast and Break Thing 对应,达到了一语双关的效果。

02 Move 语言有什么特点?

Move 语言的主要设计目标是灵活性、安全性和可验证性。

1、安全可靠
概括地说,Move 作为一种新的编程语言,作用是为 Libra 区块链提供安全可编程的基础。提交给 Libra 区块链的每个交易,都使用以 Move 编写的交易脚本进行编码。
简单来说,Move 有三大功能:发行数字货币、Token 和数字资产; 灵活处理区块链交易; 验证器管理。
区块链项目的智能合约语言,安全性是第一位的,不然,你被黑客攻击了 ,就等于把资产拱手送人,还拿走不谢,甚至会害用户家破人亡,所以,Move 设计的核心诉求就是安全性 。
在 Move 语言中,所有的合约执行路径都能在编译的时候确定,然后可以进行非常充分地分析、验证。Move 合约在运行前,都会被一个验证器进行校验,这个验证器可以检查出各种类型错误,而且合约执行的时候,还一边运行,一边被检查,所以,Move 合约相对安全。

2、记账不容易出错
传统的编程语言,包括以太坊智能合约语言中,对于数字资产的记账方式,是有可能出错的,因为它们就好比你们单位墙上的标语,人人都可以念,导致记账是有可能重复的。比如,过去几年里的各种记账漏洞搞得大家对智能合约的未来丧失信心。
而 Move 合约采用资源类型,数字资产只能被消耗,不允许复制资源,目的是防止意外重复和丢失。就像你手上的蛋糕,吃掉一块,就少一块,这样一来,数字资产就像资源一样,不能被复制,不能凭空消失。例如某个公司搞营销活动,就可以在 Libra 中通过 Move 合约产生和验证优惠券的资产,还可以使用和转让。

3、成本更低
在 Move 语言中,一个 Token 可以被想象成一个箱子,像资源一样进行传递,且不会暴露箱子内部的任何细节,这使得运行成本更低。

03 Move 和以太坊的 Solidity 语言有哪些区别?

以太坊的 Solidity 语言,功能强大并且非常灵活,具有良好的适应性和扩展性,但它的硬伤是存在安全风险。安全问题是虚拟数字货币的基本要求,也是最大的痛点。
Move 语言,主打安全牌,针对以太坊智能合约中容易出安全漏洞的语言进行了大量的修改,额外添加了一层保护,可以避免很多 Solidity 的漏洞。
Move 语言比以太坊的智能合约语言严密,可以在编译的时候发现编程的低级错误,而不是拖到运行期才爆出漏洞,这样保证智能合约在执行中不会发生低级错误。
Move 语言会阻止代表其他用户发布数据,因此用户需要确认所发布的所有内容,使他们能够完全控制选择共享的信息。

04 小结

虽然,Move 看起来还不够细腻和成熟,但 Facebook 敢于创新,独家设计出真正适合金融应用的智能合约语言,甚至可能会成为区块链的“编程范式”的一个良好的开始。
Move 让智能合约开发者拥有了更大的选择自由,在安全的前提下,未来的区块链世界将会变得更加丰富多彩,值得每一个人拭目以待。

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

众所周知,基于以太坊的编程语言 Solidity是目前区块链领域中最常用的开发语言之一。
即使 Solidity 在安全性方面存在一定的缺陷,并在近几年发生了不少类似合约溢出的安全事件,并导致用户大量损失。但由于其良好的适应性和可扩展性,已被广大开发者和社区用户所积极采用。
这次 Libra 携 Move 强势归来,便是主打的安全牌。基于 Rust 和 100%静态类型验证的全新思路,从底层内存和智能合约编程的代码层面,来提高了安全性,以期避免发生在以太坊的安全事件。这也是这次 Libra 发布后,不少人都认为,Move 语言才是 Libra 最大的创新。
但可能我们不太了解的是,由美国区块链安全公司 CertiK、耶鲁大学实验室和哥伦比亚大学实验室共同研发的编程语言 DeepSEA的研发也将于近期开发完成。
该语言利用植入其编程语言本身的形式化验证技术,自动创建数学原理来证明源代码的安全性,并获得了以太坊基金会、IBM Blockchain和量子链基金会的科研奖金。DeepSEA 语言在主打安全性的同时,也在寻求兼容除 EVM 之外的更多虚拟机,实现信息和资产的跨链共享。
今天来自CertiK 的安全专家团队对Move、Solidity、DeepSEA进行了分析比较,解释这三种编程语言之间的差异,并详细说明其中的优缺点和复杂性。
Solidity 
以太坊成功地在应用场景中引入了智能合约的概念:
当比特币将储存在区块链上的数据类型进行编码时,以太坊的用户就可以上传任意一个程序来定制该系统。与比特币相比,以太坊最大的不同点是:它可以支持更加强大的脚本语言,允许开发者在上面开发任意应用,实现任意智能合约,就是基于这个图灵完备编程语言——Solidity 用以执行这些智能合约。
在 Solidity 上发行一个应用程序其实十分的简单,它可以让用户创建一个自己的 Token(也可称为“代币”),用户可以自行持有或者将其转移至任何以太坊的账户上,也就是我们常说的发币程序。
简而言之,实现这个功能的方法只需要上传一个储存表格的程序,表中需要显示每个用户持有多少代币,并列出一些功能即可。
比如将一个账户上的代币转移至另一账户上的代码如下:
但是,在实际运行过程中,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 编译器中的例子: