Move es un lenguaje de contratos inteligentes que se puede compilar y ejecutar en entornos de blockchain que implementan MoveVM. Desde su diseño inicial, ha considerado muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y ha tomado como referencia algunos conceptos de diseño seguro del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación con la seguridad como característica principal, ¿cuál es realmente la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad específicos en Move?
Este artículo explorará el problema de la seguridad del lenguaje Move desde tres aspectos: las características del lenguaje, el mecanismo de funcionamiento y las herramientas de verificación.
1. Características de seguridad del lenguaje Move
Es difícil escribir código sin vulnerabilidades, incluso después de múltiples pruebas no se puede garantizar completamente. Es aún más desafiante escribir código que mantenga propiedades de seguridad clave al interactuar con código no confiable. Existen diversas técnicas que pueden imponer la seguridad en tiempo de ejecución, como sandboxing, aislamiento de procesos, bloqueo de objetos y otros patrones de programación; también se puede especificar la seguridad estática en tiempo de compilación, como tipos estáticos obligatorios o verificaciones de aserciones.
A veces también se pueden utilizar herramientas de análisis semántico y análisis estático para asegurar que el código cumpla con las reglas de seguridad, manteniendo ciertas invariantes lógicas demostrables incluso cuando interactúa con código no confiable. Estos métodos parecen prometedores, pueden evitar la sobrecarga en tiempo de ejecución y descubrir problemas de seguridad con antelación. Sin embargo, la seguridad que obtienen los lenguajes de programación a través de estos métodos es extremadamente limitada, por dos razones principales: en primer lugar, suelen tener características del lenguaje que son difíciles de analizar con herramientas de análisis estático, como la dispatch dinámica, la mutabilidad compartida y la reflexión, que son lógicas no lineales, y estas características violan las reglas de invariantes de seguridad, proporcionando a los atacantes una amplia superficie de ataque. En segundo lugar, la mayoría de los lenguajes de programación son difíciles de extender para admitir herramientas estáticas relacionadas con la seguridad o lenguajes de reducción expresivos, aunque estas dos extensiones son muy importantes.
El diseño de Move permite una interacción segura con código no confiable y también soporta la verificación estática. Posee estas características de seguridad porque ha eliminado toda lógica no lineal basada en consideraciones de flexibilidad, no soporta la dispatch dinámica ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de despacho dinámico y llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes han llevado a costosas vulnerabilidades de reentrada.
Las principales características de seguridad del lenguaje Move incluyen:
Modular: Cada módulo Move está compuesto por una serie de definiciones de tipos de estructura y procedimientos. Los módulos pueden importar definiciones de tipos declaradas en otros módulos y llamar a procedimientos.
Estructura: se puede definir una estructura de tipo de recurso, utilizada para representar datos que se pueden almacenar en un almacenamiento global de clave/valor.
Proceso: define los procesos de inicialización, seguros y no seguros. Los procesos pueden tener restricciones de control de acceso.
Almacenamiento global: permite almacenar datos persistentes, que 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 comprobación estática para garantizar la integridad de los recursos en el sistema.
Verificador de bytecode: impone un sistema de tipos a nivel de bytecode, evitando que los recursos sean creados, desempaquetados o referenciados inapropiadamente.
Estas características permiten que Move ofrezca una poderosa seguridad tanto en tiempo de compilación como en tiempo de ejecución.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, lo que impide el acceso directo a la memoria del sistema, asegurando que pueda funcionar de manera segura en entornos no confiables.
Move utiliza un modelo de ejecución basado en pilas. El almacenamiento global se divide en memoria (, pila ) y variables globales (. La memoria es un almacenamiento de primer nivel y no puede almacenar punteros que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, accediendo a través de direcciones y tipos.
Move utiliza un intérprete basado en pilas para ejecutar instrucciones de bytecode. Este método es fácil de implementar y controlar, con bajos requisitos de hardware, lo que lo hace adecuado para escenarios de blockchain. En comparación con un intérprete basado en registros, un intérprete basado en pilas es más fácil de controlar y detectar la copia y el movimiento entre variables.
El estado de ejecución del programa Move es una cuádruple ⟨C, M, G, S⟩, que incluye la pila de llamadas )C(, la memoria )M(, las variables globales )G( y la pila de operandos )S(. La pila de llamadas contiene información de contexto sobre la ejecución del proceso y el número de instrucción. Al ejecutar la instrucción Call, se crea un nuevo objeto de pila de llamadas, se almacenan los parámetros y se ejecutan las instrucciones del nuevo contrato. Al encontrar una instrucción de bifurcación, se realiza un salto estático dentro del proceso.
MoveVM separa el almacenamiento de datos y la pila de llamadas, esta es su principal diferencia con EVM. En Move, 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. Este diseño sacrifica cierta flexibilidad, pero mejora la seguridad y la eficiencia de la ejecución.
3. Mover Prover
Move Prover es una herramienta de verificación formal basada en inferencias que puede ayudar a los desarrolladores a garantizar la corrección de los contratos inteligentes y reducir el riesgo de transacciones. Utiliza un lenguaje formal para describir el comportamiento del programa y verifica mediante algoritmos de inferencia si el programa cumple con lo esperado.
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 lo 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:
Recibir el archivo fuente Move como entrada, que contiene las especificaciones del programa.
El analizador extrae la especificación, el compilador compila el código fuente en bytecode
Generar modelo de objeto de validador
Traducir el modelo al lenguaje intermedio Boogie
El sistema de verificación Boogie genera condiciones de verificación
Pasar las condiciones de verificación al solucionador Z3 para su comprobación
Generar un informe de diagnóstico y convertirlo en errores a nivel de código fuente
Move proporciona el Move Specification Language para describir especificaciones, que es un subconjunto del lenguaje Move, y admite la descripción estática del comportamiento de corrección de programas. Las especificaciones se pueden escribir de manera independiente al código de negocio.
Move Prover es una herramienta poderosa que ayuda a los desarrolladores a garantizar la corrección de los contratos inteligentes y a reducir el riesgo de transacciones. Utiliza métodos formales para verificar si el programa cumple con las expectativas, aumentando la confianza de los desarrolladores al desplegar contratos inteligentes.
Resumen
El lenguaje Move ha considerado exhaustivamente la seguridad, proporcionando fuertes garantías en características del lenguaje, ejecución de máquina virtual y herramientas de seguridad. Sacrifica cierta flexibilidad, implementando chequeo de tipos forzado y lógica lineal, lo cual favorece 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, lo que se alinea mejor con las necesidades de gestión de seguridad de activos en blockchain.
El lenguaje Move puede evitar eficazmente vulnerabilidades comunes en EVM como la reentrada, el desbordamiento, la inyección de Call/DelegateCall, entre otras. 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 es poderoso, no puede evitar por completo las negligencias en el diseño general.
A pesar de que Move ha considerado mucho la 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 a un equipo de seguridad profesional.
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.
23 me gusta
Recompensa
23
7
Compartir
Comentar
0/400
GasFeeWhisperer
· 08-05 12:29
move ha renovado la percepción, esto es lo que se llama seguridad.
Ver originalesResponder0
GasGasGasBro
· 08-03 23:15
Demasiado complicado, cada vez que veo la seguridad me quedo calvo.
Ver originalesResponder0
ForkTongue
· 08-03 07:07
move es una cosa divina, realmente no podemos entenderlo.
Ver originalesResponder0
AirdropBuffet
· 08-02 20:38
move es realmente alcista, es bastante más simple que rust
Ver originalesResponder0
0xLuckbox
· 08-02 20:37
move seguridad replicada es realmente buena, vamos a aprender
Ver originalesResponder0
HalfPositionRunner
· 08-02 20:29
¡move también tiene errores, ten cuidado!
Ver originalesResponder0
rugpull_survivor
· 08-02 20:19
move esto no es más que rust con un disfraz diferente
Análisis profundo de las características de seguridad del lenguaje Move: desde el diseño del lenguaje hasta la verificación formal
Análisis de la seguridad del lenguaje Move
Introducción
Move es un lenguaje de contratos inteligentes que se puede compilar y ejecutar en entornos de blockchain que implementan MoveVM. Desde su diseño inicial, ha considerado muchos problemas de seguridad relacionados con blockchain y contratos inteligentes, y ha tomado como referencia algunos conceptos de diseño seguro del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación con la seguridad como característica principal, ¿cuál es realmente la seguridad de Move? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM, WASM, etc., a nivel de lenguaje o mediante mecanismos relacionados? ¿Existen problemas de seguridad específicos en Move?
Este artículo explorará el problema de la seguridad del lenguaje Move desde tres aspectos: las características del lenguaje, el mecanismo de funcionamiento y las herramientas de verificación.
1. Características de seguridad del lenguaje Move
Es difícil escribir código sin vulnerabilidades, incluso después de múltiples pruebas no se puede garantizar completamente. Es aún más desafiante escribir código que mantenga propiedades de seguridad clave al interactuar con código no confiable. Existen diversas técnicas que pueden imponer la seguridad en tiempo de ejecución, como sandboxing, aislamiento de procesos, bloqueo de objetos y otros patrones de programación; también se puede especificar la seguridad estática en tiempo de compilación, como tipos estáticos obligatorios o verificaciones de aserciones.
A veces también se pueden utilizar herramientas de análisis semántico y análisis estático para asegurar que el código cumpla con las reglas de seguridad, manteniendo ciertas invariantes lógicas demostrables incluso cuando interactúa con código no confiable. Estos métodos parecen prometedores, pueden evitar la sobrecarga en tiempo de ejecución y descubrir problemas de seguridad con antelación. Sin embargo, la seguridad que obtienen los lenguajes de programación a través de estos métodos es extremadamente limitada, por dos razones principales: en primer lugar, suelen tener características del lenguaje que son difíciles de analizar con herramientas de análisis estático, como la dispatch dinámica, la mutabilidad compartida y la reflexión, que son lógicas no lineales, y estas características violan las reglas de invariantes de seguridad, proporcionando a los atacantes una amplia superficie de ataque. En segundo lugar, la mayoría de los lenguajes de programación son difíciles de extender para admitir herramientas estáticas relacionadas con la seguridad o lenguajes de reducción expresivos, aunque estas dos extensiones son muy importantes.
El diseño de Move permite una interacción segura con código no confiable y también soporta la verificación estática. Posee estas características de seguridad porque ha eliminado toda lógica no lineal basada en consideraciones de flexibilidad, no soporta la dispatch dinámica ni las llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de despacho dinámico y llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes han llevado a costosas vulnerabilidades de reentrada.
Las principales características de seguridad del lenguaje Move incluyen:
Modular: Cada módulo Move está compuesto por una serie de definiciones de tipos de estructura y procedimientos. Los módulos pueden importar definiciones de tipos declaradas en otros módulos y llamar a procedimientos.
Estructura: se puede definir una estructura de tipo de recurso, utilizada para representar datos que se pueden almacenar en un almacenamiento global de clave/valor.
Proceso: define los procesos de inicialización, seguros y no seguros. Los procesos pueden tener restricciones de control de acceso.
Almacenamiento global: permite almacenar datos persistentes, que 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 comprobación estática para garantizar la integridad de los recursos en el sistema.
Verificador de bytecode: impone un sistema de tipos a nivel de bytecode, evitando que los recursos sean creados, desempaquetados o referenciados inapropiadamente.
Estas características permiten que Move ofrezca una poderosa seguridad tanto en tiempo de compilación como en tiempo de ejecución.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en una máquina virtual, lo que impide el acceso directo a la memoria del sistema, asegurando que pueda funcionar de manera segura en entornos no confiables.
Move utiliza un modelo de ejecución basado en pilas. El almacenamiento global se divide en memoria (, pila ) y variables globales (. La memoria es un almacenamiento de primer nivel y no puede almacenar punteros que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, accediendo a través de direcciones y tipos.
Move utiliza un intérprete basado en pilas para ejecutar instrucciones de bytecode. Este método es fácil de implementar y controlar, con bajos requisitos de hardware, lo que lo hace adecuado para escenarios de blockchain. En comparación con un intérprete basado en registros, un intérprete basado en pilas es más fácil de controlar y detectar la copia y el movimiento entre variables.
El estado de ejecución del programa Move es una cuádruple ⟨C, M, G, S⟩, que incluye la pila de llamadas )C(, la memoria )M(, las variables globales )G( y la pila de operandos )S(. La pila de llamadas contiene información de contexto sobre la ejecución del proceso y el número de instrucción. Al ejecutar la instrucción Call, se crea un nuevo objeto de pila de llamadas, se almacenan los parámetros y se ejecutan las instrucciones del nuevo contrato. Al encontrar una instrucción de bifurcación, se realiza un salto estático dentro del proceso.
MoveVM separa el almacenamiento de datos y la pila de llamadas, esta es su principal diferencia con EVM. En Move, 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. Este diseño sacrifica cierta flexibilidad, pero mejora la seguridad y la eficiencia de la ejecución.
3. Mover Prover
Move Prover es una herramienta de verificación formal basada en inferencias que puede ayudar a los desarrolladores a garantizar la corrección de los contratos inteligentes y reducir el riesgo de transacciones. Utiliza un lenguaje formal para describir el comportamiento del programa y verifica mediante algoritmos de inferencia si el programa cumple con lo esperado.
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 lo 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 proporciona el Move Specification Language para describir especificaciones, que es un subconjunto del lenguaje Move, y admite la descripción estática del comportamiento de corrección de programas. Las especificaciones se pueden escribir de manera independiente al código de negocio.
Move Prover es una herramienta poderosa que ayuda a los desarrolladores a garantizar la corrección de los contratos inteligentes y a reducir el riesgo de transacciones. Utiliza métodos formales para verificar si el programa cumple con las expectativas, aumentando la confianza de los desarrolladores al desplegar contratos inteligentes.
Resumen
El lenguaje Move ha considerado exhaustivamente la seguridad, proporcionando fuertes garantías en características del lenguaje, ejecución de máquina virtual y herramientas de seguridad. Sacrifica cierta flexibilidad, implementando chequeo de tipos forzado y lógica lineal, lo cual favorece 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, lo que se alinea mejor con las necesidades de gestión de seguridad de activos en blockchain.
El lenguaje Move puede evitar eficazmente vulnerabilidades comunes en EVM como la reentrada, el desbordamiento, la inyección de Call/DelegateCall, entre otras. 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 es poderoso, no puede evitar por completo las negligencias en el diseño general.
A pesar de que Move ha considerado mucho la 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 a un equipo de seguridad profesional.