- Tema
27k Popularidad
57k Popularidad
7k Popularidad
16k Popularidad
30k Popularidad
2k Popularidad
95k Popularidad
27k Popularidad
26k Popularidad
7k Popularidad
- Anclado
27k Popularidad
57k Popularidad
7k Popularidad
16k Popularidad
30k Popularidad
2k Popularidad
95k Popularidad
27k Popularidad
26k Popularidad
7k Popularidad
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
Introducción
Move es un lenguaje de contratos inteligentes que puede ejecutarse en un entorno de blockchain que implemente MoveVM. Desde su creación, ha considerado muchos problemas de seguridad relacionados con la blockchain y los contratos inteligentes, y ha tomado prestados algunos diseños de seguridad del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación con la seguridad como su principal característica, ¿cuál es la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes en las máquinas virtuales de contratos como EVM y WASM 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: 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, Move fue diseñado para soportar interacciones seguras con código no confiable y también para permitir la verificación estática. Move posee estas características de seguridad porque renuncia a la lógica no lineal basada en consideraciones de flexibilidad, no soporta el despacho dinámico, ni llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar un modelo de programación alternativo. Por ejemplo, Move omite las características de despacho dinámico y llamadas recursivas que podrían dar lugar a vulnerabilidades de reentrada.
Las principales características de seguridad de Move incluyen:
Módulo(: Cada módulo Move está compuesto por una serie de tipos de estructuras y definiciones de procesos. Un módulo puede importar definiciones de tipos declaradas en otros módulos y llamar a sus procesos.
Estructura ): se puede definir como un tipo de recurso, que representa lo que se puede almacenar en un almacenamiento clave/valor global persistente.
3( proceso)función): definir la funcionalidad específica del módulo.
4( 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 integridad de los recursos en el sistema.
Verificador de bytecode: valida tipos de seguridad y linealización, previene que valores sensibles sean creados, modificados o destruidos ilegalmente.
![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)
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. El programa se ejecuta en la pila, y el almacenamiento global se divide en dos partes: memoria (, pila ) y variables globales (.
Las instrucciones de bytecode de Move se ejecutan en un intérprete basado en pila, este método es fácil de implementar y controlar, tiene bajos requisitos de hardware, y es adecuado para escenarios de blockchain. Al mismo tiempo, en comparación con los intérpretes basados en registros, los intérpretes basados en pila son más fáciles de controlar y detectar las copias y movimientos entre variables.
Durante el proceso de ejecución, el estado del programa Move está compuesto por la pila de llamadas, la memoria, las variables globales y los arreglos de operaciones. La pila de llamadas contiene toda la información contextual de la ejecución del proceso. Al ejecutar la instrucción Call, se crea un nuevo objeto de pila de llamadas. Al encontrar una instrucción de bifurcación, se realiza un salto estático dentro del proceso.
A diferencia de EVM, MoveVM separa el almacenamiento de datos y la pila de llamadas, lo que es más adecuado para las necesidades de gestión de seguridad de activos en blockchain. Este diseño 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 basada en razonamiento, que utiliza un lenguaje formal para describir el comportamiento de los programas y algoritmos de razonamiento para verificar si el programa cumple con las expectativas. Puede ayudar a los desarrolladores a garantizar la corrección de los contratos inteligentes y reducir el riesgo de transacciones.
Move Prover utiliza un algoritmo de verificación deductiva para inferir el comportamiento del programa según la información conocida, asegurando 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:
Move Specification Language se utiliza para describir sistemas de especificaciones, es un subconjunto del lenguaje Move y admite la descripción estática del comportamiento correcto del programa.
En general, Move Prover es una herramienta muy útil que puede ayudar a los desarrolladores a garantizar la corrección de los contratos inteligentes, reducir el riesgo de transacciones y aumentar la confianza en el despliegue de contratos inteligentes.
![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 lenguaje Move destaca en el diseño de seguridad, teniendo en cuenta de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica cierta flexibilidad, implementando comprobaciones de tipo forzadas y lógica lineal, lo que facilita la verificación de compilación y la validación formal. MoveVM separa el estado de la lógica, lo que lo hace más adecuado para las necesidades de gestión de seguridad de activos en blockchain.
El lenguaje Move puede evitar eficazmente vulnerabilidades comunes en EVM como la reentrada, desbordamientos, inyecciones de Call/DeleGateCall, entre otros. Sin embargo, problemas como la autenticación, la lógica del código y el desbordamiento de estructuras de enteros grandes aún requieren la atención adicional de los desarrolladores. Aunque Move Prover ofrece verificación formal, no puede compensar las omisiones en el diseño general.
A pesar de que Move ha considerado muchos aspectos de seguridad, no existe un lenguaje o programa completamente seguro. Se recomienda que los desarrolladores de contratos inteligentes de Move sigan utilizando los servicios de auditoría de empresas de seguridad de terceros y dejen la redacción y verificación de la parte normativa en manos de un equipo de seguridad profesional.