Análisis de seguridad del lenguaje Move: un cambiador de las reglas del juego para los contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que se puede compilar y ejecutar en entornos de blockchain que implementan MoveVM. Desde su creación, ha considerado numerosos problemas de seguridad en blockchain y contratos inteligentes, y ha tomado prestados algunos diseños de seguridad del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación, cuyo principal característica es la seguridad, ¿cuál es realmente la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes en máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen riesgos de seguridad específicos en sí mismo?
Este artículo explorará los problemas 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 objetivo de diseño del lenguaje Move es soportar la escritura de programas que puedan interactuar de manera segura con código no confiable, al mismo tiempo que permite la verificación estática. Para lograr este objetivo, Move renunció a la lógica no lineal basada en la flexibilidad, no admite la despachación dinámica ni las llamadas externas recursivas, y en su lugar introduce conceptos como genéricos, almacenamiento global, recursos y otros para implementar 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 dar lugar a costosas vulnerabilidades de reentrada.
Las características de seguridad fundamentales de Move incluyen:
módulo (Module): cada módulo Move consiste en una serie de definiciones de tipos estructurales y procesos. Los módulos pueden importar definiciones de tipos declaradas en otros módulos y llamar a procesos.
Estructura(: se puede definir como un tipo de recurso, que representa datos que se pueden almacenar en un almacenamiento clave/valor global persistente.
proceso ) Función (: definir la lógica de comportamiento del módulo.
Almacenamiento global: permite que el programa Move almacene datos persistentes, los cuales solo pueden ser leídos y escritos programáticamente por el módulo que los posee.
Comprobación de invariante: se pueden definir invariantes de verificación estática para garantizar la conservación del estado del sistema.
validador de bytecode: hace cumplir el sistema de tipos a nivel de bytecode, previniendo operaciones ilegales.
Move garantiza la seguridad del código en tiempo de compilación a través de estas características. A continuación, analizaremos el mecanismo de funcionamiento de Move y cómo MoveVM asegura la seguridad en tiempo 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-419437619d55298077789e6eca578b48.webp(
2. Mecanismo de funcionamiento de Move
Los programas Move se ejecutan en una máquina virtual, y durante la ejecución no pueden acceder a la memoria del sistema, lo que permite que Move se ejecute de manera segura en entornos no confiables. Los programas Move se ejecutan en la pila, y el almacenamiento global se divide en memoria ) pila ( y variables globales ) pila (. 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 modo de índice es diferente al de la memoria.
Las instrucciones de bytecode 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, tiene requisitos de hardware más bajos y es adecuada para escenarios de blockchain. 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 la copia y el movimiento entre variables.
Durante la ejecución del programa Move, su estado es un cuádruplo ⟨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 la tabla de funciones ) del módulo en sí ( para resolver las instrucciones que contienen el cuerpo de la función.
MoveVM separa el almacenamiento de datos y la lógica del proceso de la pila de llamadas ), esta 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 al programa deben cumplir con las reglas obligatorias relacionadas con los permisos y los recursos. Aunque esto sacrifica cierta flexibilidad, contribuye a la seguridad y a la eficiencia de ejecución ), logrando una gran mejora en 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-69101617731b12c40620802eecf76caf.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 lo esperado, ayudando a los desarrolladores a asegurar la corrección de los contratos inteligentes y así reducir el riesgo de transacciones.
Move Prover utiliza un algoritmo de verificación deductiva para comprobar si el programa cumple con las expectativas. Esto significa que Move Prover puede inferir el comportamiento del programa basado en la información conocida y asegurarse de 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:
Recibir el archivo fuente Move como entrada, este archivo debe establecer la especificación de entrada del programa )specification(.
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 el modelo de objeto verificador )Modelo de Objeto Prover(.
Traducir el modelo al lenguaje intermedio Boogie.
El sistema de verificación Boogie realiza la "generación de condiciones de verificación" ).
Pasar las condiciones de verificación al solucionador Z3 (, el solucionador SMT desarrollado por Microsoft ).
Z3 verifica si el código del programa SMT ( cumple con la especificación ) o si es insatisfacible.
Si no se puede satisfacer, indica que la norma se establece; de lo contrario, genera un modelo que cumple con las condiciones, convierte de nuevo al formato Boogie y publica el informe de diagnóstico.
Restaurar el informe de diagnóstico a errores a nivel de código fuente.
Move utiliza Move Specification Language para describir especificaciones del sistema. Este lenguaje es un subconjunto de Move, que admite la descripción estática del comportamiento de la corrección del programa, sin afectar la producción. Se pueden escribir documentos de especificación especializados de forma independiente, 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 asegurar la corrección de los contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de razonamiento 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 mayor confianza.
4. Resumen
El lenguaje Move destaca en el diseño de seguridad, con consideraciones exhaustivas en características del lenguaje, ejecución de la máquina virtual y herramientas de seguridad. Las características del lenguaje sacrifican cierta flexibilidad, imponiendo verificación de tipos y lógica lineal, lo que facilita la automatización de la verificación y la validación formal, así como la seguridad verificable. El diseño de MoveVM separa el estado de la lógica, alineándose mejor con las necesidades de gestión de seguridad de activos en la blockchain.
A nivel de lenguaje, Move puede evitar eficazmente vulnerabilidades comunes en EVM como reentradas, desbordamientos, inyecciones de Call/DelegateCall, etc. 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 pasa por alto el sentido general.
A pesar de que el lenguaje Move considera muchas cosas en términos de seguridad para los programadores, no existe un lenguaje completamente seguro, ni programas completamente seguros. Se recomienda a los desarrolladores de contratos inteligentes 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 especificación 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.
16 me gusta
Recompensa
16
3
Compartir
Comentar
0/400
AirdropBlackHole
· 07-20 03:29
¡Buscando a alguien afín para que me guíe, soy minero desde hace 3 años!
Ver originalesResponder0
PumpBeforeRug
· 07-20 03:29
Mira este nuevo favorito de move, que también puede prevenir vulnerabilidades.
Ver originalesResponder0
CoinBasedThinking
· 07-20 03:24
La seguridad del lenguaje, por fuerte que sea, no tiene sentido.
Análisis de la seguridad del lenguaje Move: el nuevo guardián de la seguridad de los contratos inteligentes
Análisis de seguridad del lenguaje Move: un cambiador de las reglas del juego para los contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que se puede compilar y ejecutar en entornos de blockchain que implementan MoveVM. Desde su creación, ha considerado numerosos problemas de seguridad en blockchain y contratos inteligentes, y ha tomado prestados algunos diseños de seguridad del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación, cuyo principal característica es la seguridad, ¿cuál es realmente la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes en máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen riesgos de seguridad específicos en sí mismo?
Este artículo explorará los problemas 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 objetivo de diseño del lenguaje Move es soportar la escritura de programas que puedan interactuar de manera segura con código no confiable, al mismo tiempo que permite la verificación estática. Para lograr este objetivo, Move renunció a la lógica no lineal basada en la flexibilidad, no admite la despachación dinámica ni las llamadas externas recursivas, y en su lugar introduce conceptos como genéricos, almacenamiento global, recursos y otros para implementar 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 dar lugar a costosas vulnerabilidades de reentrada.
Las características de seguridad fundamentales de Move incluyen:
módulo (Module): cada módulo Move consiste en una serie de definiciones de tipos estructurales y procesos. Los módulos pueden importar definiciones de tipos declaradas en otros módulos y llamar a procesos.
Estructura(: se puede definir como un tipo de recurso, que representa datos que se pueden almacenar en un almacenamiento clave/valor global persistente.
proceso ) Función (: definir la lógica de comportamiento del módulo.
Almacenamiento global: permite que el programa Move almacene datos persistentes, los cuales solo pueden ser leídos y escritos programáticamente por el módulo que los posee.
Comprobación de invariante: se pueden definir invariantes de verificación estática para garantizar la conservación del estado del sistema.
validador de bytecode: hace cumplir el sistema de tipos a nivel de bytecode, previniendo operaciones ilegales.
Move garantiza la seguridad del código en tiempo de compilación a través de estas características. A continuación, analizaremos el mecanismo de funcionamiento de Move y cómo MoveVM asegura la seguridad en tiempo 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-419437619d55298077789e6eca578b48.webp(
2. Mecanismo de funcionamiento de Move
Los programas Move se ejecutan en una máquina virtual, y durante la ejecución no pueden acceder a la memoria del sistema, lo que permite que Move se ejecute de manera segura en entornos no confiables. Los programas Move se ejecutan en la pila, y el almacenamiento global se divide en memoria ) pila ( y variables globales ) pila (. 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 modo de índice es diferente al de la memoria.
Las instrucciones de bytecode 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, tiene requisitos de hardware más bajos y es adecuada para escenarios de blockchain. 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 la copia y el movimiento entre variables.
Durante la ejecución del programa Move, su estado es un cuádruplo ⟨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 la tabla de funciones ) del módulo en sí ( para resolver las instrucciones que contienen el cuerpo de la función.
MoveVM separa el almacenamiento de datos y la lógica del proceso de la pila de llamadas ), esta 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 al programa deben cumplir con las reglas obligatorias relacionadas con los permisos y los recursos. Aunque esto sacrifica cierta flexibilidad, contribuye a la seguridad y a la eficiencia de ejecución ), logrando una gran mejora en 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-69101617731b12c40620802eecf76caf.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 lo esperado, ayudando a los desarrolladores a asegurar la corrección de los contratos inteligentes y así reducir el riesgo de transacciones.
Move Prover utiliza un algoritmo de verificación deductiva para comprobar si el programa cumple con las expectativas. Esto significa que Move Prover puede inferir el comportamiento del programa basado en la información conocida y asegurarse de 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:
Recibir el archivo fuente Move como entrada, este archivo debe establecer la especificación de entrada del programa )specification(.
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 el modelo de objeto verificador )Modelo de Objeto Prover(.
Traducir el modelo al lenguaje intermedio Boogie.
El sistema de verificación Boogie realiza la "generación de condiciones de verificación" ).
Pasar las condiciones de verificación al solucionador Z3 (, el solucionador SMT desarrollado por Microsoft ).
Z3 verifica si el código del programa SMT ( cumple con la especificación ) o si es insatisfacible.
Si no se puede satisfacer, indica que la norma se establece; de lo contrario, genera un modelo que cumple con las condiciones, convierte de nuevo al formato Boogie y publica el informe de diagnóstico.
Restaurar el informe de diagnóstico a errores a nivel de código fuente.
Move utiliza Move Specification Language para describir especificaciones del sistema. Este lenguaje es un subconjunto de Move, que admite la descripción estática del comportamiento de la corrección del programa, sin afectar la producción. Se pueden escribir documentos de especificación especializados de forma independiente, 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 asegurar la corrección de los contratos inteligentes. Utiliza un lenguaje formal para describir el comportamiento del programa y emplea algoritmos de razonamiento 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 mayor confianza.
4. Resumen
El lenguaje Move destaca en el diseño de seguridad, con consideraciones exhaustivas en características del lenguaje, ejecución de la máquina virtual y herramientas de seguridad. Las características del lenguaje sacrifican cierta flexibilidad, imponiendo verificación de tipos y lógica lineal, lo que facilita la automatización de la verificación y la validación formal, así como la seguridad verificable. El diseño de MoveVM separa el estado de la lógica, alineándose mejor con las necesidades de gestión de seguridad de activos en la blockchain.
A nivel de lenguaje, Move puede evitar eficazmente vulnerabilidades comunes en EVM como reentradas, desbordamientos, inyecciones de Call/DelegateCall, etc. 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 pasa por alto el sentido general.
A pesar de que el lenguaje Move considera muchas cosas en términos de seguridad para los programadores, no existe un lenguaje completamente seguro, ni programas completamente seguros. Se recomienda a los desarrolladores de contratos inteligentes 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 especificación del código a empresas de seguridad de terceros.