Move语言安全性深度剖析：语言特性、运行机制和自动化审计

前言

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

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

1. Move语言的安全特性

编写正确的代码很困难,即使经过多次测试也无法保证代码完全没有漏洞。与不受信任的代码交互时,编写能保持关键安全属性的代码更加困难。有许多技术可以强制执行运行时安全性,如沙箱、进程隔离、对象锁等编程模式;也可以在编译时指定静态安全性,如强制静态类型或断言检查。

有时也可借助语义分析与静态分析工具,确保代码符合安全规则,即使与不受信任的代码交互时也能保持某些可证明的逻辑规约不变。

这些方案看似不错,可以避免运行时开销并提前发现安全问题。但遗憾的是,编程语言通过这些方法获得的安全性极其有限,主要有两个原因:首先,它们通常具有无法使用静态分析工具的特性,如动态分派、共享可变性和反射等非线性逻辑,违反了安全不变量规则,给黑客提供了广泛的攻击面。其次,大多数编程语言难以使用与安全相关的静态工具或表达性强的规约化语言进行扩展。尽管这两种扩展都很重要,可以预先定义。

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

为了更好地理解Move语言的特性,我们来看一个示例程序:

move module 0x1::TestCoin { use 0x1::signer;

const ADMIN: address = @0x1;

struct Coin has key, store {
    value: u64
}

struct Info has key {
    total_supply: u64
}

spec module {
    invariant forall addr: address where exists<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 0);
    move_to(account, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin acquires Info {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut<info>(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Coin { value: amount }
}

public fun value(coin: &Coin): u64 {
    coin.value
}

public fun value_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value  
}

}

a) 模块(Module):每个Move模块由一系列结构类型和过程定义组成。模块可以导入类型定义并调用其他模块中声明的过程。模块的完全限定名以存储模块代码的16字节账户地址开始。账户地址作为命名空间,用于区分同名模块。

b) 结构体(Structs):该模块定义了两个结构体Coin和Info。Coin代表分配给用户的代币,Info记录代币总量。两个结构体都被定义为资源类型,可存储在持久全局键/值存储中。

c) 过程(function):代码定义了一个初始化、一个安全过程和一个不安全过程。创建Coin前必须调用initialize过程,将单例Info值的total_supply初始化为零。signer是特殊类型,表示由Move外部逻辑验证的用户。断言确保只有指定管理员账户可调用此过程。mint过程允许管理员创建新代币,同样有访问控制。value_mut过程接受Coin的可变引用,返回指向value字段的可变引用。

合约结构上与其他智能合约语言相似,但资源类型和全局存储是Move语言中存储和资源安全的关键机制。

全局存储允许Move程序存储持久数据,这些数据只能由拥有它的模块以编程方式读写,但存储在公共账本中,其他模块的用户可查看。全局存储中的每个键由完全限定的类型名称和存储该类型值的账户地址组成。虽然全局存储在所有模块间共享,但每个模块对其声明的key具有独占的读写访问权。

声明资源类型的模块可以: • 通过move_to指令将值发布到全局存储 • 通过move_from指令从全局存储中删除值 • 通过borrow_global_mut指令获取全局存储中值的引用

模块可对其控制的全局存储强制约束。例如,确保只有ADMIN账户地址可持有Info类型结构体,通过定义initialize过程实现,该过程在Info类型上使用move_to,并强制执行在ADMIN地址上调用move_to的前置条件。

以下是两个保证该模块代码安全的静态检查特性机制:不变量规约和字节码验证器

a) 不变量检查(规约检查):模块第10行表示静态检查的不变量——系统中所有Coin对象的值字段之和必须等于存储在ADMIN地址的Info对象的total_value字段。不变量是形式化验证中的术语,表示状态的守恒性。这种守恒属性适用于模块的所有可能客户端。

b) 字节码验证器:安全类型和线性化是字节码验证器的主要验证范围。虽然其他模块不能访问由0x1::TestCoin::Coin控制的全局存储单元,但它们可以在自己的过程和结构声明中使用这种类型。

Move有字节码验证器(在字节码级别强制执行的类型系统),允许模块所有者防止不希望出现的结果。只有声明结构类型Coin的模块才可以: • 创建Coin类型的值 • "解包"Coin类型的值到其组件字段 • 通过rust风格的可变或不可变borrow获得对Coin字段的引用

验证器还强制结构默认为线性,以确保在声明结构的模块之外线性地防止复制和销毁。同时,验证器还会对一些类型的常见内存问题进行强制检查。

检测过程主要有三类:

1. 结构体合法检查:保证字节码完整性,检测错误非法引用、重复资源实体和非法类型签名等
2. 过程逻辑的语义检测:包括参数类型错误、循环索引、空索引和重复定义变量等
3. 链接时错误,非法调用内部过程,或链接声明和定义不匹配的流程

验证器首先创建CFG(控制流图),然后检测栈中被调用者的访问范围,保证合约被调用者不能访问调用者的栈空间。同时为检查类型,每个Value栈都维护对应的Type栈。

接下来是资源检查和引用检查。资源主要检查不可双花、不可销毁、必有归属等约束。引用检查结合动态和静态分析,使用类似rust类型系统的borrow checking机制。

最后是链接检查,需要对链接对象和声明是否匹配、过程的访问控制等再次检查。

2. Move的运行机制

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

其次,Move程序在堆栈上执行。全局存储分为内存(堆)和全局变量(栈)。内存是一阶存储,其单元不能存储指向内存单元的指针。全局变量用于存储指向内存单元的指针,但索引方式不同。访问全局变量时,代码提供地址和绑定到该地址的类型。这种划分简化了操作,使move语言语义更易形式化。

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

在Move中,定义为资源的值只能被破坏性移动(使之前保存该值的存储位置无效),但某些值(如整数)可以被复制。

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

调用栈包含过程执行的所有上下文信息和指令编号。执行Call指令时,创建新的调用栈对象,将调用参数存储到内存和全局变量,然后解释器执行新合约的指令。遇到分支指令时,在本过程内部发生静态跳转。模块内过程依赖无环,加上模块无动态指派,强化了执行期间函数调用的不可变性:procedure执行过程的call frame必然相邻,避免了重入可能。调用return结束调用,返回值放在栈顶。

研究MoveVM代码可见,MoveVM将数据存储和调用堆栈(过程逻辑)存储分开,这是与EVM最大的不同。在EVM中,实现ERC20 Token需在一个合约中写好逻辑并记录每个用户状态,而在MoveVM中,用户状态(账户地址下的资源)独立存储,程序调用必须符合权限和关于资源的强制性规则。这虽牺牲了一定灵活性,但在安全性和执行效率(有助于实现并发执行)上获得很大提升。

3. Move Prover

最后,我们来了解Move提供的辅助自动化审计工具Move prover。

Move Prover是基于推理的形式化验证工具。它使用形式化语言描述程序行为,并用推理算法验证程序是否符合预期,帮助开发人员确保智能合约正确性,减少交易风险。简言之,形式化验证就是用数学方法证明系统无Bug。

目前主流自动软件验证算法基于可满足性模理论求解器(SMT solver)。SMT solver实际上是公式求解器。上层软件验证算法将验证目标拆分为公式,交由SMT solver求解,根据结果进一步分析,最终报告验证目标成立或发现反例。

基本验证算法是演绎验证(deductive verification),还有其他验证算法如有界模型检测、k归纳法、谓词抽象和路径抽象等。

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

Move Prover总体架构如下:

首先,Move Prover接收含程序输入规范(specification)的Move源文件。Move Parser从源码中提取规范。Move编译器将源文件编译为字节码,与规范系统一起转化为验证者对象模型(Prover Object Model)。

该模型被翻译成Boogie中间语言。Boogie代码传入Boogie验证系统,进行"验证条件生成"。验证条件传入Z3求解器(微软研发的SMT求解器)。

VC传入Z3后,验证器检查SMT公式(程序代码是否满足specification规范)是否不可满足。若是,表示规范成立。否则,生成满足条件的模型,转换回Boogie格式发布诊断报告。诊断报告还原为类似标准编译器错误的源码级错误。

![Move安