Ricerca di MoveBit di BitsLab pubblicata｜Belobog: un framework di fuzzing Move orientato ad attacchi reali

Autore: BitsLab

Move, come linguaggio che gli sviluppatori Web3 non possono ignorare, è estremamente “hardcore” in termini di sistema di tipi forti e semantica delle risorse, specialmente per quanto riguarda la proprietà degli asset, i trasferimenti illeciti e la concorrenza sui dati.

Gli ecosistemi come Sui e Aptos stanno affidando sempre più asset chiave e protocolli core a Move, proprio grazie alle sue caratteristiche fondamentali che permettono di costruire smart contract più sicuri e con minori rischi.

Tuttavia, dalla nostra esperienza di lungo termine in audit e pratiche di attacco-difesa, abbiamo osservato che una grande parte dei problemi più insidiosi non si verifica in punti evidenti come “errori di sintassi” o “incompatibilità di tipo”, ma piuttosto a livello di sistema, in scenari più complessi e realistici: interazione tra moduli, assunzioni sui permessi, confini delle macchine a stati, e sequenze di chiamate che, pur essendo ragionevoli singolarmente, possono essere sfruttate se combinate.

Proprio per questo motivo, anche se il linguaggio Move offre paradigmi di sicurezza più avanzati, nell’ecosistema si sono comunque verificati attacchi di grande impatto. È evidente che la ricerca sulla sicurezza di Move deve ancora progredire.

Abbiamo individuato un problema centrale: nel linguaggio Move manca uno strumento efficace di fuzzing. Poiché Move impone vincoli più stringenti, il fuzzing tradizionale per smart contract si scontra con una difficoltà cruciale: generare sequenze di transazioni “tipate correttamente” e “semanticamente raggiungibili” è estremamente complesso. Se l’input non è abbastanza preciso, la chiamata non può essere completata; senza chiamata, non si possono coprire i rami profondi né raggiungere stati critici, aumentando il rischio di perdere i percorsi che realmente possono attivare vulnerabilità.

Per rispondere a questa esigenza di lungo termine, abbiamo collaborato con team di ricerca universitari e pubblicato insieme i risultati:

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

arXiv:2512.02918 (preprint)

Questo articolo è attualmente pubblicato su arXiv come preprint, con l’obiettivo di permettere alla community di vedere rapidamente i progressi della ricerca e fornire feedback. Stiamo sottoponendo il lavoro a PLDI’26 e attendiamo il processo di peer review. Una volta confermato l’esito della sottomissione e completata la revisione tra pari, aggiorneremo tempestivamente sugli sviluppi.

Fuzzing che entra davvero in Move: dalla prova casuale alla guida tramite tipi

L’idea centrale di Belobog è molto diretta: dato che il sistema di tipi di Move è il suo vincolo fondamentale, anche il fuzzing dovrebbe considerare i tipi come guida, non come ostacolo.

Le pratiche tradizionali spesso si basano su generazione casuale e mutazione, ma su Move questo porta rapidamente a una grande quantità di campioni non validi: incompatibilità di tipo, risorse irraggiungibili, parametri non costruibili correttamente, blocchi nella catena di chiamate—alla fine non si ottiene copertura di test, ma solo una serie di “fallimenti alla partenza”.

Il metodo di Belobog è come dotare il fuzzer di una “mappa”. Parte dal sistema di tipi di Move per costruire, per il contratto target, un type graph basato sulla semantica dei tipi, e su questa base genera o muta le sequenze di transazioni. In altre parole, non concatena chiamate alla cieca, ma costruisce combinazioni di chiamate più ragionevoli, eseguibili e capaci di esplorare in profondità lo spazio degli stati, seguendo le relazioni tra tipi.

Per la ricerca sulla sicurezza, questo cambiamento non porta “algoritmi più sofisticati”, ma vantaggi molto semplici e fondamentali:

Una percentuale più alta di campioni validi, maggiore efficienza nell’esplorazione e più possibilità di raggiungere quei percorsi profondi dove spesso si annidano le vere vulnerabilità.

Affrontare vincoli complessi: Belobog introduce la Concolic Execution per “aprire le porte”

Nei veri smart contract Move, la logica chiave è spesso circondata da controlli, asserzioni e vincoli a più livelli. Se ci si basa solo sulla mutazione tradizionale, si rischia di sbattere continuamente contro la porta: le condizioni non vengono mai soddisfatte, i rami non vengono mai raggiunti, gli stati non vengono mai toccati.

Per risolvere questo problema, Belobog ha progettato e implementato la concolic execution (esecuzione concreta + deduzione simbolica). In parole semplici:

Da un lato mantiene l’esecuzione concreta “che può essere eseguita”, dall’altro utilizza la deduzione simbolica per avvicinarsi in modo più mirato alle condizioni dei rami, penetrando così controlli complessi e aumentando la profondità della copertura.

Questo è particolarmente importante per l’ecosistema Move, perché la “sensazione di sicurezza” dei contratti Move si basa spesso su vincoli multilivello, mentre i problemi reali si nascondono spesso nelle intersezioni tra questi vincoli. L’obiettivo di Belobog è portare i test proprio vicino a queste intersezioni.

Allinearsi al mondo reale: non solo demo funzionanti, ma avvicinarsi ai veri percorsi di attacco

Non vogliamo che questo tipo di lavoro si limiti a “far funzionare una demo”. La valutazione di Belobog si rivolge direttamente a progetti reali e a conclusioni su vulnerabilità reali. Secondo i risultati sperimentali riportati nell’articolo: Belobog è stato valutato su 109 progetti reali di smart contract Move, dimostrando di poter rilevare il 100% delle vulnerabilità Critical e il 79% delle vulnerabilità Major confermate da esperti di sicurezza umani.

Ancora più rilevante: Belobog, senza basarsi su conoscenze pregresse delle vulnerabilità, è in grado di riprodurre exploit completi (full exploits) su eventi reali on-chain. Questo è prezioso perché riflette meglio la situazione reale negli scenari di attacco-difesa: gli attaccanti non si affidano a “errori di singole funzioni”, ma a percorsi completi e all’evoluzione degli stati.

Il messaggio di questo lavoro non è solo “abbiamo creato uno strumento”

Questo articolo vale la pena di essere letto non solo perché propone un nuovo framework, ma perché rappresenta una direzione più pragmatica: astrarre l’esperienza di sicurezza di prima linea in metodi riutilizzabili e realizzarli con implementazioni ingegneristiche verificabili.

Crediamo che il valore di Belobog non sia “un altro fuzzer”, ma il fatto che avvicina il fuzzing su Move alla realtà—può entrare, andare in profondità e avvicinarsi ai veri percorsi di attacco. Belobog non è uno strumento chiuso progettato per pochi esperti di sicurezza, ma un framework developer-friendly: abbassa il più possibile la soglia d’uso, permettendo agli sviluppatori di integrare test di sicurezza nel normale flusso di sviluppo, invece di relegare il fuzzing a un’attività occasionale e postuma.

Rilasceremo anche Belobog come open source, sperando che diventi un’infrastruttura che la community possa usare, estendere ed evolvere insieme, e non solo un progetto sperimentale a livello di “strumento”.

Articolo (preprint):

(Il lavoro è anche in fase di sottomissione a PLDI’26, in attesa di peer review.)

Informazioni su MoveBit

MoveBit (Mobi Security), sub-brand di BitsLab, è una società di sicurezza blockchain focalizzata sull’ecosistema Move, che ha reso Move il più sicuro ecosistema Web3 grazie all’uso pionieristico della verifica formale. MoveBit ha già collaborato con numerosi progetti di fama mondiale, offrendo servizi di audit di sicurezza completi ai partner. Il team di MoveBit è composto da esperti di sicurezza sia accademici che industriali, con 10 anni di esperienza e pubblicazioni in conferenze di sicurezza di livello mondiale come NDSS e CCS. Sono anche tra i primi contributori dell’ecosistema Move, collaborando con gli sviluppatori Move per definire gli standard delle applicazioni Move sicure.