Análisis de seguridad del lenguaje Move: Innovador en el campo de los contratos inteligentes

El lenguaje Move es un lenguaje de contratos inteligentes que puede ejecutarse en entornos de blockchain que admiten MoveVM. Su diseño considera muchos problemas de seguridad de blockchain y contratos inteligentes, y se inspira en algunos conceptos de diseño de seguridad del lenguaje Rust. Como un lenguaje de contratos inteligentes de nueva generación centrado en la seguridad, ¿cuál es la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mecanismos relacionados? ¿Existen riesgos de seguridad únicos en Move?

Este artículo explorará el problema de la seguridad del lenguaje Move desde tres aspectos: las características del lenguaje, el mecanismo de funcionamiento y las herramientas de verificación.

1. Características de seguridad del lenguaje Move

A diferencia de muchos lenguajes de programación existentes, el objetivo de diseño del lenguaje Move es soportar la creación de programas que puedan interactuar de manera segura con código no confiable, al mismo tiempo que permite la verificación estática. Move ha descartado la lógica no lineal basada en la flexibilidad, no soporta la despachación dinámica ni las llamadas recursivas externas, sino que introduce conceptos como genéricos, almacenamiento global y recursos para lograr un modelo de programación alternativo. Por ejemplo, Move omite las características de programación dinámica y llamadas recursivas, que en otros lenguajes de contratos inteligentes pueden llevar a costosas vulnerabilidades de reentrada.

Las características de seguridad clave de Move incluyen:

1. Módulo: cada módulo Move consiste en una serie de definiciones de tipos de estructura y procesos. Los módulos pueden importar definiciones de tipos declarados en otros módulos y llamar a procesos.

2. Estructura: se puede definir como un tipo de recurso, que representa lo que se puede almacenar en un almacenamiento persistente de clave/valor global.

3. Proceso: definir la funcionalidad y la lógica del módulo.

4. Almacenamiento global: permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos de manera programática por el módulo que los posee.

5. Comprobación de invariante: se pueden definir invariantes de comprobación estática para garantizar la conservación del estado del sistema.

6. validador de bytecode: aplica un sistema de tipos a nivel de bytecode para prevenir operaciones ilegales.

A través de estas características de seguridad, Move proporciona un entorno de programación más seguro y confiable para el desarrollo de contratos inteligentes.

2. Mecanismo de funcionamiento de Move

El programa Move se ejecuta en una máquina virtual y no puede acceder a la memoria del sistema durante su ejecución, lo que permite que Move funcione de manera segura en entornos no confiables.

El programa Move se ejecuta en la pila, y el almacenamiento global se divide en dos partes: memoria (, pila ) y variables globales (. La memoria es un almacenamiento de primer orden y no puede almacenar punteros a unidades de memoria. Las variables globales se utilizan para almacenar punteros a unidades de memoria, pero el método de indexación es diferente al de la memoria.

Las instrucciones de bytecode de Move se ejecutan en un intérprete basado en pila. En comparación con un intérprete basado en registros, un intérprete basado en pila es más fácil de controlar y detectar las operaciones de copia y movimiento entre variables.

El estado de ejecución del programa Move está representado por una cuádruple ⟨C, M, G, S⟩, que incluye la pila de llamadas )C(, la memoria )M(, las variables globales )G( y los operandos )S(. La pila también mantiene una tabla de funciones para resolver las instrucciones que contienen el cuerpo de la función.

MoveVM separa la lógica del proceso de almacenamiento de datos y la pila de llamadas ), que es la principal diferencia con EVM. Los recursos bajo la dirección de la cuenta del estado del usuario ( se almacenan de forma independiente, y las llamadas de programa deben cumplir con reglas obligatorias relacionadas con permisos y recursos. Aunque este diseño sacrifica cierta flexibilidad, ha logrado una mejora significativa en seguridad y eficiencia de ejecución.

![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. Mover Prover

Move Prover es una herramienta de verificación formal basada en razonamiento, que utiliza un lenguaje formal para describir el comportamiento del programa y un algoritmo de razonamiento para verificar si el programa cumple con lo esperado. Puede ayudar a los desarrolladores a asegurar la corrección de los contratos inteligentes, reduciendo el riesgo de transacciones.

Move Prover utiliza un algoritmo de verificación deductiva para inferir el comportamiento del programa según la información conocida, asegurando que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y a reducir la carga de trabajo de las pruebas manuales.

El flujo de trabajo de Move Prover es el siguiente:

1. Recibir el archivo fuente Move como entrada, que contiene las especificaciones de entrada del programa.

2. Mover Parser extrae las normas del código fuente.

3. El compilador Move compila el archivo fuente a bytecode, que se transforma junto con el sistema de referencia en un modelo de objeto de validador.

4. El modelo de objetos se traduce al lenguaje intermedio Boogie.

5. El sistema de verificación Boogie genera "condiciones de verificación" para la entrada.

6. Se pasan las condiciones de verificación al solucionador Z3 ), el solucionador SMT desarrollado por Microsoft (.

7. Z3 verifica si la fórmula SMT es insatisfacible. Si es así, significa que la especificación es válida; de lo contrario, genera un modelo que satisface las condiciones.

8. Restaurar el informe de diagnóstico a errores a nivel de código fuente.

Move utiliza el Lenguaje de Especificación Move para describir las especificaciones del sistema, que es un subconjunto del lenguaje Move, y admite la descripción estática del comportamiento correcto del programa, sin afectar la producción. Las especificaciones se pueden escribir de forma independiente, facilitando la separación del código de negocio y el código de verificación formal.

Move Prover es una herramienta poderosa que ayuda a los desarrolladores a garantizar la corrección de los contratos inteligentes, reducir el riesgo de transacciones y aumentar la confianza en el despliegue de contratos inteligentes en entornos de producción.

![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

4. Resumen

El lenguaje Move tiene un diseño de seguridad excepcional, considerando de manera integral desde las características del lenguaje, la ejecución de la máquina virtual, hasta las herramientas de seguridad. Las características del lenguaje sacrifican parte de la flexibilidad, con verificación de tipos estricta y lógica lineal, lo que favorece la automatización y la verificabilidad de las comprobaciones de compilación y la validación formal. El diseño de MoveVM separa el estado de la lógica, lo que se adapta mejor a las necesidades de gestión de seguridad de los activos en blockchain.

A nivel de lenguaje, Move puede evitar eficazmente vulnerabilidades comunes en EVM como la reentrada, desbordamiento, inyección de Call/DeleGateCall, entre otros. Sin embargo, problemas como la autenticación, la lógica del código y el desbordamiento de estructuras de enteros grandes aún deben ser manejados con cautela por los desarrolladores. Aunque Move Prover es poderoso, puede no funcionar si hay descuidos en el diseño general.

A pesar de que el lenguaje Move ofrece múltiples garantías de seguridad a los programadores, no existe un lenguaje y programa completamente seguros. Se recomienda que los desarrolladores de contratos inteligentes Move sigan utilizando servicios de auditoría de empresas de seguridad de terceros y que la redacción y verificación de la parte de especificación del código sean realizadas por un equipo de seguridad profesional, para mejorar aún más la seguridad del contrato.

![Análisis de seguridad de Move: un cambio de juego en el lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(