前言
Move语言是一种可编译运行在实现了MoveVM的区块链环境中的智能合约语言。其诞生之初，考虑到了诸多区块链和智能合约的安全性问题，并参考了一些RUST语言的安全设计。作为新一代以安全为主要特点的智能合约语言，其安全性究竟如何？是否在语言层面或相关机制方面可以避开常见于EVM、WASM等合约虚拟机的安全威胁？其本身是否存在特有的安全性问题？
Numen Cyber Labs 在对基于MoveVM实现智能合约的两条公链——APTOS和SUI的研究过程中, 发现了一些虚拟机层面较为底层的漏洞(https://mp.weixin.qq.com/s/IY8nj73J1oyOJ-oomDcOPg和https://mp.weixin.qq.com/s/gNGtQVVPTE2tYlshRfDhmg）并得到了官方的确认和修复。
而本篇文章将从语言特性、运行机制和验证工具三个层面尝试解答有关Move语言的安全性问题。
1、Move语言的安全特性
编写正确的代码是困难的，即使经过多次测试，我们也无法保证自己编写的代码不出漏洞。在与不受信任的代码交互时，编写能够保持关键安全属性的代码则更加困难。有许多技术可以强制执行一些运行时的安全性：如沙箱、进程隔离、对象锁等编程模式；或者，可以在编译时指定静态的安全性，如强制静态类型或断言检查。
有时，我们也可以借助语义分析与静态分析工具，以确保其代码和安全规则相一致，即确保即使在代码链接到不受信任的代码并与之交互时，在一些可证明的逻辑规约上也会保持不变。
看上去这些都是很好的方案，能够避免运行时的开销，并且提前发现安全问题。然而不幸的是，编程语言能够通过使用这些方法获得安全性极其有限，我们将其归因于两个原因。首先，他们通常具有无法使用静态分析工具的语言的特性，例如动态分派、共享可变性和反射等非线性逻辑，违反了安全不变量规则，从而给黑客们提供了广泛的攻击面。所以，大多数编程语言不能轻易地使用与安全相关的静态工具或表达性强的规约化语言（specification language）进行扩展。尽管这两种扩展都是至关重要的，可被预先定义的。
与许多现有的编程语言不同，Move语言被设计为既支持编写与不受信任的代码安全交互的程序，又支持静态验证。Move语言具备这样的安全特性，是因为舍弃了所有的基于灵活性考虑的非线性逻辑，不支持动态分派，也不支持递归的外部调用，而是使用了泛型、全局存储、资源等概念来实现一些具有替代性的编程模式。例如，Move省略的动态调度和递归调用特性，这些特性在其他智能合约语言中导致了代价高昂的重入漏洞。
为了更加了解Move语言的特性，我们看以下的示例程序：
Move中一个币资产的实现
a)模块（Module）:每个Move模块由一系列结构类型和过程定义组成。模块可以导入类型定义(例如，在第2行use 0x1::signer)并调用在其他模块中声明的过程。模块的完全限定名以存储模块代码的16字节帐户地址开始(在这里，我们编写一个帐户地址，如0x1，作为16字节十六进制地址的简写，用前导0填充)。帐户地址充当一个命名空间，用于区分具有相同名称的模块;例如，0x1::TestCoin和0x2::TestCoin是不同的模块，具有自己的类型和过程。
b) 结构体（Structs）:模块中定义了两个结构体Coin和Info。一个Coin代表分配给模块用户的代币，而Info记录了该代币总共存在多少。由声明上的has key语法可知，这两个结构体都被定义为了资源类型（具备key或store Abilities的结构体），表示这两个结构体都可以存储在持久全局键/值存储中。
c)过程（function）:代码定义了一个初始化、一个安全过程和一个不安全过程。创建任何Coin之前必须调用initialize过程，它将单例Info值的total_supply初始化为零。在这里，signer是一个特殊的类型，它表示一个由Move之外的逻辑验证的用户。断言签名者的地址等于ADMIN确保这个过程只能由指定的管理员帐户调用。过程mint允许管理员创建所需数量的新代币(第25行);这是在硬币总数更新之后(第23行)。像初始化一样，这个过程有访问控制，以确保它只能由管理员帐户调用(第20和21行)。value_mut过程接受一个对Coin的可变引用作为输入，并返回一个指向Coin值字段的可变引用。
可以看到，合约结构上和其他的智能合约语言没有太大差别，但我们需要对资源类型以及全局存储(Persistent Global Store)的概念进行更详细的解释，这是Move语言中对存储和资源安全的关键机制。
全局存储允许Move程序存储持久数据(例如，Coin余额)，这些数据只能由拥有它的模块以编程方式读/写，但也存储在公共账本中，可以由在其他模块中运行代码的用户查看。
全局存储中的每个键都由完全限定的类型名称(例如，0x1::TestCoin::Coin)和存储该类型值的帐户地址(帐户地址存储模块代码和结构数据)组成。虽然全局存储在所有模块之间共享，但每个模块都对其声明的key（账户地址）具有独占的读/写访问权。也就是说声明了资源类型(比如Coin)的模块可以:
•通过move_to指令将一个值发布到全局存储(例如，第14行);
•通过move_from指令从全局存储中删除一个值;
•通过borrow_global_mut指令获取全局存储中一个值的引用(例如，第22行)。
由于模块“拥有”由其通过key控制的全局存储条目，它可以对该存储强制约束。例如，确保只有ADMIN帐户地址可以持有类型为0x1::TestCoin::Info的结构体。它只通过定义一个过程(initialize)来实现这一点，该过程在Info类型上使用move_to，并强制执行在ADMIN地址上调用move_to的前置条件(第13行)。这些约束不同于静态不变量，因为它们需要运行时检查。在这种情况下，由于参数account是在运行时提供的，程序员不能静态地强制它始终是ADMIN的，因此需要在第13行进行不变量检查。
以下就是两个保证该模块代码安全的两个静态检查特性机制：不变量规约和字节码验证器
a)不变量检查（规约检查）:模块的第10行，表示静态检查的不变量——系统中所有Coin对象的值字段之和必须等于存储在ADMIN地址的Info对象的total_value字段。所谓不变量，是形式化验证中的一个术语，表示了一种状态的守恒性，也可以称为不变式或不变性。我们希望守恒属性适用于模块的所有可能的客户端(包括恶意的客户端):任何违反都会破坏Coin的完整性。因此，不变式不只是影响单个对象，而是影响它们的集合(即所有的Coin对象)。该处其实就是我们下一节要介绍的move prover中可用于形式化检查的specification language。
b)字节码验证器:安全类型和线性化是字节码验证器的主要验证范围: 如本例，尽管其他模块不能访问由0x1::TestCoin::Coin 控制的全局存储单元，但它们可以在自己的过程和结构声明中使用这种类型。例如，另一个模块可以公开一个支付过程，该过程接受0x1::TestCoin::Coin作为输入。
乍一看，允许Coin等敏感值流出创建它们的模块可能看起来很危险——恶意客户端模块会创建假冒硬币，人为增加其拥有的硬币的价值，或复制/销毁现有硬币。幸运的是，Move有一个字节码验证器(一个在字节码级别强制执行的类型系统)，它允许模块所有者防止这些不希望出现的结果。只有声明了结构类型Coin的模块才可以:
•创建一个Coin类型的值(例如，第25行);
•“解包”一个Coin类型的值到它的组件字段中(在本例中为value);
•通过rust风格的可变或不可变borrow(例如&mut Coin)获得对Coin字段的引用。
这允许模块作者在模块中声明的结构的创建值和字段值。验证器还强制结构默认为线性。以确保线性地防止在声明结构的模块之外复制和销毁(例如，通过覆盖存储结构的变量或允许它超出作用域)。同时，验证器还会对一些类型的常见内存问题（如溢出）进行强制检查。
检测过程主要有三类：
1）结构体合法检查：保证字节码的完整性, 检测错误非法的引用，重复的资源实体以及非法的类型签名等
2）过程逻辑的语义检测：包括参数类型错误，循环索引，空索引以及重复定义变量等。
3）链接时错误，非法调用内部过程，或者链接一个声明和定义不匹配的流程。
验证器会首先创建一个CFG（Control-flow Graph，控制流图），因为没有非线性逻辑，这个控制流图可以清晰的描述程序块间的调用关系，而无需考虑递归深度的问题。
随后，验证器会检测栈里面被调用者的访问范围，保证合约的被调用者不能访问到调用者的栈空间。例如一个过程被执行的时候，调用者首先在CallStackFrame里面初始化局部变量，然后将局部变量放入到栈里面，假设当前栈的高度是n，那么有效的bytecode必须满足不变量：当调用过程结束的时候，栈的高度依然还是n。验证器主要是通过分析每个指令块的指令对栈的可能影响，保证不操作高度高于n的栈空间。这里有一个例外就是，一个以return结尾的指令块，他退出的时候高度必须是n+m，其中m是过程返回值的个数。
同时为了检查类型，每一个Value 栈都维护了一个对应的Type 栈，执行的时候Type栈也跟这指令执行进行pop和push。
接下来是资源检查和引用检查。资源主要检查资源的不可双花、不可销毁、必有归属（返回值必须被接受）等约束。而引用检查结合了动态和静态分析。静态分析利用类似rust类型系统的borrow checking机制，保证：1. 所有引用必须指向一个已经被分配的存储上，防止空指针；2. 所有的引用都有安全的读写权限。
而borrow_global调用的时候会动态的对全局变量的引用进行了计数，解释器会对每个发布了的资源进行判断，如果被borrow或者move了，再次引用就会报错。
最后是链接检查，需要对链接的对象和声明是否匹配，过程的访问控制等做再次的检查。
可见，通过不变量检查和字节码验证器两种机制，双重保障了代码在编译时的安全性。接下来我们通过分析move的运行机制，来看看MoveVM如何保证运行时的安全性。
2、Move的运行机制
首先，Move程序运行在虚拟机中，并且在运行时不能访问系统内存。这使得Move可以在不信任的环境中安全地运行，并且不会被破坏或滥用。
其次，Move程序是在堆栈上执行的，形式上，之前提到的全局存储被分为两部分:内存（堆）和全局变量（栈）。内存是一个一阶存储，因此它的单元不能用来存储指向内存单元的指针。全局变量被用来存储指向内存单元的指针，但是它们的索引方式与内存不同。为了访问全局变量，代码提供了一个地址和一个绑定到该地址的类型。这种划分简化了操作，使得move语言在语义上更容易形式化。
而Move的字节码指令在一个栈式的解释器进行执行，栈式虚拟机的好处是易于实现和控制，对硬件环境的要求较少，非常适合区块链场景。同时相对寄存器式的解释器, 栈式解释器在不同的变量之间进行copy和move更容易控制和检测。
在Move语言中，任何被定义为资源的值都只能被破坏性地移动(使以前保存该值的存储位置无效)，但只有某些值(例如，整数)可以被复制。
Move程序运行在堆栈上的时候，其状态为⟨C, M, G, S⟩的四元组，由:调用栈（C），内存（M），全局变量（G）和操作数（S）组成。堆栈还维护一个函数表(模块本身)来解析包含函数体的指令。
调用栈包含了一个过程执行的所有上下文信息以及指令编号（指令会被唯一编码，减少代码体积）。当在一个过程中执行Call指令调用其他的过程的时候，会创建一个新的调用栈对象，然后将对应的调用参数存储到内存和全局变量上面，最后解释器开始以此执行新的合约的指令。执行过程遇到分支指令的时候，会在本过程内部发生一个静态跳转，所谓静态跳转实际上是指跳转的offset是事先已经确定好的，不会像evm一样动态跳转。这也就是之前提到的不支持动态分派的特性。也就是说模块内的过程依赖是无环的，加上模块本身的没有动态指派，这样就加强了执行期间的函数调用的不可变性：一个procedure在执行过程的call frame必然是相邻的，从而避免了重入的可能性。最后调用return结束调用，同时返回值放在栈顶。
通过研究MoveVM的代码，我们可以清晰的看到，MoveVM将数据的存储和调用堆栈（过程逻辑）的存储是分开的，这点是和EVM最大的不同的地方，例如，在EVM中，要实现一个ERC20的Token，需要在一个合约中写好逻辑和对每个用户的状态进行记录，而在MoveVM中，用户状态（账户地址下的资源）是独立存储的，程序调用必须符合权限和关于资源的强制性规则，虽然牺牲了一定的灵活性，但是在安全性和执行效率（有助于实现并发执行）上获得了很大的提升。
3、Move Prover
最后，我们来了解下Move提供的能够进行辅助自动化审计的工具Move prover。
Move Prover是一种基于推理的形式化验证工具。它使用形式化语言来描述程序的行为，并使用推理算法来验证程序是否符合预期，可以帮助开发人员确保智能合约的正确性，从而减少交易风险。简单来说，形式化验证就是用数学方法去证明我们的系统是无 Bug 的。
目前主流的自动软件验证算法是基于可满足性模理论求解器（SMT solver, satisfiability module theories solver）的。虽然这名字看起来有点唬人，但其实 SMT solver 就是一个公式求解器。上层的软件验证算法将其验证目标拆分为一些公式，交由 SMT solver 求解，再根据求出的结果进一步分析，最终报告验证目标成立，或者是发现了一个反例。
一种基本的验证算法是演绎验证（deductive verification），也有不少其他的验证算法，比如有界模型检测、k 归纳法、谓词抽象和路径抽象等
Move Prover就是使用了演绎验证算法来验证程序是否符合预期。这意味着，Move Prover可以根据已知的信息推断出程序的行为，并确保其与预期的行为相匹配。这有助于确保程序的正确性，并减少了人工手动测试的工作量。
Move Prover的总体架构如下图所示：
首先，Move Prover 接收一个Move源文件作为输入，该文件中需要设置程序输入规范（specification）。之后 Move Parser 会在源码中把规范提取出来。Move 编译器将源文件编译为字节码，和规范系统(specification)共同转化为验证者对象模型(Prover Object Model)。
这个模型会被翻译成一种名为Boogie的中间语言。这段 Boogie 代码会被传入 Boogie 验证系统，该系统对输入进行“验证条件生成”(verification condition generation)。该验证条件会被传入一个名为 Z3 的求解器中，这是微软研发的一种可满足性理论（SMT）求解器。
VC 被传进 Z3 程序后，该验证器会检查 SMT公式（程序代码是否满足specification规范）是否是不可满足的。如果是这样，这意味着规范是成立的。否则，将生成一个满足条件的模型，并将其转换回Boogie格式，以便发布诊断报告。然后将诊断报告还原为与标准编译器错误类似的源码级错误。
为了描述规范系统，move使用Move Specification Language，其是Move语言的子集，它引入了对静态描述有关程序正确性的行为的支持，而不影响生产。同时可以独立为专门的规约化文件，从而让业务代码和形式化验证代码分开。
网上已经有很多其他的关于Move Specification Language的教程，感兴趣的可以自行学习，建议合约程序员们多加了解，以提高自己代码的安全性。同时，由于Move Specification Language可以不侵入代码的单独编写，对于安全性要求更高的项目来说，可以将该规约代码交由安全经验更加丰富的第三方安全公司来撰写，在审计代码的同时，可以给出更严格的形式化验证报告。
总的来说，Move Prover是一种非常有用的工具，可以帮助开发人员确保智能合约的正确性。它使用形式化语言来描述程序的行为，并使用推理算法来验证程序是否符合预期。这有助于减少交易风险，并使开发人员能够更自信地将智能合约部署到生产环境中。
4、总结
Move语言的设计在安全性的考虑上非常出色，在语言特性、虚拟机执行和安全工具层面，都给出了非常全面的考虑。语言特性上牺牲了部分灵活性，强制类型检查和线性逻辑，方便在编译检查、形式化验证时更加的自动化和具备安全可验证性，而MoveVM在设计上将状态与逻辑分开，更加贴合区块链上资产安全管理的需求。
综上，在语言层面，常见于EVM的重入、溢出、Call/DelegateCall注入等漏洞可以有效避免，但是鉴权、代码逻辑、大整数结构溢出（最新的move语言版本已经支持u256，如使用官方u256类型不会产生溢出漏洞）等问题并不能依赖语言层面的特性去避免，而Move Prover并不能在整体的大意疏忽时产生作用。
虽然Move语言在安全层面已经为程序员考虑了很多，但没有完全安全的语言，也没有完全安全的程序。我们仍然建议，Move智能合约的开发者使用第三方安全公司审计服务，并且将specification部分代码的编写和验证交由第三方安全公司来完成。
