[Paper] Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts

Source: arXiv - 2512.02918v1

Overview

The paper presents Belobog, the first fuzzing framework that can automatically generate valid transactions for smart contracts written in the Move language (used by blockchains such as Sui and Aptos). By being “type‑aware,” Belobog overcomes Move’s strict static typing and resource model, enabling systematic security testing that was previously impossible with existing fuzzers.

Key Contributions

• Type‑aware transaction generation: Constructs a type graph from a Move module and uses graph traces to synthesize only well‑typed transactions.
• Concolic execution engine: Combines concrete execution with symbolic reasoning to satisfy complex runtime checks (e.g., resource balance, capability checks).
• First Move‑specific fuzzer: Provides a practical toolchain for automatically discovering bugs in real‑world Move contracts.
• Empirical validation: Tested on 109 open‑source Move projects, achieving 100 % detection of manually‑verified critical bugs and 79 % of major bugs.
• Real‑world exploit reproduction: Successfully reproduced the Cetus and Nemo attacks without any prior knowledge of the vulnerabilities.

Methodology

1. Static Analysis & Type Graph Construction

   • Belobog parses the Move source and extracts all type definitions, structs, resources, and function signatures.
   • It builds a directed type graph where nodes represent concrete types and edges capture how types can be composed (e.g., a Vector<T> node points to its element type T).

2. Transaction Generation / Mutation

   • Starting from a graph trace (a walk through the type graph that respects Move’s linear resource rules), Belobog assembles a transaction payload that is guaranteed to type‑check.
   • For existing transactions, Belobog mutates arguments by following alternative graph traces, ensuring each mutation stays well‑typed.

3. Concolic Execution

   • The generated transaction is first executed concretely on a lightweight Move VM.
   • When a runtime guard (e.g., assert!, capability check) fails, the engine records the branch condition and solves it symbolically to produce new concrete inputs that satisfy the guard.
   • This “concrete + symbolic” loop lets Belobog explore deep contract logic that pure random fuzzing would never reach.

4. Bug Detection

   • The framework monitors for common vulnerability patterns: re‑entrancy, unauthorized resource transfer, integer overflow/underflow, and logic errors flagged by panics or failed assertions.

Results & Findings

The authors conclude that type‑aware fuzzing combined with concolic execution is essential for Move, where naïve fuzzers generate ill‑typed transactions that are rejected before any contract logic runs.

Practical Implications

• Developer tooling: Belobog can be integrated into CI pipelines for Move projects, automatically surfacing logic bugs before deployment.
• Audit automation: Security auditors can use Belobog to quickly generate high‑confidence test suites, reducing manual effort and the chance of missing subtle resource‑related bugs.
• Blockchain operators: Node operators on Sui/Aptos can run Belobog against newly submitted modules to catch exploitable patterns early, improving network safety.
• Language design feedback: The success of a type‑aware fuzzer highlights that even languages with strong static guarantees benefit from runtime testing, informing future extensions to Move’s type system or VM diagnostics.

Limitations & Future Work

• Scalability of concolic solving: As contract complexity grows, the symbolic solver may hit performance bottlenecks; the authors suggest incremental solving and caching as next steps.
• Coverage of non‑deterministic primitives: Belobog currently focuses on deterministic VM instructions; handling randomness (e.g., random_u64) or external oracle calls remains an open challenge.
• Cross‑contract interactions: The framework treats each contract in isolation; extending it to fuzz multi‑contract workflows (e.g., DeFi composability) is future work.
• User‑defined invariants: Incorporating developer‑written specifications (e.g., Move’s spec blocks) could guide the fuzzer toward more targeted security properties.

Belobog demonstrates that even a language as safety‑centric as Move needs dedicated, type‑aware dynamic testing. For developers building the next generation of blockchain applications, integrating such fuzzing tools into the development lifecycle could be the difference between a secure launch and a costly exploit.

Authors

• Wanxu Xia
• Ziqiao Kong
• Zhengwei Li
• Yi Lu
• Pan Li
• Liqun Yang
• Yang Liu
• Xiapu Luo
• Shaohua Li

Paper Information

• arXiv ID: 2512.02918v1
• Categories: cs.CR, cs.PL, cs.SE
• Published: December 2, 2025
• PDF: Download PDF