Autor: BitsLab
Move, como un lenguaje que los desarrolladores de Web3 no pueden ignorar, es muy "hardcore" en cuanto a su sistema de tipos fuerte y semántica de recursos, especialmente en temas como la propiedad de activos, transferencias ilegales y competencia de datos.
Ecologías como Sui y Aptos están colocando cada vez más activos clave y protocolos centrales en Move, precisamente por las características fundamentales del lenguaje Move, que permiten construir contratos inteligentes más seguros y con menos riesgos.
Sin embargo, en nuestra experiencia a largo plazo en auditoría y prácticas de defensa y ataque, hemos observado que muchos de los problemas más difíciles no ocurren en lugares obvios como "errores de sintaxis" o "incompatibilidad de tipos", sino en niveles de sistema más complejos y reales: interacción entre módulos, supuestos de permisos, límites de máquinas de estado, y esas secuencias de llamadas que, aunque cada paso parece razonable por separado, pueden ser explotadas cuando se combinan.
Por eso, aunque el lenguaje Move tiene un paradigma de seguridad más completo, aún han ocurrido incidentes de ataques significativos en su ecosistema. Claramente, la investigación de seguridad en Move aún debe avanzar más.
Hemos detectado un problema central: en el lenguaje Move, falta una herramienta eficaz de fuzzing (pruebas aleatorias). Debido a que Move tiene restricciones más estrictas, el fuzzing tradicional de contratos inteligentes enfrenta un problema complicado en el contexto de Move: generar secuencias de transacciones que sean "correctas en tipo" y "alcanzables semánticamente" es muy complejo. Si las entradas no son lo suficientemente precisas, la llamada no se puede completar; si no se puede llamar, no se pueden cubrir ramas profundas ni alcanzar estados críticos, lo que aumenta la probabilidad de pasar por alto rutas que realmente podrían activar vulnerabilidades.
Basándonos en este problema de larga data, colaboramos con equipos de investigación universitarios para completar y publicar los siguientes resultados:
《Belobog: Move Language Fuzzing Framework For Real-World Smart Contracts》
arXiv:2512.02918 (preprint)
Enlace al paper:
Este artículo está actualmente publicado en arXiv como preprint, lo que permite que la comunidad vea el progreso de la investigación y brinde retroalimentación más rápidamente. Estamos enviando este trabajo a PLDI’26 y esperando el proceso de peer review. Una vez que se confirme el resultado de la presentación y se complete la revisión por pares, compartiremos el progreso relevante de inmediato.
Haciendo que el Fuzzing realmente "entre" en Move: de prueba y error aleatorio a guía por tipos
La idea central de Belobog es muy directa: dado que el sistema de tipos de Move es su restricción fundamental, el fuzzing también debe tomar los tipos como guía, no como obstáculo.
El enfoque tradicional muchas veces depende de la generación y mutación aleatoria, pero en Move esto rápidamente genera una gran cantidad de muestras inválidas: incompatibilidad de tipos, recursos inalcanzables, parámetros que no se pueden construir correctamente, cuellos de botella en la cadena de llamadas; al final, lo que obtienes no es cobertura de pruebas, sino un montón de "fallos en la línea de salida".
El método de Belobog es más bien como darle un "mapa" al fuzzer. Parte del sistema de tipos de Move para construir un type graph basado en la semántica de tipos para el contrato objetivo, y luego genera o muta secuencias de transacciones basándose en ese gráfico. En otras palabras, no concatena llamadas a ciegas, sino que construye combinaciones de llamadas más razonables, ejecutables y que pueden explorar más profundamente el espacio de estados, siguiendo las relaciones de tipos.
Para la investigación en seguridad, este cambio no trae "algoritmos más vistosos", sino beneficios muy simples pero clave:
Una mayor proporción de muestras válidas, mayor eficiencia de exploración y más oportunidades de alcanzar esas rutas profundas donde suelen aparecer vulnerabilidades reales.
Frente a restricciones complejas: Belobog introduce Concolic Execution para "abrir la puerta"
En los contratos Move reales, la lógica clave suele estar rodeada de múltiples capas de comprobaciones, aserciones y restricciones. Si solo dependés de la mutación tradicional, es fácil quedarse atascado en la puerta: las condiciones nunca se cumplen, las ramas nunca se alcanzan, el estado nunca se logra.
Para resolver este problema, Belobog diseñó e implementó concolic execution (ejecución concreta + deducción simbólica combinada). En pocas palabras:
Por un lado, mantiene la ejecución concreta "que puede correr", y por otro, utiliza la deducción simbólica para acercarse de manera más dirigida a esas condiciones de ramificación, penetrando así comprobaciones complejas y profundizando la cobertura.
Esto es especialmente importante para el ecosistema Move, ya que la "sensación de seguridad" de los contratos Move suele basarse en múltiples capas de restricciones, pero los problemas reales suelen esconderse en los huecos entre esas restricciones. Lo que Belobog busca es llevar las pruebas a esos huecos.
Alineado con el mundo real: no solo correr un demo, sino acercarse a rutas de ataque reales
No queremos que este tipo de trabajo se quede solo en "poder correr un demo". La evaluación de Belobog se dirige directamente a proyectos reales y conclusiones de vulnerabilidades reales. Según los resultados experimentales del paper: Belobog fue evaluado en 109 proyectos reales de contratos inteligentes Move, y los resultados muestran que Belobog puede detectar el 100% de las vulnerabilidades críticas y el 79% de las vulnerabilidades mayores confirmadas por expertos en seguridad humanos.
Lo más destacable es que: Belobog, sin depender de conocimientos previos sobre vulnerabilidades, puede reproducir ataques completos (full exploits) en eventos reales en la blockchain. El valor de esta capacidad radica en que se acerca más a lo que enfrentamos en la defensa y ataque real: los atacantes no triunfan por un "error puntual en una función", sino por rutas completas y evolución de estados.
Lo que este trabajo quiere expresar no es solo "hicimos una herramienta"
Este paper vale la pena leerlo no solo porque propone un nuevo framework, sino porque representa una dirección más pragmática: abstraer la experiencia de seguridad de primera línea en métodos reutilizables y aterrizarlos con implementaciones de ingeniería verificables.
Creemos que el valor de Belobog no está en ser "otro fuzzer más", sino en acercar el fuzzing en Move a la realidad: que pueda entrar, profundizar y acercarse más a rutas de ataque reales. Belobog no es una herramienta cerrada diseñada solo para unos pocos expertos en seguridad, sino un framework developer-friendly: busca reducir la barrera de uso para que los desarrolladores puedan incorporar pruebas de seguridad de forma continua en su flujo de trabajo habitual, en vez de convertir el fuzzing en una tarea puntual y posterior.
También publicaremos Belobog como open source, esperando que se convierta en una infraestructura que la comunidad pueda usar, expandir y evolucionar en conjunto, y no se quede en un proyecto experimental a nivel de herramienta.
Papel (preprint):
(Al mismo tiempo, este trabajo está siendo enviado a PLDI’26 y está esperando revisión por pares.)
Sobre MoveBit
MoveBit (MoveBit Security), una sub-marca de BitsLab, es una empresa de seguridad blockchain enfocada en el ecosistema Move, que ha convertido a Move en el ecosistema Web3 más seguro al ser pionera en el uso de la verificación formal. MoveBit ya ha colaborado con varios proyectos reconocidos a nivel mundial, brindando servicios de auditoría de seguridad integrales a sus socios. El equipo de MoveBit está compuesto por referentes de seguridad tanto del ámbito académico como empresarial, con 10 años de experiencia en seguridad y publicaciones en conferencias internacionales de primer nivel como NDSS y CCS. Además, son de los primeros contribuyentes al ecosistema Move, colaborando con los desarrolladores de Move en la definición de estándares para aplicaciones Move seguras.
