MoveBit Research Release | Belobog: A Move Fuzzing Framework for Real-World Attacks

marsbitPublished on 2025-12-16Last updated on 2025-12-16

Abstract

MoveBit introduces Belobog, a novel fuzzing framework designed specifically for Move smart contracts to address security challenges beyond syntax and type errors. Unlike traditional fuzzing methods that struggle with Move’s strong type system and resource semantics, Belobog leverages type-guided input generation and mutation. It constructs a type graph to produce semantically valid and executable transaction calls, significantly improving the efficiency and depth of state exploration. The framework integrates concolic execution (combining concrete and symbolic execution) to penetrate complex constraints and branch conditions, enabling deeper coverage of potential vulnerabilities. Evaluated on 109 real-world Move contracts, Belobog detected 100% of Critical and 79% of Major vulnerabilities confirmed by manual audits. It also demonstrated the ability to reproduce full exploit paths without prior knowledge of vulnerabilities. Designed to be developer-friendly, Belobog will be released as open-source to encourage community adoption and extension. The work is currently under peer review for PLDI’26. Preprint: https://arxiv.org/abs/2512.02918

Move, as a language that Web3 developers cannot afford to ignore, is particularly "hardcore" in its strong type system and resource semantics, especially regarding asset ownership, illegal transfers, and data races. Ecosystems like Sui and Aptos place increasingly important assets and core protocols on Move precisely because of its core language features, which enable the creation of more secure and lower-risk smart contracts.

However, the reality we've observed through long-term auditing and offensive/defensive practices is that a significant portion of thorny issues often do not occur in obvious places like "syntax errors" or "type mismatches," but rather at more complex, real-world levels—cross-module interactions, permission assumptions, state machine boundaries, and those call sequences that seem reasonable step-by-step but can be exploited when combined. Precisely because of this, even though the Move language has more robust security paradigms, there have still been significant attack incidents within its ecosystem. Clearly, security research for Move needs to go further.

We identified a core problem: the lack of an effective fuzzing tool for the Move language. Because Move has stronger constraints, traditional smart contract fuzzing faces a tricky pain point in the Move context: generating transaction sequences that are both "type-correct" and "semantically reachable" is very complex. If the input isn't precise enough, the call cannot be completed; if the call cannot be made, it fails to cover deep branches and reach critical states, making it easier to miss the paths that can truly trigger vulnerabilities.

Based on this long-standing pain point, we collaborated with a university research team to jointly complete and publish our research findings:

《Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts》

arXiv:2512.02918 (Preprint)

Paper Link:https://arxiv.org/abs/2512.02918

This paper is currently published on arXiv as a preprint, its significance is to allow the community to see research progress faster and receive feedback. We are submitting this work to PLDI’26 and awaiting the peer review process. After the submission result is confirmed and peer review is completed, we will also share relevant updates promptly.

Making Fuzzing Truly "Run Into" Move: From Random Trial and Error to Type-Guided Exploration

Belobog's core idea is straightforward: since Move's type system is its fundamental constraint, fuzzing should use types as a guide, not an obstacle.

Traditional approaches often rely on random generation and mutation, but on Move, this quickly produces a large number of invalid samples: type mismatches, unreachable resources, parameters that cannot be correctly constructed, call chains with blocking points—what you end up with is not test coverage, but a pile of "failures at the starting line."

Belobog's method is more like giving the Fuzzer a "map." It starts from Move's type system, constructs a type graph based on type semantics for the target contract, and then uses this graph to generate or mutate transaction sequences. In other words, it doesn't blindly stitch calls together but constructs more reasonable, more executable, and更容易深入状态空间的调用组合 (easier to深入 state space call combinations) along type relationships.

For security research, the benefit this change brings is not a "fancier algorithm," but a very simple yet crucial gain:
Higher proportion of valid samples, higher exploration efficiency, and a better chance of reaching the deep paths where real vulnerabilities often appear.

Facing Complex Constraints: Belobog Introduces Concolic Execution to "Push Open the Door"

In real Move contracts, critical logic is often surrounded by layers of checks, assertions, and constraints. If you only rely on traditional mutation, you easily keep bumping at the door: the conditions are never met, the branches are never entered, the state is never reached.

To solve this problem, Belobog further designed and implemented concolic execution (a hybrid of concrete execution + symbolic reasoning). Simply put:

It maintains concrete execution that "can run," while on the other hand, it uses symbolic reasoning to more directionally approximate those branch conditions, thereby more effectively penetrating complex checks and advancing coverage depth.

This is particularly important for the Move ecosystem because the "sense of security" in Move contracts is often built on multiple layers of constraints, and the real problems often hide in the gaps after these constraints intersect. What Belobog wants to do is push testing near these gaps.

Aligning with the Real World: Not Just Running Demos, But Approaching Real Attack Paths

We don't want this kind of work to stop at "being able to run demos." Belobog's evaluation directly targets real projects and real vulnerability findings. According to the experimental results in the paper: Belobog was evaluated on 109 real-world Move smart contract projects. The experimental results show that Belobog was able to detect 100% of the Critical vulnerabilities and 79% of the Major vulnerabilities confirmed by manual security expert audits.

More notably: Without relying on prior vulnerability knowledge, Belobog was able to reproduce full exploits in real on-chain incidents. The value of this capability lies in the fact that it更接近我们在现实攻防里面对的情况 (closer to the situations we face in real-world offense/defense): attackers succeed not through "single-point function errors" but through complete paths and state evolution.

What This Work Aims to Express is Not Just "Making a Tool"

This paper is worth reading not only because it proposes a new framework, but because it represents a more pragmatic direction: abstracting frontline security experience into reusable methods and落地 (grounding) it with verifiable engineering implementations.

We believe the significance of Belobog lies not in being "yet another Fuzzer," but in making Fuzzing on Move closer to reality—able to run in, go deep, and align more closely with real attack paths. Belobog is not a closed tool designed for a few security experts, but a developer-friendly framework: it strives to lower the barrier to entry, allowing developers to continuously integrate security testing into their familiar development workflow, rather than making Fuzzing a one-time, after-the-fact task.

We will also release Belobog as open source, hoping it becomes infrastructure that the community can collectively use, extend, and evolve, rather than remaining an experimental project at the "tool level."

Paper (Preprint):https://arxiv.org/abs/2512.02918
(This work is also currently submitted to PLDI’26, awaiting peer review.)

About MoveBit

MoveBit (Mobi Security), a sub-brand under BitsLab, is a blockchain security company focused on the Move ecosystem, aiming to make the Move ecosystem the most secure Web3 ecosystem by pioneering the use of formal verification. MoveBit has successively cooperated with many well-known global projects and provided partners with comprehensive security audit services. The MoveBit team consists of security experts from academia and industry leaders with 10 years of security experience, having published security research results at top international security academic conferences such as NDSS and CCS. Moreover, they are early contributors to the Move ecosystem, working with Move developers to establish standards for secure Move applications.

Related Questions

QWhat is the main challenge that traditional fuzzing tools face when applied to Move smart contracts?

ATraditional fuzzing tools struggle with generating transaction sequences that are both 'type-correct' and 'semantically reachable' in Move. Due to Move's strong type system and resource semantics, random generation and mutation produce a high volume of invalid samples, such as type mismatches, unreachable resources, and incorrectly constructed parameters. This results in many calls failing immediately, preventing deep branch coverage and making it difficult to reach critical states where real vulnerabilities often lie.

QHow does Belobog's approach differ from traditional fuzzing methods for smart contracts?

ABelobog uses Move's type system as a guide rather than an obstacle. It constructs a type graph based on the semantic relationships within the target contract and uses this graph to generate or mutate transaction sequences. This approach ensures that calls are constructed along type relationships, making them more reasonable, executable, and capable of penetrating deeper into the state space, unlike traditional methods that rely on blind, random splicing of calls.

QWhat technique does Belobog employ to handle complex constraints and branch conditions in Move contracts?

ABelobog employs concolic execution (a hybrid of concrete execution and symbolic reasoning). It maintains concrete execution to keep the program running' while using symbolic derivation to directionally approach branch conditions. This allows it to more effectively penetrate complex checks, such as assertions and constraints, and advance coverage depth, which is crucial for uncovering vulnerabilities hidden behind layered security checks in Move contracts.

QWhat were the key results of Belobog's evaluation on real-world Move smart contracts?

AIn an evaluation on 109 real-world Move smart contract projects, Belobog was able to detect 100% of the Critical vulnerabilities and 79% of the Major vulnerabilities that were confirmed by manual security audits. Notably, without relying on prior vulnerability knowledge, Belobog could also replicate full attack exploits (full exploits) from real on-chain incidents, demonstrating its ability to uncover complex attack paths that involve state evolution and multiple steps.

QHow does the Belobog team plan to release the framework, and what is its intended impact on the community?

AThe Belobog team plans to release the framework as open source. The goal is to make it a developer-friendly infrastructure that the community can collectively use, extend, and evolve, rather than keeping it as an experimental tool. By lowering the barrier to entry, it aims to integrate security testing seamlessly into developers' familiar workflows, promoting continuous security assessment rather than one-off, post-development audits.

Related Reads

Trading

Spot
Futures
活动图片