Análisis de la seguridad del lenguaje Move

El lenguaje Move, como un lenguaje de contratos inteligentes de nueva generación, se caracteriza principalmente por su seguridad. Este artículo analiza la seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de ejecución y herramientas de verificación.

1. Características de seguridad del lenguaje Move

El lenguaje Move fue diseñado teniendo en cuenta los problemas de seguridad de blockchain y contratos inteligentes, y se basó en el diseño de seguridad del lenguaje Rust. A diferencia de muchos lenguajes de programación existentes, Move abandona la lógica no lineal basada en la flexibilidad, no admite la dispatch dinámica ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar un modelo de programación alternativo.

Las principales características de seguridad de Move incluyen:

• Módulo (Module): compuesto por tipos de estructura y definiciones de procesos, puede importar definiciones de tipos y procesos de otros módulos.

• Estructura (Structs): puede definirse como un tipo de recurso, almacenado en un almacenamiento global de clave/valor.

• Proceso (Función ): define la inicialización, el proceso seguro y el proceso no seguro.

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

• Comprobación de invariantes: se pueden definir invariantes para la verificación estática, garantizando la conservación del estado del sistema.

• Verificador de bytecode: impone un sistema de tipos a nivel de bytecode, previniendo operaciones ilegales.

2. Mecanismo de funcionamiento de Move

El programa Move se ejecuta en una máquina virtual y no puede acceder directamente a la memoria del sistema. El programa se ejecuta en la pila, y el almacenamiento global se divide en dos partes: memoria (, pila ) y variables globales (.

Las instrucciones de bytecode de Move se ejecutan en un intérprete basado en pila. El estado del programa está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Los valores de recursos solo pueden ser movidos de manera destructiva, ciertos valores ) como los enteros ( pueden ser copiados.

MoveVM separa el almacenamiento de datos y la pila de llamadas, a diferencia de EVM. Este diseño mejora significativamente la seguridad y la eficiencia de ejecución, pero sacrifica cierta flexibilidad.

![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 que utiliza algoritmos de verificación deductiva para comprobar si el programa cumple con las expectativas. Su flujo de trabajo es el siguiente:

1. Recibir el archivo fuente de Move y las especificaciones como entrada
2. Normas de extracción, compilar archivos fuente a código de bytes
3. Convertir al modelo de objeto validador
4. Traducir al idioma intermedio de Boogie
5. Generar condiciones de verificación
6. Utilizar el solucionador Z3 para verificar fórmulas SMT
7. Generar informe de diagnóstico

El Lenguaje de Especificación Move se utiliza para describir especificaciones, y es un subconjunto del lenguaje Move. Se pueden escribir especificaciones de forma independiente, sin afectar al código 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 se destaca en el diseño de seguridad, considerando de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Puede evitar eficazmente vulnerabilidades comunes en EVM, como la reentrada y el desbordamiento, pero aún es necesario prestar atención a problemas de autenticación y lógica.

Aunque Move tiene grandes ventajas en términos de seguridad, no existe un lenguaje y programa completamente seguros. Se recomienda a los desarrolladores que sigan utilizando auditorías de seguridad de terceros y que un equipo de seguridad profesional escriba y verifique el código normativo.

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