Move 智能合约安全性研究
2024-11-2219:18
作者单位：电子科技大学计算机（网安）学院
研究方向：区块链、Move 智能合约、缺陷检测、程序分析
近年来，Move 作为一种面向智能合约的编程语言，因其以安全为核心的设计理念而备受关注。Move 引入了多项创新以提高资产的安全性，例如为资产安全专门设计的新数据类型、严格访问控制以及内置的安全组件 Move Prover。目前，Move 已被多个区块链平台采用，如 Starcoin、Aptos 和 Sui。然而，Move 合约在实际应用中的安全有效性仍存在不确定性。
尽管已有大量关于 Solidity 智能合约的实证研究，关于 Move 合约的系统性研究却相对稀缺。已有的研究方法虽涵盖了 Move 合约中的部分缺陷检测和形式化验证，但在真实世界中的 Move 合约中，关于这些缺陷的广泛性、潜在安全风险的分类和分析依然不足。当前缺乏对大量 Move 合约中缺陷的全面研究，这些缺陷可能会造成安全隐患、功能缺陷、误导用户或浪费计算资源，因此亟需进一步系统性和自动化的分析工具来支持 Move 合约的安全性研究。为了填补这一研究空白，我们首次针对 Move 合约的安全性进行了全面研究，开展了首个关于 Move 合约安全性的实证研究，通过审计来自真实项目的 652 个开源合约，发现了八种类型的缺陷。同时提出了专为 Move 字节码设计的自动化分析框架 MoveScan，证明其在性能上优于现有工具。将 MoveScan 应用于采用 Move 的主流区块链后，我们发现了 97,028 个缺陷，突显出已部署合约中此类问题的显著存在。该文章相关研究成果发表于 2024 软件工程顶会 ISSTA。注：实证研究侧重于通过观察和实验来收集数据，主要依赖于可观察的事实和数据，并用这些数据来验证理论或假设。
为了探讨研究问题，我们制作了两个数据集作为实验支撑，如下图所示，其中:
数据集一（ds1）：该数据集收集了 92 个真实 Move 项目的源代码，共计 652 份合约，涵盖去中心化金融、代币、跨链桥、标准库、基础设施等领域。源代码来自 Aptos 和 Sui 官方推荐的项目列表及 Starcoin 仓库。ds1 的合约主要用于人工审计、形式验证和源码检测，并作为基准来对比 MoveScan 与 Move Prover、MoveLint 等工具的性能，以此论证研究的问题 RQ1、RQ2 和 RQ3。数据集二（ds2）：该数据集聚焦于区块链上已部署的合约字节码。我们收集了从 2022 年 10 月 14 号至 2024 年 1 月 30 日 Aptos 和 Sui 链上部署的合约字节码，得到 37,302 份合约字节码（其中 Aptos 合约 15,479 个，Sui 合约 21,823 个）。具体的，数据集中 Aptos 的字节码通过 Chainbase 查询获取，Sui 的字节码则通过 Suiscan 的 API 获取。
针对 Move 合约的安全性进行了全面研究，我们围绕以下三个问题进行展开：RQ1：Move 合约中存在哪些缺陷？
RQ2：Move Prover 的缺陷识别效果如何？
RQ3：MoveLint 的缺陷识别效果如何？
我们首次对 Move 合约的安全性进行了全面的实证研究，为揭示 Move 合约的真实安全问题，我们与区块链安全团队 BitsLab 旗下 MoveBit 合作，人工审计来自 ds1 的 652 个合约，识别出 1,064 个缺陷，涵盖八种类型，并给出了具体的案例分析。这些缺陷可能引发安全风险、功能缺陷、误导用户或浪费 gas。
RQ2：Move Prover 的缺陷识别效果如何？
Move Prover 与 Move 语言一起发布，是由 Move 核心团队开发的形式验证工具。它通过规范提取、字节码编译和 SMT 公式生成的多步骤过程，根据形式化规范验证 Move 项目源代码，以便由 SMT 求解器进行验证。Move Prover 通过验证源代码是否符合形式化规范来识别缺陷，因此，除了源代码之外，还需要在源代码中编写相应的形式化规范，因此我们首先检查 ds1 中的合约是否已经包含开发人员编写的规范。如果存在相应的规范，我们可以重用它们，而不必从头开始编写它们。然而，统计显示只有 89 个（13.65%）合约包含规范，但不能直接用于检测定义的缺陷。因此我们使用 Move Prover 定义的 Move Specification Language (MSL) 为包含缺陷的合约编写规范，最终成功地针对 Inf. Loop、Ovflw. 、Prec. Loss 三种缺陷编写了规范。为评估 Move 的官方形式化验证工具 Move Prover 的有效性，我们对 ds1 中 283 个带有缺陷的合约进行了测试。表 1 的结果表明，Move Prover 仅能识别 6.02% 的缺陷（64/1,064），主要由于 Move Prover 是通过监测变量的状态变化进行验证，而其中的五类缺陷并不涉及变量的状态变化。此外，Move Prover 要求编写新的形式化规范语言，增加了使用难度，且仅支持源代码输入，无法单独分析合约。因此，由于需要人工干预、支持的缺陷类型数量有限、缺乏字节码支持以及需要完整的项目源代码，Move Prover 在识别缺陷方面存在局限性。MoveLint 是目前唯一可用的静态分析工具，它将源代码转换为 AST，并通过预定义的规则识别漏洞。我们将 MoveLint 应用于 ds1 的 652 个合约，结果显示其只能检测到 4.61% 的缺陷（49/1,064），在表 1 中，“-”表示 MoveLint 不支持的缺陷类型。除此之外依然存在许多漏报问题，归因于其依赖的编译器仅支持原生 Move，无法支持 Aptos 和 Sui 修改过的 Move，造成 ds1 中的 460 合约无法被 MoveLint 使用的原生编译器编译，导致其漏报率较高。同时，MoveLint 同样需要源代码支持，难以在大规模分析中广泛应用。如果排除无法编译的合约，召回率和 F1 分数将分别提高到 25% 和 38.89%。在性能方面，MoveLint 的时间开销在可以接受的范围内，每个项目平均需要 71.72 毫秒。因此，MoveLint 由于漏报率高、缺乏字节码支持以及需要完整的项目源代码，因此在缺陷识别方面效果不佳。
在上述背景下，MoveScan 框架被设计出来，用于满足自动化、字节码支持、更多缺陷类型支持以及高精度的需求，解决现有工具无法有效分析大规模 Move 合约缺陷的问题。MoveScan 通过三阶段流程实现对 Move 字节码的高效自动化分析：字节码转换为中间表示：MoveScan 将字节码转换为更适合元数据提取的中间表示，以此替代基于栈的操作码，将其转换为基于局部变量的操作。中间表示转换简化了元数据提取过程，为后续分析提供了基础。元数据收集：在中间表示的基础上，MoveScan 收集缺陷检测所需的元数据，包括控制流图（CFG）、调用图（CG）、数据依赖树（DDT）和变量范围约束。缺陷检测与扩展支持：MoveScan 使用八个内置检测器，通过预定义接口提取必要的元数据并识别缺陷。还为用户提供了开发新检测器的接口，平均仅需 96 行代码即可增加一个检测器，方便扩展以支持新的缺陷类型，提高适应性。通过这一设计，MoveScan 实现了对字节码的全面分析，能够自动检测多种缺陷，且具备灵活扩展性。为了评估 MoveScan 的准确率，我们使用 MoveScan 检测 ds1 中的 652 个合约，报告了 1,041 个缺陷。与人工审计到的 1,064 个缺陷相比，漏报仅 35 个（均为 Un. Const.，无安全风险），误报 12 个（均为 Ovflw.），MoveScan 的准确率、召回率和 f1 分数分别达到 98.85%、96.71% 和 97.77%。MoveScan 在检测效率上同样出色，单个合约平均分析时间仅 0.77 毫秒，且 90% 以上的合约分析时间低于 16.91 毫秒。在以项目为单位的分析中，MoveScan 的平均时间为 5.45 毫秒，仅为 MoveLint 的 7.6%。在链上数据集 ds2 的分析中，90% 的合约分析时间低于 3.01 毫秒，进一步展现了 MoveScan 的高效性。综上所述，MoveScan 在准确性、效率和适用性方面显著优于现有工具，为 Move 生态的安全性研究提供了重要支持。
论文链接：
https://dl.acm.org/doi/abs/10.1145/3650212.3680391
实验数据：
https://anonymous.4open.science/r/support_material-D28C
联系方式：
shuwei@std.uestc.edu.cn
原文出处： Science BC
【免责声明】市场有风险，投资需谨慎。本文不构成投资建议，用户应考虑本文中的任何意见、观点或结论是否符合其特定状况。据此投资，责任自负。
