Análisis de seguridad del lenguaje Move: innovador de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en entornos de blockchain que implementan MoveVM. Desde su diseño inicial, ha tenido en cuenta muchos problemas de seguridad relacionados con la blockchain y los contratos inteligentes, y se ha inspirado en algunos principios de diseño de seguridad del lenguaje Rust. Como un lenguaje de contratos inteligentes de nueva generación con un enfoque principal 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 y WASM a nivel de lenguaje o a través de mecanismos relacionados? ¿Existen vulnerabilidades de seguridad únicas en Move?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de funcionamiento y 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 forma segura con código no confiable, al mismo tiempo que se admite la verificación estática. Move logra este objetivo al descartar toda lógica no lineal basada en consideraciones de flexibilidad, no admite despacho dinámico y tampoco admite llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar algunos patrones de programación alternativos.
A continuación se presentan algunas características de seguridad clave del lenguaje Move:
Modular: Cada módulo Move está compuesto por una serie de tipos de estructura y definiciones de procesos. Los módulos pueden importar tipos declarados en otros módulos y llamar a sus procesos.
Tipo de recurso: el tipo de recurso definido mediante la sintaxis de clave has es una estructura que se puede almacenar en un almacenamiento de clave-valor global persistente.
Almacenamiento global: permite que los programas Move almacenen datos persistentes, estos datos solo pueden ser leídos y escritos programáticamente por el módulo que los posee, pero almacenados en un libro mayor público pueden ser vistos por otros módulos.
Sistema de tipos estáticos: Move tiene un poderoso sistema de tipos estáticos que puede capturar muchos errores en tiempo de compilación.
Tipos lineales: el tipo de recurso es por defecto un tipo lineal, lo que impide que se copie o se destruya implícitamente.
Reducción de invariantes: se pueden definir invariantes de conservación del estado, utilizados para la verificación formal.
Validador de bytecode: aplica un sistema de tipos a nivel de bytecode para prevenir comportamientos maliciosos.
Estas características construyen conjuntamente la base de seguridad del lenguaje Move, permitiéndole evitar muchas vulnerabilidades comunes en 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 en tiempo de ejecución, lo que garantiza una ejecución segura en entornos no confiables.
Move utiliza un intérprete basado en pilas para ejecutar instrucciones de bytecode. Su estado está compuesto por la pila de llamadas, la memoria, las variables globales y la pila de operandos. Este diseño facilita el control y la detección de copias y movimientos entre variables.
MoveVM separa el almacenamiento de datos y la pila de llamadas, esta es su mayor diferencia con EVM. Los recursos bajo la dirección de la cuenta de 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 mejora significativamente la seguridad y la 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 del lenguaje Move, que utiliza algoritmos de verificación deductiva para comprobar si un programa cumple con el comportamiento esperado. Puede inferir el comportamiento del programa a partir de la información conocida, asegurando que coincida con lo esperado, lo que 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, el cual debe contener la especificación del programa.
Extraer la especificación y compilar el archivo fuente en bytecode.
Convertir la especificación y el bytecode en un modelo de objeto validador.
Traducir el modelo al lenguaje intermedio Boogie.
El sistema de verificación Boogie genera condiciones de verificación.
El solucionador Z3 verifica si se cumplen las condiciones de validación.
Generar un informe de diagnóstico y convertirlo en errores a nivel de código fuente.
El Lenguaje de Especificación de Move se utiliza para describir las especificaciones de programas, siendo un subconjunto del lenguaje Move. Soporta la descripción estática del comportamiento correcto del programa, sin afectar al código de producción. Las especificaciones se pueden escribir de forma independiente, facilitando la separación entre el código de negocio y el código de verificación.
![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 diseño del lenguaje Move en términos de seguridad es excepcional, considerando de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica algo de flexibilidad, refuerza la verificación de tipos y la lógica lineal, facilitando la automatización de la verificación de compilación y la validación formal. 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 blockchain.
El lenguaje Move puede evitar eficazmente vulnerabilidades comunes en la EVM, como reentradas, desbordamientos, inyecciones de Call/DeleGateCall, entre otras. Sin embargo, problemas como la autorización, la lógica del código y los desbordamientos en estructuras de enteros grandes aún requieren atención adicional por parte de los desarrolladores. Aunque Move considera cuidadosamente la seguridad para los programadores, no existe un lenguaje o programa absolutamente seguro. Se recomienda a los desarrolladores de contratos inteligentes en Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que dejen la redacción y verificación del código normativo a equipos de seguridad profesionales.
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
5
Republicar
Compartir
Comentar
0/400
OptionWhisperer
· 07-15 10:34
Avanzar hasta el Precio mínimo para ver move
Ver originalesResponder0
NftCollectors
· 07-14 08:08
Move este conjunto de mecanismos de seguridad no es inferior a la proporción áurea del arte bizantino, desde la perspectiva de la historia del arte en la cadena de bloques, es completamente un hito.
Ver originalesResponder0
BearMarketSurvivor
· 07-14 03:19
La seguridad es un buen lugar común.
Ver originalesResponder0
ForkTongue
· 07-14 03:08
¿Ya hay nuevos juguetes para escribir contratos?
Ver originalesResponder0
FancyResearchLab
· 07-14 03:05
Otra nueva trampa que a Luban le gusta, teóricamente es bastante segura.
Análisis de la seguridad del lenguaje Move: el nuevo estándar para el desarrollo de contratos inteligentes
Análisis de seguridad del lenguaje Move: innovador de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en entornos de blockchain que implementan MoveVM. Desde su diseño inicial, ha tenido en cuenta muchos problemas de seguridad relacionados con la blockchain y los contratos inteligentes, y se ha inspirado en algunos principios de diseño de seguridad del lenguaje Rust. Como un lenguaje de contratos inteligentes de nueva generación con un enfoque principal 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 y WASM a nivel de lenguaje o a través de mecanismos relacionados? ¿Existen vulnerabilidades de seguridad únicas en Move?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de funcionamiento y 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 forma segura con código no confiable, al mismo tiempo que se admite la verificación estática. Move logra este objetivo al descartar toda lógica no lineal basada en consideraciones de flexibilidad, no admite despacho dinámico y tampoco admite llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar algunos patrones de programación alternativos.
A continuación se presentan algunas características de seguridad clave del lenguaje Move:
Modular: Cada módulo Move está compuesto por una serie de tipos de estructura y definiciones de procesos. Los módulos pueden importar tipos declarados en otros módulos y llamar a sus procesos.
Tipo de recurso: el tipo de recurso definido mediante la sintaxis de clave has es una estructura que se puede almacenar en un almacenamiento de clave-valor global persistente.
Almacenamiento global: permite que los programas Move almacenen datos persistentes, estos datos solo pueden ser leídos y escritos programáticamente por el módulo que los posee, pero almacenados en un libro mayor público pueden ser vistos por otros módulos.
Sistema de tipos estáticos: Move tiene un poderoso sistema de tipos estáticos que puede capturar muchos errores en tiempo de compilación.
Tipos lineales: el tipo de recurso es por defecto un tipo lineal, lo que impide que se copie o se destruya implícitamente.
Reducción de invariantes: se pueden definir invariantes de conservación del estado, utilizados para la verificación formal.
Validador de bytecode: aplica un sistema de tipos a nivel de bytecode para prevenir comportamientos maliciosos.
Estas características construyen conjuntamente la base de seguridad del lenguaje Move, permitiéndole evitar muchas vulnerabilidades comunes en 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 en tiempo de ejecución, lo que garantiza una ejecución segura en entornos no confiables.
Move utiliza un intérprete basado en pilas para ejecutar instrucciones de bytecode. Su estado está compuesto por la pila de llamadas, la memoria, las variables globales y la pila de operandos. Este diseño facilita el control y la detección de copias y movimientos entre variables.
MoveVM separa el almacenamiento de datos y la pila de llamadas, esta es su mayor diferencia con EVM. Los recursos bajo la dirección de la cuenta de 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 mejora significativamente la seguridad y la 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 del lenguaje Move, que utiliza algoritmos de verificación deductiva para comprobar si un programa cumple con el comportamiento esperado. Puede inferir el comportamiento del programa a partir de la información conocida, asegurando que coincida con lo esperado, lo que 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:
El Lenguaje de Especificación de Move se utiliza para describir las especificaciones de programas, siendo un subconjunto del lenguaje Move. Soporta la descripción estática del comportamiento correcto del programa, sin afectar al código de producción. Las especificaciones se pueden escribir de forma independiente, facilitando la separación entre el código de negocio y el código de verificación.
![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 diseño del lenguaje Move en términos de seguridad es excepcional, considerando de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica algo de flexibilidad, refuerza la verificación de tipos y la lógica lineal, facilitando la automatización de la verificación de compilación y la validación formal. 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 blockchain.
El lenguaje Move puede evitar eficazmente vulnerabilidades comunes en la EVM, como reentradas, desbordamientos, inyecciones de Call/DeleGateCall, entre otras. Sin embargo, problemas como la autorización, la lógica del código y los desbordamientos en estructuras de enteros grandes aún requieren atención adicional por parte de los desarrolladores. Aunque Move considera cuidadosamente la seguridad para los programadores, no existe un lenguaje o programa absolutamente seguro. Se recomienda a los desarrolladores de contratos inteligentes en Move que utilicen servicios de auditoría de empresas de seguridad de terceros y que dejen la redacción y verificación del código normativo a equipos de seguridad profesionales.