MoveBit is a blockchain security company focused on the Move ecosystem, making it the safest Web3 ecosystem by being the first to use formal verification.

Author: BitsLab

Move, as a language that Web3 developers cannot ignore, is very "hardcore" in terms of its strong type system and resource semantics, particularly regarding asset ownership, illegal transfers, and data races.

Ecosystems like Sui and Aptos are placing more and more key assets and core protocols on Move, also due to the core features of the Move language, which enable the establishment of safer and lower-risk smart contracts.

However, what we have observed in long-term auditing and offensive-defensive practices is that a significant portion of tricky issues often does not occur in obvious places like "syntax errors" or "type mismatches," but rather at more complex and realistic system levels—cross-module interactions, permission assumptions, state machine boundaries, and those calling sequences that seem reasonable at each step but can be exploited when combined.

Because of this, even though the Move language has a more complete security paradigm, significant attack incidents have still occurred within its ecosystem. Clearly, security research on Move still needs to advance further.

We have identified a core issue: there is a lack of an effective fuzzing tool in the Move language. Due to the stronger constraints of Move, traditional smart contract fuzzing faces a tricky pain point in the Move scenario: generating transaction sequences that are "type correct" and "semantically reachable" is very complex. If the input is not precise enough, the call cannot be completed; if it cannot be called, deep branches cannot be covered, and critical states cannot be reached, making it easier to miss the paths that can actually trigger vulnerabilities.

Based on this long-term pain point, we collaborated with academic research teams to jointly complete and publish research results:

"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, meaning it allows the community to see research progress more quickly and provide feedback. We are submitting this work to PLDI’26 and awaiting the peer review process. Once the submission results are confirmed and the peer review is completed, we will promptly share relevant updates.

Making Fuzzing Truly "Run" in Move: From Random Trial and Error to Type Guidance

The core idea of Belobog is straightforward: since the type system of Move is its foundational constraint, fuzzing should treat types as navigation rather than obstacles.

Traditional approaches often rely on random generation and mutation, but in Move, this quickly generates a large number of invalid samples: type mismatches, unreachable resources, incorrectly constructed parameters, and bottlenecks in the call chain—ultimately, what you get is not test coverage, but a bunch of "failures right from the start."

Belobog's method is more like equipping the fuzzer with a "map." It starts from Move's type system to construct a type graph based on type semantics for the target contract, and then generates or mutates transaction sequences based on this graph. In other words, it does not blindly stitch calls together but constructs more reasonable, executable, and deeper-reaching calling combinations along type relationships.

For security research, this change brings not "fancier algorithms," but very simple yet critical benefits:

A higher ratio of valid samples, greater exploration efficiency, and a better chance of reaching those deep paths where real vulnerabilities often appear.

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

In real Move contracts, key logic is often surrounded by layers of checks, assertions, and constraints. If you rely solely on traditional mutation, you can easily bump back and forth at the door: conditions are never satisfied, branches are never entered, and states are never reached.

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

On one hand, it maintains "runnable" concrete execution, while on the other hand, it uses symbolic reasoning to more directionally approach those branch conditions, thus effectively penetrating complex checks and advancing coverage depth.

This is particularly important for the Move ecosystem because the "sense of security" of Move contracts is often built on multiple layers of constraints, while the real issues often hide in the gaps between these constraints. What Belobog aims to do is push testing into these gaps.

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

We do not want this kind of work to stop at "being able to run a demo." Belobog's evaluation directly targets real projects and real vulnerability conclusions. According to the experimental results in the paper: Belobog evaluated 109 real-world Move smart contract projects, and the results showed that Belobog could detect 100% of Critical vulnerabilities and 79% of Major vulnerabilities confirmed by human security experts.

What is even more noteworthy is that Belobog can reproduce complete attacks (full exploits) in real on-chain events without relying on prior knowledge of vulnerabilities. The value of this capability lies in its closer alignment with the situations we face in real offensive and defensive scenarios: attackers do not succeed through "single-point function errors," but through complete paths and state evolution.

What this work aims to express is not just "creating a tool."

This paper is worth reading not only because it proposes a new framework but also because it represents a more pragmatic direction: abstracting frontline security experience into reusable methods and implementing it with verifiable engineering.

We believe the significance of Belobog lies not in being "another fuzzer," but in bringing fuzzing closer to reality in Move—capable of running, delving deeper, and being closer to real attack paths. Belobog is not a closed tool designed for a few security experts, but a developer-friendly framework: it aims to lower the barriers to use, allowing developers to continuously introduce security testing into familiar development processes, rather than making fuzzing a one-time, post-factum task.

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

Paper (preprint): https://arxiv.org/abs/2512.02918

(At the same time, this work is being submitted to PLDI’26 and is awaiting peer review.)

About MoveBit

MoveBit (Mobi Security), a sub-brand of BitsLab, is a blockchain security company focused on the Move ecosystem, making it the safest Web3 ecosystem by being the first to use formal verification. MoveBit has collaborated with many well-known projects globally and provided comprehensive security auditing services to its partners. The MoveBit team consists of leading figures in security from academia and industry, with 10 years of security experience, having published security research results at top international security conferences such as NDSS and CCS. They are also among the earliest contributors to the Move ecosystem, working with Move developers to establish standards for secure Move applications.

免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。