Análisis de la seguridad del lenguaje Move: el revolucionario del lenguaje de contratos inteligentes
Introducción
El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en un entorno de blockchain que implemente MoveVM. Su diseño considera muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y se basa en parte en los conceptos de diseño de seguridad del lenguaje Rust. Como un lenguaje de contratos inteligentes de nueva generación cuya característica principal es la seguridad, ¿cuál es la seguridad de Move? ¿Puede evitar amenazas de seguridad comunes de máquinas virtuales de contratos como EVM, WASM, etc. a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad particulares en Move?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: las características del lenguaje, el mecanismo de ejecución 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 está diseñado para soportar interacciones seguras con código no confiable y también para soportar la verificación estática. Move deshecha la lógica no lineal basada en consideraciones de flexibilidad, no soporta la despachación dinámica y las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar patrones de programación alternativos. Por ejemplo, Move omite las características de despachado dinámico y llamadas recursivas que podrían conducir a vulnerabilidades de reentrada.
Las principales características de seguridad de Move incluyen:
Módulo: cada módulo de Move consiste en una serie de definiciones de tipos de estructura y procedimientos. Un módulo puede importar definiciones de tipos y llamar a procedimientos declarados en otros módulos.
Estructura: se puede definir como un tipo de recurso, que representa algo que se puede almacenar en un almacenamiento clave/valor global persistente.
Proceso: define la inicialización, el proceso seguro y el proceso inseguro.
Almacenamiento global: permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos de forma programática por el módulo que los posee.
Comprobación de invariante: soporta invariante de comprobación estática, garantizando la integridad de los recursos en el sistema.
validador de bytecode: fuerza el sistema de tipos a nivel de bytecode, previniendo operaciones ilegales de módulos de clientes maliciosos.
A través de dos mecanismos, la verificación de invariantes y el validador de bytes, Move logra una doble garantía de seguridad del código en tiempo de compilación.
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 en tiempo de ejecución. Esto permite que Move se ejecute de manera segura en entornos no confiables, sin ser destruido o abusado.
El programa Move se ejecuta en la pila, y el almacenamiento global se divide en memoria ( pila ) y variables globales (. La memoria es un almacenamiento de primer nivel, cuyas unidades no pueden 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 bytecode de Move se ejecutan en un intérprete basado en pilas. La máquina virtual basada en pilas es fácil de implementar y controlar, requiere menos del entorno de hardware y es adecuada para escenarios de blockchain. En comparación con el intérprete basado en registros, el intérprete basado en pilas facilita el control y la detección de las operaciones de copia y movimiento entre variables.
El estado en tiempo de ejecución del programa Move es una tupla ⟨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 el almacenamiento de datos y la lógica de proceso de la pila de llamadas ), lo que es la mayor diferencia con EVM. En MoveVM, los recursos bajo la dirección de la cuenta de estado del usuario ( se almacenan de manera independiente, y las llamadas a programas deben cumplir con reglas obligatorias relacionadas con permisos y recursos. Este diseño sacrifica cierta flexibilidad, pero contribuye a mejorar significativamente en términos de seguridad y eficiencia de ejecución ), lo que ayuda a lograr la ejecución concurrente (.
![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 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 y reducir el riesgo de transacciones.
Move Prover utiliza algoritmos de verificación deductiva para validar si un programa cumple con las expectativas. Esto significa que puede inferir el comportamiento del programa en función de la información conocida, asegurando que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reducir 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, este archivo debe 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, convirtiéndolo junto con el sistema de especificaciones en un modelo de objeto validador.
El modelo se traduce al lenguaje intermedio Boogie.
El código Boogie se envía al sistema de verificación Boogie para generar las condiciones de verificación.
Pasar las condiciones de verificación al solucionador Z3 ), el solucionador SMT desarrollado por Microsoft (.
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.
Restaurar el informe de diagnóstico a errores a nivel de código fuente.
Move utiliza el Lenguaje de Especificación Move para describir especificaciones del sistema. Es un subconjunto del lenguaje Move, que apoya la descripción estática del comportamiento de corrección del programa, sin afectar a la producción. Se puede escribir de forma independiente como un archivo de especificación especializado, separando el código de negocio y el código de verificación formal.
Move Prover es una herramienta útil que ayuda a los desarrolladores a garantizar la corrección de contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de razonamiento para verificar si el programa cumple con lo esperado, lo que ayuda a reducir el riesgo de transacciones y permite a los desarrolladores desplegar contratos inteligentes en un entorno de producción con mayor confianza.
![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(
4. Resumen
El lenguaje Move se destaca en el diseño de seguridad, ofreciendo una consideración integral en las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Las características del lenguaje sacrifican parte de la flexibilidad, exigiendo verificación de tipos y lógica lineal, lo que facilita la automatización de la verificación de compilación y la validación formal, así como la seguridad verificable. El diseño de MoveVM separa el estado de la lógica, adaptándose 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, entre otras. Sin embargo, los problemas de autenticación, lógica de código y desbordamientos en estructuras de enteros grandes aún requieren la atención de los desarrolladores. Move Prover puede no ser efectivo si se descuida el sentido general.
Aunque el lenguaje Move ha considerado mucho en términos de seguridad para los programadores, no hay un lenguaje o programa completamente seguro. Se recomienda a los desarrolladores de contratos inteligentes de Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que deleguen la redacción y verificación de la parte de especificaciones del código a empresas de seguridad de terceros.
Esta página puede contener contenido de terceros, que se proporciona únicamente con fines informativos (sin garantías ni declaraciones) y no debe considerarse como un respaldo por parte de Gate a las opiniones expresadas ni como asesoramiento financiero o profesional. Consulte el Descargo de responsabilidad para obtener más detalles.
17 me gusta
Recompensa
17
4
Compartir
Comentar
0/400
DegenRecoveryGroup
· hace16h
Hay algo, el sabor a óxido es demasiado fuerte.
Ver originalesResponder0
AlwaysAnon
· 08-06 01:22
Seguridad impresionante, pero el ecosistema es demasiado débil.
Ver originalesResponder0
GasGrillMaster
· 08-06 01:15
¡El movimiento ha comenzado! Solo falta la explosión.
Análisis de seguridad del lenguaje Move: un nuevo paradigma para los contratos inteligentes
Análisis de la seguridad del lenguaje Move: el revolucionario del lenguaje de contratos inteligentes
Introducción
El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en un entorno de blockchain que implemente MoveVM. Su diseño considera muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y se basa en parte en los conceptos de diseño de seguridad del lenguaje Rust. Como un lenguaje de contratos inteligentes de nueva generación cuya característica principal es la seguridad, ¿cuál es la seguridad de Move? ¿Puede evitar amenazas de seguridad comunes de máquinas virtuales de contratos como EVM, WASM, etc. a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad particulares en Move?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: las características del lenguaje, el mecanismo de ejecución 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 está diseñado para soportar interacciones seguras con código no confiable y también para soportar la verificación estática. Move deshecha la lógica no lineal basada en consideraciones de flexibilidad, no soporta la despachación dinámica y las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar patrones de programación alternativos. Por ejemplo, Move omite las características de despachado dinámico y llamadas recursivas que podrían conducir a vulnerabilidades de reentrada.
Las principales características de seguridad de Move incluyen:
Módulo: cada módulo de Move consiste en una serie de definiciones de tipos de estructura y procedimientos. Un módulo puede importar definiciones de tipos y llamar a procedimientos declarados en otros módulos.
Estructura: se puede definir como un tipo de recurso, que representa algo que se puede almacenar en un almacenamiento clave/valor global persistente.
Proceso: define la inicialización, el proceso seguro y el proceso inseguro.
Almacenamiento global: permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos de forma programática por el módulo que los posee.
Comprobación de invariante: soporta invariante de comprobación estática, garantizando la integridad de los recursos en el sistema.
validador de bytecode: fuerza el sistema de tipos a nivel de bytecode, previniendo operaciones ilegales de módulos de clientes maliciosos.
A través de dos mecanismos, la verificación de invariantes y el validador de bytes, Move logra una doble garantía de seguridad del código en tiempo de compilación.
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 en tiempo de ejecución. Esto permite que Move se ejecute de manera segura en entornos no confiables, sin ser destruido o abusado.
El programa Move se ejecuta en la pila, y el almacenamiento global se divide en memoria ( pila ) y variables globales (. La memoria es un almacenamiento de primer nivel, cuyas unidades no pueden 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 bytecode de Move se ejecutan en un intérprete basado en pilas. La máquina virtual basada en pilas es fácil de implementar y controlar, requiere menos del entorno de hardware y es adecuada para escenarios de blockchain. En comparación con el intérprete basado en registros, el intérprete basado en pilas facilita el control y la detección de las operaciones de copia y movimiento entre variables.
El estado en tiempo de ejecución del programa Move es una tupla ⟨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 el almacenamiento de datos y la lógica de proceso de la pila de llamadas ), lo que es la mayor diferencia con EVM. En MoveVM, los recursos bajo la dirección de la cuenta de estado del usuario ( se almacenan de manera independiente, y las llamadas a programas deben cumplir con reglas obligatorias relacionadas con permisos y recursos. Este diseño sacrifica cierta flexibilidad, pero contribuye a mejorar significativamente en términos de seguridad y eficiencia de ejecución ), lo que ayuda a lograr la ejecución concurrente (.
![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 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 y reducir el riesgo de transacciones.
Move Prover utiliza algoritmos de verificación deductiva para validar si un programa cumple con las expectativas. Esto significa que puede inferir el comportamiento del programa en función de la información conocida, asegurando que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reducir la carga de trabajo de las pruebas manuales.
El flujo de trabajo de Move Prover es el siguiente:
Move utiliza el Lenguaje de Especificación Move para describir especificaciones del sistema. Es un subconjunto del lenguaje Move, que apoya la descripción estática del comportamiento de corrección del programa, sin afectar a la producción. Se puede escribir de forma independiente como un archivo de especificación especializado, separando el código de negocio y el código de verificación formal.
Move Prover es una herramienta útil que ayuda a los desarrolladores a garantizar la corrección de contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de razonamiento para verificar si el programa cumple con lo esperado, lo que ayuda a reducir el riesgo de transacciones y permite a los desarrolladores desplegar contratos inteligentes en un entorno de producción con mayor confianza.
![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(
4. Resumen
El lenguaje Move se destaca en el diseño de seguridad, ofreciendo una consideración integral en las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Las características del lenguaje sacrifican parte de la flexibilidad, exigiendo verificación de tipos y lógica lineal, lo que facilita la automatización de la verificación de compilación y la validación formal, así como la seguridad verificable. El diseño de MoveVM separa el estado de la lógica, adaptándose 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, entre otras. Sin embargo, los problemas de autenticación, lógica de código y desbordamientos en estructuras de enteros grandes aún requieren la atención de los desarrolladores. Move Prover puede no ser efectivo si se descuida el sentido general.
Aunque el lenguaje Move ha considerado mucho en términos de seguridad para los programadores, no hay un lenguaje o programa completamente seguro. Se recomienda a los desarrolladores de contratos inteligentes de Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que deleguen la redacción y verificación de la parte de especificaciones del código a empresas de seguridad de terceros.