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

然而,我们在 Move 智能合约审计过程中发现,许多开发者要么没有利用 Move 的内置保护机制,要么采用了与 Move 设计理念相悖的编程模式。这一现象产生的原因有两方面:其一是掌握一门新语言必须经历漫长的学习过程,其二是程序员们直接将遗留代码结构「迁移」到了新项目中,这样的编程习惯被称为 immovables(不动如山)。

作为一种编程语言,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被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Output 1:溢出测试案例中出现的运行时 ARITHMETIC_ERROR

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Spec 1:代码片段 1 使用的规格

遗留编程习惯带来的挑战

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

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

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

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

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

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

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

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

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

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

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

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
代码片段 2:Move 合约实现中所使用的脆弱 I128 类型

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

修复建议

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

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

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Spec 2:代码片段 2 使用的规格

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
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 操作。

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
代码片段 3:对全局资源 CoinStore 的无效更新

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

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Spec 3:代码片段 3 使用的规格

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Output 3:Move 验证器不满足代码片段 3 和 Spec 3 的输出结果

修复建议

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
代码片段 4:使用推荐的 Move 编程习惯组织资源

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Spec 4:代码片段 4 使用的规格

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

Move被误用的编程习惯:我们可以从Aptos智能合约审计中得到哪些启示?
Output 4:Move 验证器对代码片段 4 和 Spec 4 的输出结果

写在最后

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

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

(声明:请读者严格遵守所在地法律法规,本文不代表任何投资建议)

(0)
上一篇 2022年11月29日 下午2:54
下一篇 2022年11月29日 下午3:27

相关推荐

  • 数据解读:衍生品开始决定加密货币价格走势?

    首先谈谈 BTC。4 月中旬涌入大量多头头寸,但一旦资金费率变成负数,价格就会见顶。自此之后,随着价格下降,未平仓合约量(OI)也呈下降趋势,因为资金仍然是多空混合的,所以没有明确的趋势。但下图揭示了永合约现在是如何真正推动价格走势的。

    2023年5月5日
    2.4K
  • 加密货币交易所为什么都要做钱包?

    市面上钱包已有很多,但很少看见哪个钱包拥有「交易所」一样话语权,交易所站着把钱赚了,回来还抢钱包的一亩三分地。Why?

    2023年11月7日
    300
  • 以太坊被低估了吗?

    此前不少人称以太坊那么多年没有什么进展,实际上,以太坊扩容路线从侧链到 Rollups 等各种 Layer2 的落地,基本上安全可靠地突破了区块链技术扩容瓶颈,从各种公链包括比特币生态也在纷纷模仿复用以太坊的 OP-Rollup、ZK-Rollup 技术方案来搭建 Layer2 就可以侧面看出以太坊 Layer2 已经成功解决了公链扩容这一行业最核心问题。

    2024年5月3日
    58

发表回复

登录后才能评论
微信

联系我们
邮箱:whylweb3@163.com
微信:gaoshuang613