Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts
Wanxu Xia, Ziqiao Kong, Zhengwei Li, Yi Lu, Pan Li, Liqun Yang, Yang Liu, Xiapu Luo, Shaohua Li
TL;DR
<3-5 sentence high-level summary> Belobog tackles the gap in Move smart contract testing by introducing the first type-aware fuzzing framework that guarantees well-typed transactions through a formal type graph, and bolsters exploration with a MoveVM-based concolic executor. It systematically handles Move-specific challenges such as type parameters and Hot Potato objects, achieving superior bug-finding, coverage, and throughput on real-world datasets and reproducing major incidents like Cetus and Nemo. The work provides substantial empirical evidence that automated, type-conscious fuzzing can significantly enhance Move ecosystem security, and it ships open-source tooling to enable broader adoption and extension.
Abstract
Move is a research-oriented programming language design 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 Move smart contracts, i.e., Cetus and Nemo. Belobog successfully reproduced full exploits for both of them, without any prior knowledge.