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从原始类型中移除了带符号整数类型，只支持无符号整数用于内置的整数溢出检测。

代码片段1：用内置的溢出检测功能进行一次简单的u64加法

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

Output 1：溢出测试案例中出现的运行时ARITHMETIC_ERROR

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

Spec 1：代码片段1使用的规格

遗留编程习惯带来的挑战

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

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

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

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

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

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

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

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

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

Immovables 1

易受攻击的类型被恢复

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

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

代码片段2：Move合约实现中所使用的脆弱I128类型

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

修复建议

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

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

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

Spec 2：代码片段2使用的规格

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

Output 2：Move验证器对Spec 2和代码片段2的输出结果

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

Immovables 2

被误解的引用安全

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

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

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

代码片段3：对全局资源CoinStore的无效更新

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

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

Spec 3：代码片段3使用的规格

通过Move验证器指定被increase_fees函数修改的Config资源，我们就可以检测这类bug。如下图所示，验证器给出了不满足条件的错误信息，这表明increase_fees函数并没有改变全局资源Config。

Output 3：Move验证器不满足代码片段3和Spec 3的输出结果

修复建议

使用Move资源所有权模式可以有效降低上述代码的复杂性，并提高其安全性。以下示例运用了通用的幽灵类型来实现配置结构。

代码片段4：使用推荐的Move编程习惯组织资源

为了保证increase_fees函数修改全局状态，我们可以继续编写如下规格。

Spec 4：代码片段4使用的规格

在修复完成之后，验证器证明了次此执行符合规格要求，且没有引起任何故障。

Output 4：Move验证器对代码片段4和Spec 4的输出结果

写在最后

本文重点探讨了Move项目中一些常见的错误编程习惯。这些问题的出现大多是由于开发人员从非类型安全语言的代码中直接将遗留的编程设计进行生搬硬套。

好消息是，Move语言提供了一个内置的验证器以用于验证代码的执行情况。我们演示了如何利用Move验证器来验证和修复一些容易出错的编程习惯。但最彻底的办法还是让开发者们学习并使用Move的新型代码设计习惯。