Move es un lenguaje de contratos inteligentes diseñado para entornos de blockchain, que puede ejecutarse en cadenas que soportan MoveVM. Su diseño considera los problemas de seguridad en blockchain y contratos inteligentes, y se basa en algunos conceptos de diseño de seguridad de Rust. Este artículo analizará 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 mejora la seguridad al renunciar a cierta flexibilidad, no admite la dispatch 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.
Los principales componentes de Move incluyen:
Módulo: compuesto por tipos de estructura y definiciones de proceso
Estructura: se puede definir como un tipo de recurso, almacenado en el almacenamiento de clave-valor global.
Proceso: Definir la lógica del contrato
El almacenamiento global de Move permite la persistencia de datos, que solo pueden ser leídos y escritos de manera programática por el módulo propietario, pero que pueden ser consultados en el libro mayor público.
Move garantiza la seguridad de la compilación del código a través de dos mecanismos:
Invariantes: para la verificación estática, define la conservación del estado del sistema.
Verificador de bytecode: ejecución forzada de tipos seguros y linealización, previene operaciones ilegales
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. Utiliza un modelo de ejecución basado en pilas, dividiendo el almacenamiento global en memoria ( pila ) y variables globales ( pila ).
El estado de Move está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Durante la ejecución, la pila de llamadas guarda información de contexto, y el salto estático evita la despachación dinámica, lo que previene ataques de reentrada.
MoveVM separa el almacenamiento de datos y la pila de llamadas, a diferencia de EVM. Este diseño mejora la seguridad y la eficiencia de ejecución.
3. Mover Proveedor
Move Prover es una herramienta de verificación formal que utiliza algoritmos de verificación deductiva para validar la corrección de los programas. Su flujo de trabajo es:
Recibir el archivo fuente Move y las especificaciones
Compilar a bytecode y verificar el modelo de objeto
Convertir a lenguaje intermedio Boogie
Generar condiciones de verificación
Verificar con el solucionador Z3
Generar informe de diagnóstico
El Lenguaje de Especificación de Movimiento se utiliza para describir especificaciones de programas, y se puede escribir independientemente del código de negocio.
4. Resumen
Move ha considerado de manera integral el diseño del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica parte de la flexibilidad, pero mejora la seguridad y la verificabilidad. Las vulnerabilidades comunes de EVM como la reentrada, desbordamiento, etc., se pueden evitar eficazmente, pero aún se deben tener en cuenta problemas como la autenticación, la lógica y el desbordamiento de enteros grandes.
A pesar de que Move ofrece múltiples garantías de seguridad, se recomienda a los desarrolladores que utilicen servicios de auditoría de seguridad de terceros y que dejen la redacción y verificación de las especificaciones a empresas 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.
26 me gusta
Recompensa
26
8
Republicar
Compartir
Comentar
0/400
CountdownToBroke
· 08-04 13:47
De nuevo, el hermano rust ha hecho una versión recortada, casi equivalente a lo que escribió el amigo.
Ver originalesResponder0
TerraNeverForget
· 08-03 01:26
¿Así que nuevamente se mueve, verdad? Entonces yo también me muevo.
Ver originalesResponder0
DuckFluff
· 08-02 19:38
Y tomé prestada una parte de Rust, me hace sentir abrumado.
Ver originalesResponder0
SurvivorshipBias
· 08-01 22:52
Move es tan seguro que los tiburones ya no tendrán comida.
Ver originalesResponder0
Ser_This_Is_A_Casino
· 08-01 22:50
Siento que move es un poco demasiado rígido, incluso más que rust.
Ver originalesResponder0
SchrodingerAirdrop
· 08-01 22:50
Otra vez no puedo aprender, realmente es un gran problema.
Ver originalesResponder0
MetaverseMigrant
· 08-01 22:49
Escribir en move aún no es tan rápido como correr en mi caso...
Ver originalesResponder0
GasFeeDodger
· 08-01 22:45
No es mejor que escribir en solidity, es realmente un esfuerzo.
Análisis completo de la seguridad del lenguaje Move: características del lenguaje, mecanismo de ejecución y herramientas de verificación
Análisis de la seguridad del lenguaje Move
Introducción
Move es un lenguaje de contratos inteligentes diseñado para entornos de blockchain, que puede ejecutarse en cadenas que soportan MoveVM. Su diseño considera los problemas de seguridad en blockchain y contratos inteligentes, y se basa en algunos conceptos de diseño de seguridad de Rust. Este artículo analizará 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 mejora la seguridad al renunciar a cierta flexibilidad, no admite la dispatch 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.
Los principales componentes de Move incluyen:
El almacenamiento global de Move permite la persistencia de datos, que solo pueden ser leídos y escritos de manera programática por el módulo propietario, pero que pueden ser consultados en el libro mayor público.
Move garantiza la seguridad de la compilación del código a través de dos mecanismos:
Invariantes: para la verificación estática, define la conservación del estado del sistema.
Verificador de bytecode: ejecución forzada de tipos seguros y linealización, previene operaciones ilegales
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. Utiliza un modelo de ejecución basado en pilas, dividiendo el almacenamiento global en memoria ( pila ) y variables globales ( pila ).
El estado de Move está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Durante la ejecución, la pila de llamadas guarda información de contexto, y el salto estático evita la despachación dinámica, lo que previene ataques de reentrada.
MoveVM separa el almacenamiento de datos y la pila de llamadas, a diferencia de EVM. Este diseño mejora la seguridad y la eficiencia de ejecución.
3. Mover Proveedor
Move Prover es una herramienta de verificación formal que utiliza algoritmos de verificación deductiva para validar la corrección de los programas. Su flujo de trabajo es:
El Lenguaje de Especificación de Movimiento se utiliza para describir especificaciones de programas, y se puede escribir independientemente del código de negocio.
4. Resumen
Move ha considerado de manera integral el diseño del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica parte de la flexibilidad, pero mejora la seguridad y la verificabilidad. Las vulnerabilidades comunes de EVM como la reentrada, desbordamiento, etc., se pueden evitar eficazmente, pero aún se deben tener en cuenta problemas como la autenticación, la lógica y el desbordamiento de enteros grandes.
A pesar de que Move ofrece múltiples garantías de seguridad, se recomienda a los desarrolladores que utilicen servicios de auditoría de seguridad de terceros y que dejen la redacción y verificación de las especificaciones a empresas de seguridad profesionales.