Move被误用的编程习惯：我们可以从Aptos智能合约审计中得到哪些启示？

作为一种编程语言，Move 的设计初衷是为了创建可被形式化验证的安全智能合约。

通过严格的类型强制访问控制和加载时间验证，Move 的语言功能提供了一套强大的安防措施。与遗留的语言相比，Move 的内置资源和编程模式使开发人员能够创建更加安全的应用程序。

然而，我们在 Move 智能合约审计过程中发现，许多开发者要么没有利用 Move 的内置保护机制，要么采用了与 Move 设计理念相悖的编程模式。

这一现象产生的原因有两方面：其一是掌握一门新语言必须经历漫长的学习过程，其二是程序员们直接将遗留代码结构「迁移」到了新项目中，这样的编程习惯被称为 immovables（不动如山）。

本文包含关于 Move 智能合约代码审计的经验总结，需要读者对 Move 语言有一定的基本了解。

接下来，我们将介绍 immovables 类型的具体案例，并为其提供相应的修复建议。

Move 编程语言的优势

类型安全、资源安全和引用安全是 Move 语言的三个最重要的安全特性。

Move 将类型信息嵌入其字节码层面，并提供指定和强制执行资源所有权的运行机制。

每个资源对象的允许行为都会在加载时得到严格验证，并在运行时得以强制执行。

与 Rust 编程语言类似，Move 的语言设计也通过所有权规则来防止悬挂引用（dangling references）。但本文的目的并非对上述功能进行回顾，而是探讨在创建智能合约时不使用 Move 内置功能所引发的后果及补救措施。

Aptos 是一个使用 Move 语言编写的大型区块链项目，我们的安全专家团队已对 Aptos 核心代码进行了全面检查。

本文将对此过程中遇到的问题进行总结，以期对未来使用 Move 语言编写的项目有所帮助。

Move 和 Rust 一样都对类型系统进行了简化和限制，为开发者们在管理和转移资产方面提供了更多自由，同时也提供了必要的安全保护措施，以防止资产遭到攻击。如下图所示，Move 从原始类型中移除了带符号整数类型，只支持无符号整数用于内置的整数溢出检测。

Move被误用的编程习惯：我们可以从Aptos智能合约审计中得到哪些启示？ — 代码片段 1：用内置的溢出检测功能进行一次简单的 u64 加法

在代码片段 1 中，我们设定了一个包含两个 u64 值的加法函数。从下方测试案例可以看出，如果加法溢出，将在运行时触发 ARITHMETIC_ERROR。

Move 还提供了一个验证器，用于帮助开发者对合约代码的属性进行形式化验证。开发者可以在 spec blobs 中为每个函数指定前置条件和后置条件。随后，Move 验证器可以证明指定条件是否被满足，如果没有，则会提供具体反馈。例如，通过编写如下规格，我们可以验证内置的溢出检测功能。

遗留编程习惯带来的挑战

虽然 Move 具有许多强大的安全功能，但开发人员在编写智能合约时仍会面临一些安全挑战。

缺乏经验的开发人员可能会使用他们更熟悉但并不适用的遗留编程习惯，也可能因为学习难度过高而误用了某些 Move 的功能。

在最新开发的项目中，我们发现了一些基于 Move 编程习惯的案例，这些案例动摇了因 Move 强大的类型系统和抽象编程所带来的安全性。

有些编程习惯甚至会重现那些 Move 设计者们试图用创新的语法特性消除的漏洞。这些遗留的编程习惯包括：

① 不用 Move 类型重新设计项目，而是仍使用了易受攻击的类型；

② 不使用包含所有权限制的资源，只创建可拷贝的对象。

这些遗留的编程习惯在基于 Move 的智能合约中被称为 immovables。

由于许多项目程序是由开发人员从其他编程语言（如 Solidity）创建的项目中搬运过来的，而 Solidity 在其语言架构中并没有同等强大的类型特征（和限制），所以这些「大山」也变得尤为常见。

下文将介绍关于这类编程习惯及其问题的案例，同时我们也会针对每种情形给出修复建议。

Immovables 1 易受攻击的类型被恢复

在合约实现中，许多智能合约都使用了带符号整数进行数学运算。当拥有上述习惯的开发人员发现 Move 中都是无符号整数类型时也许会不知所措。

虽然有经验的开发者可以选择学习 Move 中的内置类型，并重新实现只包含无符号数字的合约，但有些开发者却选择将带符号整数类型直接搬回到他们的 Move 代码中。我们已经在 Move 项目中找到了一些案例，以下是一个简化版的示例：

在该案例当中，开发人员选择实现带符号整数类型（即 I128），这可能是由于引用实现使用了带符号整数，然后开发人员决定干脆保留这个设计，但使用上述实现实际上引发了整数溢出的问题。

修复建议

我们建议开发人员避免向 Move 项目导入这些不推荐的类型。最佳做法是使用内置的 Move 类型来重新设计应用程序。

然而，对于那些必须使用遗留习惯（如带符号整数对象）的情况，我们可以利用Move 的内置验证器来增加一层验证级别。

下图展示了通过 Move 验证器和如下规格寻找违规属性的示例，该规格保证了两个正整数相加的结果也应为正整数。

通过上述规格，我们可以运行内置的 Move 验证器，结果如下：

输出结果显示，Move 验证器捕捉到了一个违规情况。我们建议开发人员在不得不重新引入遗留类型时，利用验证器来验证自定义类型。

Immovables 2 被误解的引用安全

遗留习惯的第二个案例与 Move 语言的资源类型有关。

Move 提供了一种新颖的存储模型，在每个账户的地址下分离资源存储（指定为结构），并通过其类型信息进行索引。开发者需要添加能力注解来控制资源的 copy、key、store、drop 功能。

以下是一个经过简化的错误代码案例，该代码用于管理一个全局资源 Config。在 Config 中维护着多个 CoinStores，且以 coin_type 为索引。每个 CoinStore 中都包含一个 fees field 来指定当前的资产费率。该示例中 increase_fees 函数的目的是对 CoinStore 全局资源进行定位，并对 fees field 进行加 1 操作。

该代码包含一个因滥用资源拷贝功能而产生的 bug。调用 borrow_mut 的 increase_fee 函数后，本应返回 CoinStore 的一个可变引用，却返回了 CoinStore 的一个自有对象，即向量中原始对象的副本，因此 increase_fees 函数的任何更新都不会影响全局存储。

值得注意的是，开发者将拷贝能力分配给了结构定义，所以 CoinStore 的隐式拷贝行为也受到允许。