6月18日，Facebook发布Libra项目白皮书，旨在建立一个简单的全球性货币且为数十亿人赋能的金融基础设施。
FacebookLibra在全球被普遍关注，金融监管者、从业者和学者纷纷从不同角度进行解读。还有很多人从哲学、学或是经济学等角度分析Libra。正如一千个人眼中有一千个哈姆雷特，一千个人心中也有一千种货币观点。
我们作为一个技术驱动的公司，更关注这次Libra发布的智能合约语言Move，这个被很多人都誉为Libra最大的创新，Move和以太坊的Solidity、以及可验证智能合约的DeepSEA语言到底有哪些区别呢？
众所周知，基于以太坊的编程语言Solidity是目前区块链领域中最常用的开发语言之一。
即使Solidity在安全性方面存在一定的缺陷，并在近几年发生了不少类似合约溢出的安全事件，并导致用户大量损失。但由于其良好的适应性和可扩展性，已被广大开发者和社区用户所积极采用。
而这次Libra携Move强势归来，便是主打的安全牌。基于Rust和100%静态类型验证的全新思路，从底层内存和智能合约编程的代码层面，来提高了安全性，以期避免发生在以太坊的安全事件。这也是这次Libra发布后，不少人都认为，Move语言才是Libra最大的创新。
但可能我们不太了解的是，由美国区块链安全公司CertiK、耶鲁大学实验室和哥伦比亚大学实验室共同研发的编程语言DeepSEA的研发也将于近期开发完成。
该语言利用植入其编程语言本身的形式化验证技术，自动创建数学原理来证明源代码的安全性，并获得了以太坊基金会、IBMBlockchain和量子链基金会的科研奖金。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检查输出的内容是否正确。
DeepSEA的设计理念是为了提供一个高于其他语言能够提供的保护层。在区块链世界中，系统具有去中心化、可自我执行、永久、开源等特性，这让哪怕是最微小的错误都有可能导致巨大且严重的问题。作为一个新时代的编程语言，DeepSEA的开发团队运用过去的经验和知识，致力于为创造一个更加安全和可信赖的区块链生态铺路。
虽然Move语言比标准编程稍稍先进一些，提供了“验证友好”的设计。但它仍旧需要创造额外的工具，这与继承了形式化验证语言本身的DeepSEA不同，DeepSEA语言允许开发者在一个交互式辅助证明工具的环境下开发自己的智能合约。
未来
综上所述，我们发现在智能合约编程语言这个底层技术支撑中，不同的安全实现方式，将会给我们的应用带来不同的安全保障。Solidity的动态灵活、应用广泛却安全性不够；Move语言的安全性提升但是还没有做到全方位的安全保障机制；DeepSEA的安全机制相对领先，但是还没有在足够多的应用上使用。
随着区块链生态环境的不断成熟，新的编程语言开始浮现，和过去几年间所发生的安全问题相抗衡。Solidity作为先行者，拥有了巨大的采用度和公众熟悉度等优势，Move和DeepSEA等新语言也紧随其后，取其精华，去其糟粕，学习其一路走来的经验，避免历史上的错误重演。
随着这三个语言的先后问世，智能合约开发者拥有了更大程度的选择自由的同时，在安全的前提下，未来的区块链世界将会变得更加丰富多彩。这值得每一个人拭目以待。
关于CertiK
CertiK公司于2017年底成立于纽约和硅谷，2019年初成立北京办公室，我们是由来自耶鲁大学和哥伦比亚大学的科研团队携数十年研究成果成立，通过形式化验证科技为智能合约和区块链应用及协议提供代码安全解决方案。团队迄今已经成功守护了价值近45亿美元的数字资产免受黑客攻击。
GeneralInformation:
Audit&Partnerships:
Website:certik.org
Twitter:@certik.org
Telegram:t.me/certik.org
Medium:medium.com/certik
币乎：bihu.com/people/1093109
原文链接点击：号称Libra最大创新的Move与Solidity、DeepSEA到底有何区别？
郑重声明： 本文版权归原作者所有， 转载文章仅为传播更多信息之目的， 如作者信息标记有误， 请第一时间联系我们修改或删除， 多谢。