资助金额：200 usdt
Bounty链接：Hacker Dōjo|课题研究：Move Prover | Bounties | DoraHacks
创作者：0x7ac61a
本项目由Hacker Dōjo资助，文章转载请联系
Telegram: @HackerDojo0
WeChat: @HackerDojo0
Move语言介绍
Move语言是最早被用在Libra blockchain上，现在主要用于Aptos与Sui链，Sui还对Move语言做了一些个性化的修改。Move Prover是Move语言的形式化验证语言，开发者可以通过编写一些specification来形式化地对程序进行验证。Move Prover的存在源于Move语言设计的几个优势：
- Move语言在被设计之初就考虑了支持形式化验证
- Move语言在设计开始就有书写specification的文化（Libra blockchain上的Move module都在编写spec模块）
- Move Prover在不断改进，目标是被设计成一个准确、快速、用户友好的prover。
Global Storage
Move 的全局存储是由地址（address）索引的，每个地址下都有 Move 模块和 Move 资源。账户下的存储结构是BTreeMap，通过不同的key来存储不同的值。Move语言中提供了五种访问全局存储的方法。
Move语言
Move有两种程序类型：Modules和Scripts。
- Modules：模块是定义结构类型以及对这些类型进行操作的函数的库（可以理解为合约），模块本身也存储在全局存储中。模块中结构类型定义了 Move全局存储的模式，模块函数定义了更新存储的规则。从语法结构看Move语言的模块包含了五种元素，分别是use、friend、type、function和constant。
编译这个程序产生的字节码：
在Move中定义了五种对全局存储进行访问的方法，除非是Move module中的声明，否则不能在全局存储中创建、修改、销毁内容：
- Scripts：是链下编写的，编译成bytecode后随交易一起执行的脚本，script不会被存储在链上，在script中可以直接调用module中的方法。
运行script可以调用module中的function：
Ability是 Move 语言中的一种类型特性，用于控制对给定类型的值允许哪些操作。这种通过能力的控制是通过控制对某些字节码指令的访问来实现的，因此对于要与字节码指令一起使用的值，它必须具有所需的能力（并非每条指令都由能力控制）。
- copy：允许此类型的值被复制
- drop：允许此类型的值被弹出/丢弃，没有话表示必须在函数结束之前将这个值销毁或者转移出去。
- store：允许此类型的值存在于全局存储中或者某个结构体中
- key：允许此类型作为全局存储中的键（类型名会作为key，结构体的值会作为value）
Move语言安全约束
Move的类型系统在编译时对语言进行了一些安全限制，Move的bytecode verifier保证了：
- 程序和结构声明的类型良好
- 依赖的模块和程序是存在的（静态链接）
- 模块的依赖性是无环的
- 每个基本块的开始和结束时，操作数栈的高度都是一样的
- 一个程序只能通过传递给被调用者的引用来接触属于调用者的堆栈
- 全局和局部内存总是树形的
- 不存在悬空的引用
- 可变引用对其引用者有独占访问权
变量与类型
Move是静态语言，类型可以在编译时由Move编译器进行推断，或者显示的标注出来。在Move中除非是生成一个新的变量的类型转换（使用as），否则一个变量有且仅有一种类型。
Move中的局部变量可以通过两种方式使用，move或copy，如果未指定其中之一，Move编译器能够推断应该使用copy还是move。在move发生之后先前的局部变量会变得不可用。Move 编译器将推断一个copy或move是否未指示：
- 复制任何具有copy能力的标量值都被赋予一个copy
- 任何引用（可变的&mut和不可变&的）都被赋予一个copy
- 除此之外的其他任何其他值会被视为move。
Resource
Move中在定义struct的时候，可以有四种能力进行选择（key、copy、store、drop），coin只有store功能但是无drop能力，外部module/script可以将coin对象进行存储，但是不能将coin对象直接销毁。
struct Coin has store { /// Amount of coin this address has. value: u64, }
比如只写下面这个函数，当试图传入一种资源但是并没有返回时，该资源需要拥有drop能力：
fun test_ref(coin:Coin){ }
字节码验证器会捕捉这个错误：
引用
Move中不存在空悬指针，这一点是由Move类型系统保证的。例如下面这个例子，join过程接受两个参数：&mut LibraCoin::T类型的coin（一个存储在其他地方的LibraCoin::T值的可变引用）和to_consume类型的LibraCoin::T（一个拥有的LibraCoin::T值）。
如果c_value_ref是对to_consume的引用，在类似C语言中，第一行将使c_value_ref成为一个悬空的引用，而Move的字节码验证器确保这种情况不会发生。
在Move的验证中，像to_consume这样的自有值只有在没有对该值的未决引用的情况下才能被move（无论是move到操作数栈还是移动到全局存储）。可以举一个反例：
我们得到了对应的报错：
我们也不能同时拥有可变的和不可变的引用，例如这个反例：
我们能够得到对应的报错：
可以理解为，Move对引用的更新要保证不可能同时影响到现有引用的值。Move Prover
整体结构
首先，Move Prover 接收一个Move源文件作为输入，该文件中需要设置程序输入规范（specification）。规范被从注释的代码中提取出来，而Move源代码被编译成Move字节码。
接下来，所有的堆栈操作都被从字节码中移除，并被局部变量的操作所取代，无堆栈的的字节码被抽象成一个验证器对象模型。沿着一个条路径，规范被解析并添加到验证器对象模型中。
最终确定的模型被翻译成Boogie中间验证语言（IVL）中的一个程序并传入Boogie验证系统，该系统对输入进行“验证条件生成”(verification condition generation)。该验证条件(VC)会被传入一个名为 Z3 的自动理论验证器(automated theorem prove)中。
VC 被传进 Z3 程序后，该验证器会检查 SMT公式是否是不可满足的。如果是这样，这意味着规范是成立的。否则，将生成一个满足条件的模型，并将其转换回Boogie格式，以便发布诊断报告。然后将诊断报告还原为与标准编译器错误类似的源码级错误。
spec
Move Prover有一个用于单个函数的基本规范语言（specifications）。规范包括经典的Floyd-Hoare前置条件，后置条件，以及一个新的条件，指定一个函数何时中止。规范被声明在“规范代码块”(specification block，spec代码块)中，它可能在Move Module的函数中，也可能作为一个单独的规范module文件。"规范块 "通过名称与正在指定的结构或函数或包含的模块相联系，规范永远不会影响模块的执行。
- 前置条件和后置条件是标准的。前置条件是由的保留词
requires引入，而后置条件则由ensures引入，并且每个后面都有一个布尔表达式，其语法与Move非常相似。ensures后面的子表达式可以用old(...)括起来，使表达式在进入函数后立即使用当前状态下的变量值进行计算。 - Move Prover允许用户指定一个函数在哪些条件下会被终止。这种类型的规范是由保留词
aborts_if引入。当aborts_if P出现在一个函数的规范中，Move Prover要求该函数终止，并且只在 P成立的情况下。如果指定了多个aborts_if条件，就会出现除非当且仅当所有条件的析取关系成立时，函数才会中止，否则就会出现错误。
一个简单的例子：
对应的spec：
Reference Elimination
引用消除转换是实现Move Prover中无别名内存模型的原因，在大多数软件验证和静态分析系统中，引用之间可能存在的别名关系的数量激增会导致高计算复杂性。
在Move中引用系统是基于借用语义设计的。初始借用必须来自堆栈上的全局内存或局部变量(从现在起都称为位置)。对于局部变量，可以创建不可变引用(使用语法&x)和可变引用(使用语法&mut x)。对于全局内存，引用可以通过borrow global和borrow_global mut内建来创建。给定对整个结构的引用，相应字段的借用可以通过&mut x.f 和&x.f 产生。
Move语言本身提供了以下保证，这些保证由借款检查器强制执行:
- 对于任何位置，都可以有一个可变引用，或n个不可变引用。（类似于Rust中的借用语义，只不过Rust中不存在全局存储）。
- 对堆栈上数据的引用的生存期不能超过堆栈位置的生存期。这也包括从函数内部借用的全局内存–全局内存的引用不能从函数返回。
这些属性有效地允许消除Move程序中的引用，消除了验证程序对别名的推理需要。
不可变引用
不可变引用可以直接被值替换：如下所示，我们从代码中删除了引用类型构造函数和所有的引用操作。
当执行一个Move程序时，不可变的引用对于避免复制的性能和执行所有权是很重要的。然而，对于正确的Move程序的符号推理来说，不可变的引用和值之间的区别并不重要。
可变引用
从一个可变引用&mut r 开始，Move可以选择更新这个引用的值（*r = v ），或者导出一个子引用(r' = &mut r.f )。当r和它派生的r’超出可用范围时，这个可变引用的生命周期就结束了。Move中的borrow checker会保证在引用数据可变期间，没有其他引用可以进入相同的数据。这也意味着不可能在引用被保留时观测这个值是否发生了变化。
这样的Move语义允许通过读-更新-写周期来处理可变的引用。我们可以在某个位置L中创建一个数据的副本，并执行一连串的变化步骤，这些步骤被表示为纯粹的功能数据更新。一旦L中数据的最后一个引用超出了范围，更新的值就会被写回L中。
这就可以把一个有引用的命令式程序转换为一个只有全局内存或堆栈上的变量有状态更新的命令式程序，没有别名。
动态可变引用
动态可变引用是指，引用的位置可能不是静态的，例如下面这种情况：
在逻辑编码中需要额外的信息来处理这种情况，当一个引用超出范围时，还需要知道它来自哪个位置以便写回更新的值。
于是引入了一个新的Mut<T> 类型，它是MVP的内部类型来跟踪T所来自的位置和T的值，并且支持以下操作：
-
Mvp::mklocal(value, LOCAL_ID)为一个新的可变引用创建一个给定的local id。 一个local id在函数中唯一地标识了一个局部变量。 -
Mvp::mkglobal(value, TYPE_ID, addr)为一个给定类型和地址创建一个新的可变变量。 - 可变值被替换为
r'=Mvp::field(r, FIELD_ID)，并使用v = Mvp::get(r)取回 -
Mvp::is_local(r, LOCAL_ID)可以测试r是否来自给定的本地，Mvp::is_global(r, TYPE_ID, addr)来测试一个特定的全局位置。Mvp::is_field(r, FIELD_ID)测试r是否是来自于给定的字段。
MVP通过数据流分析从程序中构建一个引用图来实现上图的转换，图会跟踪了引用的时间以及它们之间的关系。
例如r' = &mut r.f 创建了一条从r到r’的标记为f的边，r'= &mut r.g 创建了另一条同样从r开始的边。引用分析是程序间的，需要对被调用函数的引用图进行计算总结。
然后所得到的引用图被用来指导转换的过程，插入Mut类型的操作（图L14）。当对一个变量的引用结束时，相关的变化必须写回它的原始位置（L29）。
Global Invariant Injection
大多数软件验证工具通过在每个函数的入口处假设不变量并在函数出口处验证，来证明函数中的不变量，早期的Move Prover使用了这种方法。
当前的MVP采用了相反的方案，它会确保每条指令后的不变量都是成立的，除非用户明确指示某些不变性验证暂停。这是一种更细粒度的方法，并且具有性能优势。除非不变量被指示为暂停，不变量只需要在执行了一条可能使得不变性失效的指令时才进行验证。而这种证明通常在计算上是简单的，因为单一指令的变化通常很小。
不变式有两种类型：归纳不变式（Inductive invariant）和更新不变式（update invariant）
归纳不变式是在Move模块中声明的属性，这些属性必须默认在任何时候都对全局内存有效。基于Move的引用语义，归纳不变性在内存可变引用时不需要保持，因为在可变引用被写回之前，其他代码是看不到这些变化的。
归纳不变量是通过对全局存储器的演化进行归纳证明的。基本情况是，在创世事务之前的空状态下，该不变式必须成立。对于归纳步骤，可以假设不变式在每个验证的函数入口点上都是成立的，因为它没有被暂停，现在必须证明它在程序点之后成立，这些程序点要么是直接更新全局内存，要么是调用暂停不变式的函数。
更新不变量涉及两个状态，旧状态与当前状态，old操作被用来计算旧状态下的表达式。对于更新不变量，不需要归纳证明，因为它们只是与两个状态。前状态是在更新发生之前捕获的一些记录，而后状态是当前的状态。
对于这个例子：
- 第一个不变式，I1，是一个归纳不变式。它在函数输入时被假定，并在状态更新后被断言。
- 第二个，I2，是一个更新不变量，它与前、后状态有关。因此一个状态快照被存储在某个标签I2_BEFOR下，然后被用于断言。
全局不变性注入（Global Invariant Injection）：是通过静态分析获得的关于访问和修改的内存的知识来优化验证器的。定义accessed(f)是一个函数访问的内存，modified(f)是修改的内存。让accessed(I)由一个不变量构成（包括它所调用的所有函数的过境）。
-
如果accessed(f)与accessed(I)有重叠，则在进入f时注入assumption I。
-
在每个程序步骤之后，如果以下情况之一为真则注入断言I。
- 该步骤修改了accessed(I)中的一个内存位置M，
- 或该步骤是对函数f’的调用，并且modifies(f’)与accessed(I)相交，此外如果I是一个更新变量，在更新或调用之前注入一个内存快照的保存。
全局不变量利用泛型还可以变得通用起来，参考这个例子：
不变量I1对一个特定的类型实例S成立，而I2是通用的在S的所有类型实例上。在实例S上工作的非通用函数f将需要注入专门的实例I2[T = u8]。
然而，不变式I1并不适用于这个函数。因为它与S没有重叠。相比之下，g是通用的在R类型中，它可以被实例化为u64。所以，g适用于S的I1和I2。
Monomorphization
单态化是一种转换，它通过对相关类型实例化的程序进行专业化处理，将通用类型从移动程序中移除。单态化避免了通用值表示的问题，支持SMT逻辑中的多排序表示。
为了验证所有可能实例的泛型函数，单态化破坏了类型参数。即该函数被验证为一个没有特殊属性的新类型，然后它将所有被调用的函数用这个新的类型和他们可能使用的任何其他具体类型的数据类型具体化。
但是还需要考虑某些特殊的例子，例如：
根据T的不同类型，函数会有不同的行为，如果T取值是u64的话函数会abort。
算法工作原理：
- 对于modified(f)中的每个内存M，如果在modified(f)+accessed(f)中存在一个内存M’，使得M和M’可以通过T1,…,Tn进行统一，则从所产生的替换中收集一个类型参数Ti的实例化。这个实例化可能不会给所有类型参数赋值，那些未赋值的参数保持原样。例如，f<T1, T2>可能有一个部分实例化f<T1, u8>。
- 一旦所有的部分实例被计算出来，这个集合就会通过实例之间的统一而得到扩展。如果和<T’>在集合中，并且它们在替换s下统一，那么<s(T)>也将是集合的一部分。例如，考虑f<T1，T2>，它修改了M和R，也访问了M和R。由此计算出实例<u64, T2>和<T1, u8>，额外的实例<u64, u8>将被添加到该集合中。
- 如果在计算和扩展实例化之后，仍有任何类型参数，它们将被规划到前面描述的一个给定类型中。
Boogie
Boogie IVL是一种简单的命令式编程语言，支持局部和全局变量、分支和循环，以及过程和过程调用。Boogie是为验证而设计的，所以它也支持前后条件、循环不变量和全局公理。
Boogie验证系统，它应用验证策略来生成验证条件（SMT公式）。如果所有的验证条件都成立，那么每个程序在其前置条件成立的前提下确保其后置条件。
Boogie IVL所支持的变量类型与SMT求解器所支持的类型一致。例如，布尔运算、整数、数组、位向量和数据类型。Boogie被用来作为作为各种验证工具的后端。一般的策略是对源语言的语义在Boogie中建模。然后，源语言的程序和规范可以翻译成源语言的程序和规范可以被翻译成Boogie IVL，并使用Boogie验证系统进行检查。