一文了解Move的编程魅力：Facebook的Diem团队梦碎，但成果留存

Move 是一种相对发展时间较短的编程语言，但已经在许多 Web3.0 项目中得到了应用。

CertiK 安全专家团队最近审计了一个支持 Move 编写智能合约的新型 Layer 1 区块链。借此机会，我们将为大家整体概述一下 Move 这一新型编程语言。

鉴于该内容较为专业，在这篇文章中，我们将讨论 Move 及其两个特性：可编程资源（有助于支持高交易率）和形式化验证（有助于提高安全性）。

在这一过程中，本文也将展示 Move 的语法、类型系统和内存模型，并研究工程师在使用 Move 时可能犯的一些常见错误。除此之外，我们也将从技术角度审视 Move 形式化验证的潜力及面临的挑战。

什么是 Move？

Move 是一种用于编写智能合约的特定领域编程语言。最近推出的几个热门项目均支持 Move 语言，包括 Aptos 、0L 和 Starcoin 区块链。另外还有 Sui 区块链同样支持 Move 语言并将其命名为 Sui Move。

Move 最初是作为 Diem 项目的一部分开发的，但这一属于 Meta（原 Facebook ）的基于区块链的支付网络现在已被解散。

在 Diem 发表的《为什么要创建 Move？》文档中，其指出：

「为了成功支持像 Diem 支付网络这样的支付系统，我们需要一种可以对数字资产的所有权进行编码，并为这些资产的转移创建程序的编程语言。目前已经有数百种语言在使用，其中一些已经作为原生语言包含到区块链的实现中。

Diem Networks 本可以选择一种通用语言，如 WebAssembly 或 Java 字节码，或现有的区块链语言，如 EVM 字节码或比特币 script。理论上，我们的确应当选择一种现有的语言，毕竟一种语言的社区、库、工具都和语言设计一样重要，而这些都需要多年的时间来建立。从这一角度上来说，应该谨慎创建一种新语言。但最终选择创建 Move 是因为我们看到了一个机会——Move 将可以帮助我们在几个重要方面对现有替代方案进行逐步改进。」

Diem 需要安全地支持大量的交易，因此其团队决定以这些目标为基础创建 Move。

可编程资源

Move 的关键特征之一是它对可编程资源的使用。一个资源（Resource）直接代表着一条有价值的数据（例如一个用户所持有的项目资产数量）。在 Move 中，每个持有项目资产的账户中通常都存储着可以直接代表该资产的数据。这与 Solidity 中项目资产的表示形成了鲜明的对比，从账户到他们持有的项目资产数量的映射，Solidity 通常是使用一张映射表在智能合约中进行记录。

这种对可编程资源的利用有两个主要优势。首先，它形成了一个支持高交易率的智能合约编程模型。如果一项交易涉及两个「仅相互交互」的账户，该交易可以与其他交易并行执行。类似于现实生活中，小明在便利店结账付款并不影响小红的结账付款。Aptos 区块链就是一个很好的例子，其使用软件交易存储器来并行运行交易，并检测两个同时进行的交易是否可能发生冲突。

可编程资源的第二个优势是它们可以自动验证程序是否存在某些类型的错误：例如，资源永远不会被悄无声息地删除或复制——这是由 Move 编译器完成的。但是仍然有可能在智能合约代码中引入算术或逻辑错误，从而导致资源中出现不正确的值。

下图来自 GitHub（https://github.com/move-language/move）上的 Move 文档，显示了区块链数据在 Move 中的组织方式。Move 将区块链状态称为全局存储。

每个区块链地址代表一个账户，其中一些可能是外部拥有的。与以太坊不同的是，所有地址都可以存储数据。在下图中，BasicCoin 持有者的账户中有数据表明他们所持有的 BasicCoin 数量（资源）。该图显示，地址 0x42 还拥有一个实现 BasicCoin 的代码模块。

当使用 Move 编写智能合约时，最好的做法是将资源存储在拥有该资源的账户中，而非包含该智能合约代码的账户中。尽管有可能在 Move 智能合约中实现「Ethereum 风格」的资源映射，但涉及此类合约的交易可能无法并行执行。

Move 的安全功能

Move 包含几个可帮助开发者创建更安全智能合约的功能。其中就包括上文所提到的“编译器会检查资源的基本使用情况”这一功能。Move 语言原生就支持形式化验证，并有意排除了那些容易导致形式化验证困难的语言结构。

此外，Move 还支持泛型。泛型编程（Generic Programming）允许通用代码在不同类型中被重复使用。

这一点很重要，因为使代码更安全的一种方法是重用那些已被专家精心编写过的代码，少编写一些新代码。就像许多 Coin 共享实现代码——如 Aptos Coin 标准所示，通用编程允许该代码在不同 Coin 之间共享。

Move 类型系统和 Rust

在处理有价值的数据时，追踪清楚是谁拥有这些数据，并限制对这些数据的操作（如复制或删除）十分重要。

幸运的是，已经有一种开发完善的支持所有权特性的编程语言：Rust。Move 的开发者在类型和语法方面都受到了 Rust 思想的启发。

此图表显示了 Move 的内置原始类型：

此图表显示了 Move 的结构类型，这些是由其他类型构建的类型：

当涉及到结构类型时，事情就变得有趣了，结构类型是 Move 中唯一的用户定义类型，一个结构类型是一个存储在字段中的值的集合：

在 Move 中，结构是一种“value”类型。结构类型的 value 在内存或存储中是线性排列的，对一个结构的引用必须明确地构建。这与 Solidity 不同，在 Solidity 中，结构变量通常是对底层 value 的引用。下图说明了这一点：

字段可以是除引用类型之外的任何类型，结构的实例是通过打包创建的（就像在 Rust 中那样）。

Move 为结构类型的 value 实现了一个类似于 Rust 的所有权系统，其中每个 value 都由包含它的变量或字段拥有。引用并不拥有它们所指向的任何 value。

默认情况下，结构 value 只能被转移到另一个所有者，它们不能被复制或删除。当一个结构 value 被转移到另一个所有者那里时，它将无法被先前的所有者访问。

在一个结构类型的 value 被创建后，同一时间只存在该 value 的一个可以使用的副本。以下代码说明了这一点：

Move 还有一个称为 abilities 的类型特性，它可以控制一个给定类型的 value 可被允许进行哪些操作——这是受到了 Rust 的启发。这四种能力分别是：

Copy：value 可以被复制。不具备复制能力的结构在被使用后无法被访问。

Drop：value 可以被删除。当一个 value 的所属变量或字段超出范围时，该 value 将被删除。不具备删除能力的结构则必须被使用，无法被丢弃。要么明确地销毁它们，要么将它们「转移」到其他地方。它们不能被无声无息地删除或丢弃。

Store：value 可以存储在全局存储的其他结构中。

Key：该类型可用作「键」来对全局存储进行访问。

对于结构类型来说，abilities 是在结构类型声明中声明的，如下图所示：

以上内容主要介绍了 Move 是什么，以及其一个关键特性：可编程资源。

接下来我们介绍 Move 的另一关键特性：形式化验证，及该特性为 Move 所带来的优势和弊端。

深度资源

一个资源是一个只有 key 和 store 能力的结构体。在 Move 中，一个账号每种类型的资源只能持有一个。资源不能被复制或丢弃，这使得资源适合直接代表价值的物品，例如 coin。

账户与其资源之间的直接关联，使得编写某些「不好的」代码也变得更加困难，例如导致价值意外损失的代码。

但是，不正确的计算以及与资源有关的那些更微妙的逻辑错误还是有可能会出现。这就是为什么我们强烈建议进行智能合约审计来增强安全保障。

区块链上全局存储的编程接口执行了一个限制——每个账户最多只能持有每个资源的一个副本。

一个程序可以使用以下操作在全局存储中创建、读取、更新和删除资源：

为了避免资源的伪造及其他不当操作，Move 执行严格的数据封装（encapsulation of data）。Move 的代码和类型声明被分组为 module。代码作为 module 的一部分被部署到一个账户中。

当一个结构类型在一个模块中被声明时，只有在同一模块中定义的函数可以访问该结构类型的字段或创建该结构类型的 value。Move 结构声明被视为抽象数据类型，对其 module 以外的代码隐藏其内部工作原理。module 中的函数默认为私有，只能在模块内调用。它们可以被声明为 public，这使得它们可以被外部代码访问。module 可以有 friend，也就是他们信任的其他 module，并且可以声明个别 non-public 方法以供 friend 访问。

References

Reference 是 pointer 的一种类型，包括对其使用方式的限制。使用 pointer 的语言中，一个常见问题是悬挂引用（dangling references）：指向已被重新用于其他目的或被取消分配的内存或存储。

例如，如果你为一个向量的最后一个元素创建了一个 reference，然后缩小了向量，则该 reference 现在就指向了无效的内存或存储。悬挂引用和其他与不受限制的 pointer 相关的问题历来是导致大多数软件安全漏洞的原因。

Move 处理 reference 的方式与 Rust 处理 reference 的方式类似。它包括类型检查规则，以确保 reference 的生命周期不长于原始数据的生命周期。当代码创建一个 reference 时，该 reference 并没有取得数据的所有权。相反，代码借用了读取或写入数据的能力。

在阅读 Move 代码时，名称中带有“borrow”一词的操作就会产生 reference。

Move 语言的定义中并不包含对 reference checking 的完整描述（「borrow checker」，它确保 borrow 的 reference 不会存留太长时间）。

不过，今年有一份详细的技术论文被发表（https://arxiv.org/abs/2205.05181），该定义中的两个关键规则是：

不允许对 reference 的 reference，而且 reference 不能存储在结构中。这意味着，当一个函数被调用并带有一个 reference 参数时，尽管它可以返回 reference，但也不能将 reference 存储在一个长期存在的数据结构中。一个函数调用并不会延长 reference 的生命周期。

对局部变量或局部变量字段的 reference 不能超过局部变量的作用域的终点。

类 Rust 语法

Move 有一种类似于 Rust 的语法，在某些地方与 C 风格的语言有些不同。在此，我们总结了一些重要的语法规则，以便更轻松地浏览 Move 代码。

使用 let 声明变量：

类型注释：type 和 initializer=e 是可选的。当它们被省略时，Move 使用类型推理来确定变量的类型。

下图是一些变量声明的例子：

Move 有典型的表达式，用于算术、移位操作、函数调用、赋值等，用于流程控制的有 if、while、for、break 和 continue 等表达式。

函数是使用以下语法声明的：

其中 id 是函数的名称，parameter-list 声明参数，return-type 是返回类型。还有一些必要的注释，如 acquires 注释。这些注释列出了函数从全局存储中访问的资源，还有关于可见性的注解。如前所述，函数可以是公共的、私有的，或者可以被 friend module 访问。

形式化验证

智能合约安全和正确地运行至关重要，因为其往往持有巨额的资产。形式化验证是确保一个程序（如智能合约）执行其预期操作的最佳技术之一。

在形式化验证中，工程师编写规范，并以数学方式表达代码的预期行为。然后使用工具尝试检查代码是否符合规范。

我们可以将这种检查视为测试，但这其中有一个关键的区别：它不是检查代码在某些特定情况下的行为，而是检查代码在所有可能情况下的行为。

如果检查通过，则说明该工具找不到代码违反规范的用例。不过这并不意味着代码 100% 不存在违反规范的情况，因为工具或编译器的漏洞还是有可能导致错误的发生。但这依旧使得其比运行一组测试用例提供了更严格的规范保证。

对于一些代码，特别是复杂的代码，工具可能无法自动检查代码是否符合规范。因此工程师也许需要为一小部分的代码添加具体化的规范，直到检查器能够成功运行为止。工程师甚至可能需要写证明规则，然后该工具会根据数学原理检查代码是否符合这些证明规则。

因为确保智能合约的安全是至关重要的，一些智能合约编程语言会原生就提供对形式化验证的支持。就像 Solidity 编译器提供的 SMTChecker 工具，它假设 requires 子句始终为真，然后试图证明 assert 子句永远不会失败。

Move 也对形式化验证技术进行了集成支持。它含有丰富的用于形式化验证的规范语言，能够规范比 Solidity 的 requires 和 assert 子句更复杂的属性，并且有目的地删除了会对形式化验证造成问题的语言结构。Move 的开发环境中就包括一个名为「Move Prover」的检查器。

CertiK 由两位常春藤盟校的计算机科学教授所创立。作为区块链安全领域的先驱，CertiK 运用的正是目前最先进的形式化验证技术。创办 CertiK 的两位教授均是形式化验证方面的专家，并创建了 CertiKOS——世界上第一个也是唯一一个完全被验证的并发式多核操作系统和管理程序。CertiK 致力于通过将形式化验证技术应用于安全审计以确保智能合约的安全。

因此，CertiK 安全专家自然而然地就注意到了 Move 这一集成了形式化验证技术的编程语言。

下方是一个 double 函数及其规范的简单示例。double 函数的功能是将一个 64 位无符号整数（unsigned integer）进行翻倍计算。由 spec double 给出的 double 规范从数学上描述了预期的结果。