El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de nueva generación, tiene un diseño de seguridad excepcional. Este artículo analizará la seguridad de Move desde tres aspectos: características del lenguaje, mecanismo de ejecución y herramientas de verificación.
1. Las características de seguridad del lenguaje Move
El lenguaje Move, en su diseño, ha abandonado la lógica no lineal, no admite la distribución dinámica ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar un patrón de programación alternativo. Estas características evitan eficazmente vulnerabilidades comunes como la reentrada.
El mecanismo de seguridad central de Move incluye:
Módulo: cada módulo está compuesto por un tipo de estructura y una definición de proceso, y puede importar definiciones de tipo de otros módulos.
Estructura: se puede definir como un tipo de recurso, almacenado en el almacenamiento clave-valor global.
Almacenamiento global: permite el almacenamiento persistente de datos, que solo puede ser leído y escrito programáticamente por el propietario del módulo.
Verificador de bytecode: aplica de manera estricta tipos de seguridad y linealización, previniendo operaciones ilegales sobre valores de tipos de recurso.
Invariante de restricción: se pueden definir invariantes de verificación estática para garantizar la seguridad del código.
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. Su estado está compuesto por la pila de llamadas, memoria, variables globales y un arreglo de operaciones.
MoveVM separa el almacenamiento de datos y la pila de llamadas, lo que representa una gran diferencia con EVM. Los recursos bajo la dirección de cuenta de estado de usuario ( se almacenan de forma independiente, y las llamadas a programas deben cumplir con las reglas de permisos y recursos, mejorando 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-69101617731b12c40620802eecf76caf.webp(
3. Mover Prover
Move Prover es una herramienta de verificación formal que utiliza algoritmos de verificación deductiva para comprobar si un programa cumple con lo esperado. Su flujo de trabajo es el siguiente:
Recibir la entrada del archivo fuente Move, extraer las especificaciones
Compilar a bytecode, convertir a modelo de objeto del validador
Traducir a lenguaje intermedio de Boogie
Generar condiciones de verificación
Verificar la fórmula SMT utilizando el solucionador Z3
Generar informe de diagnóstico
El Lenguaje de Especificación de Movimiento se utiliza para describir especificaciones, se puede escribir de forma independiente sin afectar el código de producción.
![Análisis de seguridad de Move: el cambiante de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Resumen
Move tiene en cuenta de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Evita vulnerabilidades comunes como la reentrada y el desbordamiento, pero los problemas de gestión de permisos y errores lógicos aún requieren la atención de los desarrolladores. Se recomienda utilizar auditorías de seguridad de terceros y dejar que un equipo profesional escriba el código de especificación 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(
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.
20 me gusta
Recompensa
20
5
Republicar
Compartir
Comentar
0/400
MEVHunterZhang
· 07-13 14:53
Mientras la seguridad sea lo suficientemente sólida, lo demás es solo ilusión.
Análisis completo de la seguridad del lenguaje Move: características, mecanismos y herramientas de verificación
Análisis de la seguridad del lenguaje Move
El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de nueva generación, tiene un diseño de seguridad excepcional. Este artículo analizará la seguridad de Move desde tres aspectos: características del lenguaje, mecanismo de ejecución y herramientas de verificación.
1. Las características de seguridad del lenguaje Move
El lenguaje Move, en su diseño, ha abandonado la lógica no lineal, no admite la distribución dinámica ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar un patrón de programación alternativo. Estas características evitan eficazmente vulnerabilidades comunes como la reentrada.
El mecanismo de seguridad central de Move incluye:
Módulo: cada módulo está compuesto por un tipo de estructura y una definición de proceso, y puede importar definiciones de tipo de otros módulos.
Estructura: se puede definir como un tipo de recurso, almacenado en el almacenamiento clave-valor global.
Almacenamiento global: permite el almacenamiento persistente de datos, que solo puede ser leído y escrito programáticamente por el propietario del módulo.
Verificador de bytecode: aplica de manera estricta tipos de seguridad y linealización, previniendo operaciones ilegales sobre valores de tipos de recurso.
Invariante de restricción: se pueden definir invariantes de verificación estática para garantizar la seguridad del código.
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. Su estado está compuesto por la pila de llamadas, memoria, variables globales y un arreglo de operaciones.
MoveVM separa el almacenamiento de datos y la pila de llamadas, lo que representa una gran diferencia con EVM. Los recursos bajo la dirección de cuenta de estado de usuario ( se almacenan de forma independiente, y las llamadas a programas deben cumplir con las reglas de permisos y recursos, mejorando 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-69101617731b12c40620802eecf76caf.webp(
3. Mover Prover
Move Prover es una herramienta de verificación formal que utiliza algoritmos de verificación deductiva para comprobar si un programa cumple con lo esperado. Su flujo de trabajo es el siguiente:
El Lenguaje de Especificación de Movimiento se utiliza para describir especificaciones, se puede escribir de forma independiente sin afectar el código de producción.
![Análisis de seguridad de Move: el cambiante de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
Resumen
Move tiene en cuenta de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Evita vulnerabilidades comunes como la reentrada y el desbordamiento, pero los problemas de gestión de permisos y errores lógicos aún requieren la atención de los desarrolladores. Se recomienda utilizar auditorías de seguridad de terceros y dejar que un equipo profesional escriba el código de especificación 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(