Move语言安全性解析:智能合约语言的变革者

Move语言是一种可在实现MoveVM的区块链环境中运行的智能合约语言。它在设计之初就考虑到了区块链和智能合约的诸多安全性问题,并参考了RUST语言的安全设计。作为新一代以安全为主要特点的智能合约语言,它的安全性如何?是否能在语言层面或相关机制上规避EVM、WASM等合约虚拟机常见的安全威胁?本身是否存在特有的安全问题?

本文将从语言特性、运行机制和验证工具三个层面探讨Move语言的安全性问题。

1. Move语言的安全特性

与许多现有编程语言不同,Move语言被设计为既支持编写与不受信任代码安全交互的程序,又支持静态验证。Move具备这样的安全特性,是因为舍弃了基于灵活性考虑的非线性逻辑,不支持动态分派,也不支持递归的外部调用,而是使用泛型、全局存储、资源等概念来实现一些替代性的编程模式。例如,Move省略了动态调度和递归调用特性,这些特性在其他智能合约语言中导致了代价高昂的重入漏洞。

Move的主要安全特性包括:

1. 模块(Module):每个Move模块由一系列结构类型和过程定义组成。模块可以导入类型定义并调用在其他模块中声明的过程。

2. 结构体(Structs):可以定义为资源类型,表示可以存储在持久全局键/值存储中。

3. 过程(Function):定义了合约的业务逻辑。

4. 全局存储:允许Move程序存储持久数据,这些数据只能由拥有它的模块以编程方式读/写。

5. 不变量检查:可以定义静态检查的不变量,表示系统中资源的守恒性。

6. 字节码验证器:对字节码进行安全类型和线性化验证,强制执行资源的创建、销毁和访问规则。

通过这些特性,Move在编译时就能保证较高的安全性。接下来我们分析Move的运行机制,看看MoveVM如何保证运行时的安全性。

2. Move的运行机制

Move程序运行在虚拟机中,在运行时不能访问系统内存。这使得Move可以在不信任的环境中安全地运行,不会被破坏或滥用。

Move程序是在堆栈上执行的。全局存储被分为内存(堆)和全局变量(栈)两部分。内存是一阶存储,不能存储指向内存单元的指针。全局变量用于存储指向内存单元的指针,但索引方式与内存不同。

Move的字节码指令在栈式解释器中执行。栈式虚拟机易于实现和控制,对硬件环境要求较低,适合区块链场景。同时相对寄存器式解释器,栈式解释器在变量间进行copy和move更容易控制和检测。

Move程序运行时状态为⟨C, M, G, S⟩四元组,由调用栈(C)、内存(M)、全局变量(G)和操作数(S)组成。堆栈还维护一个函数表来解析包含函数体的指令。

调用栈包含过程执行的所有上下文信息和指令编号。执行Call指令时创建新的调用栈对象,存储调用参数,然后执行新合约指令。遇到分支指令时在过程内部进行静态跳转。这种设计避免了动态分派,加强了函数调用的不可变性,从而避免了重入的可能性。

MoveVM将数据存储和调用堆栈(过程逻辑)的存储分开,这是与EVM最大的不同。在MoveVM中,用户状态(账户地址下的资源)是独立存储的,程序调用必须符合权限和资源相关的强制规则。这种设计虽然牺牲了一定灵活性,但在安全性和执行效率上获得了很大提升。

3. Move Prover

Move Prover是一种基于推理的形式化验证工具。它使用形式化语言描述程序行为,并使用推理算法验证程序是否符合预期,帮助开发人员确保智能合约的正确性,从而减少交易风险。

Move Prover使用演绎验证算法来验证程序是否符合预期。它可以根据已知信息推断出程序的行为,并确保其与预期行为相匹配。这有助于确保程序的正确性,并减少了人工手动测试的工作量。

Move Prover的工作流程如下:

1. 接收Move源文件作为输入,该文件中需要设置程序输入规范。
2. Move Parser从源码中提取规范。
3. Move编译器将源文件编译为字节码,与规范系统共同转化为验证者对象模型。
4. 该模型被翻译成Boogie中间语言。
5. Boogie验证系统对输入进行"验证条件生成"。
6. 验证条件传入Z3求解器进行检查。
7. 如果规范成立,验证通过;否则生成诊断报告。

为描述规范系统,Move使用Move Specification Language,它是Move语言的子集,引入了对静态描述程序正确性行为的支持。Move Specification Language可以独立为专门的规约化文件,从而让业务代码和形式化验证代码分开。

Move Prover是一种非常有用的工具,可以帮助开发人员确保智能合约的正确性。它使用形式化语言描述程序行为,并使用推理算法验证程序是否符合预期。这有助于减少交易风险,让开发人员更自信地将智能合约部署到生产环境中。

4. 总结

Move语言在安全性设计上非常出色,在语言特性、虚拟机执行和安全工具层面都给出了全面的考虑。语言特性上牺牲了部分灵活性,强制类型检查和线性逻辑,方便在编译检查、形式化验证时更加自动化和具备安全可验证性。MoveVM设计将状态与逻辑分开,更贴合区块链上资产安全管理的需求。

在语言层面,Move可以有效避免EVM中常见的重入、溢出、Call/DelegateCall注入等漏洞。但鉴权、代码逻辑、大整数结构溢出等问题仍需开发者额外注意。Move Prover虽然强大,但在整体大意疏忽时可能无法发挥作用。

尽管Move语言在安全层面为程序员考虑了很多,但没有完全安全的语言和程序。建议Move智能合约开发者使用第三方安全公司审计服务,并将specification部分代码的编写和验证交由第三方安全公司完成,以进一步提高合约安全性。