Análisis de la seguridad del lenguaje Move: el revolucionario del lenguaje de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que puede ejecutarse en un entorno de blockchain que implemente MoveVM. Desde su diseño inicial, se han considerado muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y se ha hecho referencia al diseño de seguridad del lenguaje RUST. Como un nuevo lenguaje de contratos inteligentes con características de seguridad como principal atributo, ¿cuál es su nivel de seguridad? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad específicos en sí mismo?
Este artículo explorará el problema de 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 lenguaje Move fue diseñado para soportar tanto la escritura de programas que interactúan de manera segura con código no confiable, como para soportar la verificación estática. Move posee estas características de seguridad porque ha abandonado la lógica no lineal basada en consideraciones de flexibilidad, no soporta la dispatch dinámica, ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de programación dinámica y llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes conducen a costosas vulnerabilidades de reentrada.
Las principales características de seguridad de Move incluyen:
módulo (Module): cada módulo Move está compuesto por una serie de definiciones de tipos de estructura y procedimientos. Los módulos pueden importar definiciones de tipos y llamar a procedimientos declarados en otros módulos.
Estructura (Structs): se puede definir como un tipo de recurso, que indica que se puede almacenar en un almacenamiento persistente de clave/valor global.
proceso ( Función ): define la lógica de negocio del contrato.
Almacenamiento global: permite que el programa Move almacene datos persistentes, los cuales solo pueden ser leídos/escritos programáticamente por el módulo que los posee.
Comprobación de invariantes: se pueden definir invariantes de comprobación estática que representan la conservación de recursos en el sistema.
validador de bytecode: realiza validaciones de tipo de seguridad y linealización sobre el bytecode, imponiendo reglas para la creación, destrucción y acceso a recursos.
A través de estas características, Move puede garantizar una alta seguridad en tiempo de compilación. A continuación, analizaremos el mecanismo de funcionamiento de Move y veremos cómo MoveVM garantiza la seguridad en tiempo de ejecución.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, y durante su ejecución no puede acceder a la memoria del sistema. Esto permite que Move se ejecute de manera segura en entornos no confiables, sin ser comprometido ni abusado.
El programa Move se ejecuta en la pila. 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 que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, pero el método de indexación es diferente al de la memoria.
Las instrucciones de bytes de Move se ejecutan en un intérprete basado en pila. La máquina virtual basada en pila es fácil de implementar y controlar, requiere menos recursos del entorno de hardware, y es adecuada para escenarios de blockchain. Al mismo tiempo, en comparación con el intérprete basado en registros, el intérprete basado en pila facilita más el control y la detección de copias y movimientos entre variables.
El estado de ejecución del programa Move es un cuádruple ⟨C, M, G, S⟩, compuesto por 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 cuerpos de funciones.
La pila de llamadas contiene toda la información contextual y los números de instrucción de la ejecución del proceso. Se crea un nuevo objeto de pila de llamadas al ejecutar la instrucción Call, almacenando los parámetros de llamada y luego ejecutando las instrucciones del nuevo contrato. Al encontrar una instrucción de bifurcación, se realiza un salto estático dentro del proceso. Este diseño evita el despacho dinámico, refuerza la inmutabilidad de las llamadas a funciones, evitando así la posibilidad de reentrada.
MoveVM separa el almacenamiento de datos y la lógica del proceso de la pila de llamadas ) (, lo cual es la mayor diferencia con EVM. En MoveVM, los recursos ) bajo la dirección de la cuenta de estado del usuario ( se almacenan de forma independiente, y las llamadas a programas deben cumplir con las reglas obligatorias relacionadas con permisos y recursos. Este diseño, aunque sacrifica cierta flexibilidad, ha logrado una gran mejora 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-372ff914a241634ca57784dc9685a03d.webp(
3. Mover Prover
Move Prover es una herramienta de verificación formal basada en la inferencia. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de inferencia para verificar si el programa cumple con las expectativas, ayudando a los desarrolladores a garantizar la corrección de los contratos inteligentes, reduciendo así el riesgo de transacciones.
Move Prover utiliza algoritmos de verificación deductiva para validar si un programa cumple con las expectativas. Puede inferir el comportamiento del programa en función de la información conocida y asegurarse de que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reduce la carga de trabajo de las pruebas manuales.
El flujo de trabajo de Move Prover es el siguiente:
Recibir el archivo fuente Move como entrada, en el cual se deben establecer las especificaciones de entrada del programa.
Move Parser extrae la especificación del código fuente.
El compilador Move compila el archivo fuente en bytecode, transformándolo junto con el sistema de referencia en un modelo de objeto de validador.
El modelo se traduce al lenguaje intermedio Boogie.
El sistema de verificación Boogie genera "condiciones de verificación" para la entrada.
Pasar las condiciones de verificación al solucionador Z3 para su revisión.
Si la norma se establece, la verificación es correcta; de lo contrario, se genera un informe de diagnóstico.
Para describir un sistema de especificaciones, Move utiliza el Lenguaje de Especificación Move, que es un subconjunto del lenguaje Move, e introduce soporte para la descripción estática del comportamiento correcto del programa. El Lenguaje de Especificación Move puede existir de forma independiente como documentos de especificación especializados, lo que permite separar el código de negocio del código de verificación formal.
Move Prover es una herramienta muy útil que puede ayudar a los desarrolladores a asegurar la corrección de los contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de inferencia para verificar si el programa cumple con las expectativas. Esto ayuda a reducir el riesgo de transacciones, permitiendo a los desarrolladores desplegar contratos inteligentes en un entorno de producción con más confianza.
![Análisis de la seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Resumen
El lenguaje Move se destaca en el diseño de seguridad, proporcionando consideraciones exhaustivas en las características del lenguaje, la ejecución de la máquina virtual y la capa de herramientas de seguridad. En las características del lenguaje, se sacrifica cierta flexibilidad, forzando la verificación de tipos y la lógica lineal, lo que facilita una mayor automatización y verificabilidad de seguridad durante la verificación 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 la seguridad de los activos en la blockchain.
A nivel de lenguaje, Move puede evitar de manera efectiva vulnerabilidades comunes en EVM como reentradas, desbordamientos, inyecciones de Call/DelegateCall, etc. Sin embargo, problemas como la autenticación, la lógica del código y el desbordamiento de estructuras de enteros grandes aún requieren atención adicional por parte de los desarrolladores. Aunque Move Prover es poderoso, puede no funcionar si se descuida el sentido general.
A pesar de que el lenguaje Move ha considerado muchos aspectos de seguridad para los programadores, no existe un lenguaje y un programa completamente seguros. Se recomienda a los desarrolladores de contratos inteligentes de Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que dejen la redacción y verificación de partes del código de especificación a empresas de seguridad de terceros, para aumentar aún más la seguridad del contrato.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
Análisis profundo de la seguridad del lenguaje Move: el nuevo estándar para el desarrollo de contratos inteligentes
Análisis de la seguridad del lenguaje Move: el revolucionario del lenguaje de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que puede ejecutarse en un entorno de blockchain que implemente MoveVM. Desde su diseño inicial, se han considerado muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y se ha hecho referencia al diseño de seguridad del lenguaje RUST. Como un nuevo lenguaje de contratos inteligentes con características de seguridad como principal atributo, ¿cuál es su nivel de seguridad? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad específicos en sí mismo?
Este artículo explorará el problema de 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 lenguaje Move fue diseñado para soportar tanto la escritura de programas que interactúan de manera segura con código no confiable, como para soportar la verificación estática. Move posee estas características de seguridad porque ha abandonado la lógica no lineal basada en consideraciones de flexibilidad, no soporta la dispatch dinámica, ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de programación dinámica y llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes conducen a costosas vulnerabilidades de reentrada.
Las principales características de seguridad de Move incluyen:
módulo (Module): cada módulo Move está compuesto por una serie de definiciones de tipos de estructura y procedimientos. Los módulos pueden importar definiciones de tipos y llamar a procedimientos declarados en otros módulos.
Estructura (Structs): se puede definir como un tipo de recurso, que indica que se puede almacenar en un almacenamiento persistente de clave/valor global.
proceso ( Función ): define la lógica de negocio del contrato.
Almacenamiento global: permite que el programa Move almacene datos persistentes, los cuales solo pueden ser leídos/escritos programáticamente por el módulo que los posee.
Comprobación de invariantes: se pueden definir invariantes de comprobación estática que representan la conservación de recursos en el sistema.
validador de bytecode: realiza validaciones de tipo de seguridad y linealización sobre el bytecode, imponiendo reglas para la creación, destrucción y acceso a recursos.
A través de estas características, Move puede garantizar una alta seguridad en tiempo de compilación. A continuación, analizaremos el mecanismo de funcionamiento de Move y veremos cómo MoveVM garantiza la seguridad en tiempo de ejecución.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, y durante su ejecución no puede acceder a la memoria del sistema. Esto permite que Move se ejecute de manera segura en entornos no confiables, sin ser comprometido ni abusado.
El programa Move se ejecuta en la pila. 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 que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, pero el método de indexación es diferente al de la memoria.
Las instrucciones de bytes de Move se ejecutan en un intérprete basado en pila. La máquina virtual basada en pila es fácil de implementar y controlar, requiere menos recursos del entorno de hardware, y es adecuada para escenarios de blockchain. Al mismo tiempo, en comparación con el intérprete basado en registros, el intérprete basado en pila facilita más el control y la detección de copias y movimientos entre variables.
El estado de ejecución del programa Move es un cuádruple ⟨C, M, G, S⟩, compuesto por 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 cuerpos de funciones.
La pila de llamadas contiene toda la información contextual y los números de instrucción de la ejecución del proceso. Se crea un nuevo objeto de pila de llamadas al ejecutar la instrucción Call, almacenando los parámetros de llamada y luego ejecutando las instrucciones del nuevo contrato. Al encontrar una instrucción de bifurcación, se realiza un salto estático dentro del proceso. Este diseño evita el despacho dinámico, refuerza la inmutabilidad de las llamadas a funciones, evitando así la posibilidad de reentrada.
MoveVM separa el almacenamiento de datos y la lógica del proceso de la pila de llamadas ) (, lo cual es la mayor diferencia con EVM. En MoveVM, los recursos ) bajo la dirección de la cuenta de estado del usuario ( se almacenan de forma independiente, y las llamadas a programas deben cumplir con las reglas obligatorias relacionadas con permisos y recursos. Este diseño, aunque sacrifica cierta flexibilidad, ha logrado una gran mejora 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-372ff914a241634ca57784dc9685a03d.webp(
3. Mover Prover
Move Prover es una herramienta de verificación formal basada en la inferencia. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de inferencia para verificar si el programa cumple con las expectativas, ayudando a los desarrolladores a garantizar la corrección de los contratos inteligentes, reduciendo así el riesgo de transacciones.
Move Prover utiliza algoritmos de verificación deductiva para validar si un programa cumple con las expectativas. Puede inferir el comportamiento del programa en función de la información conocida y asegurarse de que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reduce la carga de trabajo de las pruebas manuales.
El flujo de trabajo de Move Prover es el siguiente:
Para describir un sistema de especificaciones, Move utiliza el Lenguaje de Especificación Move, que es un subconjunto del lenguaje Move, e introduce soporte para la descripción estática del comportamiento correcto del programa. El Lenguaje de Especificación Move puede existir de forma independiente como documentos de especificación especializados, lo que permite separar el código de negocio del código de verificación formal.
Move Prover es una herramienta muy útil que puede ayudar a los desarrolladores a asegurar la corrección de los contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de inferencia para verificar si el programa cumple con las expectativas. Esto ayuda a reducir el riesgo de transacciones, permitiendo a los desarrolladores desplegar contratos inteligentes en un entorno de producción con más confianza.
![Análisis de la seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Resumen
El lenguaje Move se destaca en el diseño de seguridad, proporcionando consideraciones exhaustivas en las características del lenguaje, la ejecución de la máquina virtual y la capa de herramientas de seguridad. En las características del lenguaje, se sacrifica cierta flexibilidad, forzando la verificación de tipos y la lógica lineal, lo que facilita una mayor automatización y verificabilidad de seguridad durante la verificación 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 la seguridad de los activos en la blockchain.
A nivel de lenguaje, Move puede evitar de manera efectiva vulnerabilidades comunes en EVM como reentradas, desbordamientos, inyecciones de Call/DelegateCall, etc. Sin embargo, problemas como la autenticación, la lógica del código y el desbordamiento de estructuras de enteros grandes aún requieren atención adicional por parte de los desarrolladores. Aunque Move Prover es poderoso, puede no funcionar si se descuida el sentido general.
A pesar de que el lenguaje Move ha considerado muchos aspectos de seguridad para los programadores, no existe un lenguaje y un programa completamente seguros. Se recomienda a los desarrolladores de contratos inteligentes de Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que dejen la redacción y verificación de partes del código de especificación a empresas de seguridad de terceros, para aumentar aún más la seguridad del contrato.