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)
Gao的头像Gao
上一篇 2022年11月29日 下午2:54
下一篇 2022年11月29日 下午3:27

相关推荐

  • 超 760 亿美元资金被窃取,盘点六大加密资产安全工具

    过去,加密领域因 Rug pulls 和骗局已经造成超 760 亿美元的损失。如何避免这些加密骗局,本文将盘点 6 个工具来为资金安全保驾护航。

    2023年5月22日
    2.1K
  • Coinbase研报:加密市场仍缺乏强有力的叙事,Q3将以波动为主

    第三季度开局不利,供应过剩,原因是对价格不敏感的持有者抛售比特币。其中包括德国政府的联邦刑事调查局 (BKA),该机构于 6 月 19 日开始出售其扣押的比特币。尽管他们的比特币销售规模(平均每天 8500 万美元)相对于每天 106 亿美元的 BTC 现货交易量(自 6 月 1 日以来,在全球中心化交易所)而言并不是特别大,但 BKA 无脑抛售的做法让市场感到不安,从而给比特币价格带来压力。

    2024年7月15日
    28
  • AI与Web3的首个交汇点已经出现?

    Paradigm 原文提出的概念为「以意图为中心的协议和基础设施」,这个「意图」其实很好理解,就是谁需要什么就会快速得到满足,而不是需要冗长的步骤来完成这些目标,我们以生活中一个意图为例,并总结在下图中。

    2023年8月28日
    532

发表回复

登录后才能评论
微信

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