Move is a research-oriented programming language designed for secure and verifiable smart contract development and has been widely used in managing billions of digital assets in blockchains, such as Sui and Aptos. Move features a strong static type system and explicit resource semantics to enforce safety properties such as the prevention of data races, invalid asset transfers, and entry vulnerabilities. However, smart contracts written in Move may still contain certain vulnerabilities that are beyond the reach of its type system. It is thus essential to validate Move smart contracts. Unfortunately, due to its strong type system, existing smart contract fuzzers are ineffective in producing syntactically or semantically valid transactions to test Move smart contracts. This paper introduces the first fuzzing framework, Belobog, for Move smart contracts. Belobog is type-aware and ensures that all generated and mutated transactions are well-typed. More specifically, for a target Move smart contract, Belobog first constructs a type graph based on Move's type system, and then generates or mutates a transaction based on the graph trace derived from the type graph. In order to overcome the complex checks in Move smart contracts, we further design and implement a concolic executor in Belobog. We evaluated Belobog on 109 real-world Move smart contract projects. The experimental results show that Belobog is able to detect 100% critical and 79% major vulnerabilities manually audited by human experts. We further selected two recent notorious incidents in the Move ecosystem, i.e., Cetus and Nemo. Belobog successfully reproduced full exploits for both of them, without any prior knowledge. Moreover, we applied Belobog on three ongoing auditing projects and found 2 critical, 2 major, and 3 medium new vulnerabilities, all acknowledged by the project developers.

翻译：Move是一种面向研究的编程语言，专为安全且可验证的智能合约开发而设计，已广泛应用于管理区块链（如Sui和Aptos）中的数十亿数字资产。Move具备强大的静态类型系统和显式资源语义，可强制执行安全性属性，例如防止数据竞争、无效资产转移和入口漏洞。然而，用Move编写的智能合约仍可能包含其类型系统无法覆盖的某些漏洞。因此，对Move智能合约进行验证至关重要。遗憾的是，由于其强大的类型系统，现有的智能合约模糊测试工具难以生成语法或语义有效的交易来测试Move智能合约。本文介绍了首个针对Move智能合约的模糊测试框架Belobog。Belobog具备类型感知能力，确保所有生成和变异的交易均为良类型的。具体而言，对于目标Move智能合约，Belobog首先基于Move的类型系统构建类型图，然后根据从类型图导出的图迹生成或变异交易。为了克服Move智能合约中的复杂检查，我们进一步在Belobog中设计并实现了混合执行器。我们在109个真实世界的Move智能合约项目上评估了Belobog。实验结果表明，Belobog能够检测出人工专家手动审计的100%关键漏洞和79%主要漏洞。我们进一步选取了Move生态系统中最近发生的两起著名事件，即Cetus和Nemo。Belobog在没有任何先验知识的情况下，成功复现了这两起事件的完整利用过程。此外，我们将Belobog应用于三个正在进行的审计项目，发现了2个关键、2个主要和3个中等的新漏洞，所有漏洞均得到了项目开发者的确认。