AD
前言
6 月 18 日，Facebook 发布 Libra 项目白皮书，旨在建立一个简单的全球性货币且为数十亿人赋能的金融基础设施。Facebook Libra 在全球被普遍关注，金融监管者、从业者和学者纷纷从不同角度进行解读。还有很多人从哲学、政治学或是经济学等角度分析 Libra。正如一千个人眼中有一千个哈姆雷特，一千?心中也有一千种货币观点。我们作为一个技术驱动的公司，更关注这次 Libra 发布的智能合约语言 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 编译器中的例子：
与 Solidity 相比，DeepSEA 语言与 Move 类似，在程序模型上会有所限制。目前来看，在第一个版本中还未引用，所以开发团队将会用与Move 使用相同的“树状结构储存”结构（每个位置都可以在单个路径下访问），它具有与 Move 谈及的相同的“验证友好设计”。
DeepSEA 系统的另一个主要优势是其编译器本身是由 Coq 编写的，并已证明其正确性。这意味着它在基础上就与其他的系统?同。我们可以确保高级语言的语义将会保留在字节码中。这与仅检查输出类型是否正确的 Move ?同，DeepSEA 检查输出的内容是否正确（它可以满足 Coq 模型可证明的所有属性）。
DeepSEA 的设计理念是为?提供一个高于其他语言能够提供的保护层。在区块链世界中，系统具有去中心化、可自我执行、永久、开源等特性，这让哪怕是最微小的错误都有可能导致巨大且严重的问题。作为一个新时代的编程语言，DeepSEA 的开发团队运用过去的经验和知识，致力于为创造一个更加安全和可信赖的区块链生态铺路。
虽然 Move 语言比标准编程稍稍先进一些，提供了“验证友好”的设计。但它仍旧需要创造额外的工具，这与继承?形式化验证语言本身的 DeepSEA 不同，DeepSEA 语言允许开发者在一个交互式辅助证明工具（Coq）的环境下开发自己的智能合约。
未来
综上所述，我们发现在智能合约编程语言这个底层技术支撑中，不同的安全实现方式，将会给我们的应用带来不同的安全保障。Solidity 的动态灵活、应用广泛却安全性不够；Move 语言的安全性提升但是还没有做到全方位的安全保障机制；DeepSEA 的安全机制相对领先，但是还没有在足够多的应用上使用。
随着区块链生态环境的不断成熟，新的编程语言开始浮现，和过去几年间所发生的安全问题相抗衡。Solidity 作为先行者，拥有了巨大的采用度和公众熟悉度等优势，Move 和 DeepSEA 等新语言也紧随其后，取其精华，去其糟粕，学习其一路走来的经验，避免历史上的错误重演。
随着这三个语言的先后问世，智能合约开发者拥有了更大程度的选择自由的同时，在安全的前提下，未来的区块链世界将会变得更加丰富多彩。这值得每一个人拭目以待。
本文首发于微信公众号：硅谷密探。文章内容属作者个人观点，不代表和讯网立场。投资者据此操作，风险请自担。
