El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de nueva generación, consideró desde su diseño inicial los problemas de seguridad en blockchain y contratos inteligentes. Este artículo explorará la seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de ejecución y herramientas de verificación.
1. Características de seguridad del lenguaje Move
El lenguaje Move tiene las siguientes características de seguridad principales:
Se abandonó la lógica no lineal, no se admite la dispatch dinámica ni las llamadas externas recursivas.
Implementar patrones de programación alternativos utilizando conceptos como genéricos, almacenamiento global, recursos, etc.
Diseño modular, cada módulo se compone de un tipo de estructura y una definición de proceso.
El tipo de recurso y el mecanismo de almacenamiento global garantizan la seguridad del almacenamiento y de los recursos
Implementación de verificación de seguridad en tiempo de compilación para invariables y verificadores de bytecode
El validador de bytecode realiza principalmente tres tipos de verificaciones:
Verificación de la validez de la estructura
Detección semántica de la lógica del proceso
Detección de errores al enlazar
A través de estos mecanismos, Move puede garantizar una alta seguridad en el momento de la compilación.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, sin acceso directo a la memoria del sistema. Su estado se compone de la pila de llamadas, la memoria, las variables globales y las operaciones.
A diferencia de EVM, MoveVM separa el almacenamiento de datos y la pila de llamadas. El estado del usuario se almacena de forma independiente, y las llamadas a programas deben cumplir con las reglas de permisos y recursos. Este diseño mejora la seguridad y la eficiencia de la ejecución.
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 las expectativas. Su proceso de verificación es el siguiente:
Recibir los archivos fuente de Move y las especificaciones
Compilar a bytecode y modelo de objeto validador
Traducir al lenguaje intermedio de Boogie
Generar condiciones de verificación
Verificación usando el solucionador Z3
Generar informe de diagnóstico
El Lenguaje de Especificación de Movimiento se utiliza para describir sistemas de especificación, y es un subconjunto del lenguaje Move.
En general, Move Prover es una poderosa herramienta de seguridad, pero no puede reemplazar completamente la auditoría manual. Se recomienda que los desarrolladores sigan utilizando servicios de auditoría de seguridad de terceros y dejen que la parte de especificación sea completada por una empresa de seguridad.
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.
Análisis de la seguridad del lenguaje Move: características del lenguaje, mecanismo de funcionamiento y Verificación formal
Análisis de seguridad del lenguaje Move
El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de nueva generación, consideró desde su diseño inicial los problemas de seguridad en blockchain y contratos inteligentes. Este artículo explorará la seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de ejecución y herramientas de verificación.
1. Características de seguridad del lenguaje Move
El lenguaje Move tiene las siguientes características de seguridad principales:
El validador de bytecode realiza principalmente tres tipos de verificaciones:
A través de estos mecanismos, Move puede garantizar una alta seguridad en el momento de la compilación.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, sin acceso directo a la memoria del sistema. Su estado se compone de la pila de llamadas, la memoria, las variables globales y las operaciones.
A diferencia de EVM, MoveVM separa el almacenamiento de datos y la pila de llamadas. El estado del usuario se almacena de forma independiente, y las llamadas a programas deben cumplir con las reglas de permisos y recursos. Este diseño mejora la seguridad y la eficiencia de la ejecución.
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 las expectativas. Su proceso de verificación es el siguiente:
El Lenguaje de Especificación de Movimiento se utiliza para describir sistemas de especificación, y es un subconjunto del lenguaje Move.
En general, Move Prover es una poderosa herramienta de seguridad, pero no puede reemplazar completamente la auditoría manual. Se recomienda que los desarrolladores sigan utilizando servicios de auditoría de seguridad de terceros y dejen que la parte de especificación sea completada por una empresa de seguridad.