Análisis de seguridad del lenguaje Move: el transformador de contratos inteligentes

El lenguaje Move es un lenguaje de contratos inteligentes que se puede compilar y ejecutar en un entorno de blockchain que implemente MoveVM. Como un lenguaje de contratos inteligentes de nueva generación con un enfoque principal en la seguridad, ¿cuál es su nivel de seguridad? ¿Puede evitar las amenazas de seguridad comunes de las máquinas virtuales de contratos como EVM y WASM? Este artículo explorará los problemas de seguridad del lenguaje Move desde tres perspectivas: características del lenguaje, mecanismo de ejecución y herramientas de verificación.

1. Características de seguridad del lenguaje Move

A diferencia de muchos lenguajes de programación existentes, el lenguaje Move fue diseñado para soportar tanto interacciones seguras con código no confiable como validación estática. Move abandona la lógica no lineal basada en la flexibilidad, no soporta despacho dinámico ni llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar un modelo de programación alternativo.

A continuación se muestra un ejemplo de implementación de un activo de token en el lenguaje Move:

mover módulo 0x1::TestCoin { usar 0x1::signer;

const ADMIN: address = @0x1;

struct Coin tiene clave, almacenar { 
    valor: u64
}

struct Info tiene la clave {
    total_supply: u64  
}

módulo de especificación {
    invariante para todo addr: dirección donde existe<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(cuenta, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let coin = Coin { value: amount };
    let info = borrow_global_mut\u003cinfo\u003e(ADMIN);
    info.total_supply = info.total_supply + amount;
    moneda
}

public fun value(coin: &Coin): u64 {
    coin.value  
}

}

Este ejemplo muestra algunas características clave de seguridad del lenguaje Move:

1. Modular: cada módulo Move está compuesto por definiciones de tipo de estructura y de proceso, y puede importar definiciones de tipo de otros módulos y llamar a procesos de otros módulos.

2. Tipo de recurso: Se define como tipo de recurso una estructura marcada con has key o store, que puede almacenarse en un almacenamiento clave-valor global persistente.

3. Almacenamiento global: permite que los programas Move almacenen datos persistentes, que solo pueden ser leídos y escritos programáticamente por el módulo propietario, pero que pueden ser vistos por otros módulos en el libro mayor público.

4. Control de acceso: se puede implementar el control de acceso a operaciones clave a través de afirmaciones y otros métodos.

5. Reducción de invariante: se pueden definir invariantes de verificación estática, utilizados para la verificación formal.

6. Verificación de bytecode: incluye verificación de tipo seguro y verificación de linealización, para prevenir operaciones ilegales sobre tipos de recursos.

Estas características garantizan la seguridad de la lengua Move en el momento de la compilación.

2. Mecanismo de funcionamiento de Move

El programa Move se ejecuta en una máquina virtual, no puede acceder a la memoria del sistema y puede ejecutarse de manera segura en un entorno no confiable.

El programa Move se ejecuta en la pila, el almacenamiento global se divide en memoria (, pila ) y variables globales (. La memoria no puede almacenar punteros que apunten a celdas de memoria, las variables globales se utilizan para almacenar punteros que apuntan a celdas de memoria.

Las instrucciones de bytecode de Move se ejecutan en un intérprete basado en pila, lo que facilita su implementación y control, siendo adecuado para escenarios de blockchain. Los valores de tipo de recurso solo se pueden mover de manera destructiva.

El estado de ejecución del programa Move es un cuádruple ⟨C, M, G, S⟩, que incluye la pila de llamadas, la memoria, las variables globales y los operandos. Durante la ejecución, las llamadas a funciones crean nuevos objetos de pila de llamadas, y las instrucciones de bifurcación realizan saltos estáticos, evitando la distribución dinámica.

MoveVM separa el almacenamiento de datos y la pila de llamadas, a diferencia del diseño de EVM. Este diseño, aunque sacrifica flexibilidad, mejora 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 basada en la inferencia, que utiliza un lenguaje formal para describir el comportamiento del programa y aplica algoritmos de inferencia para verificar si el programa cumple con las expectativas.

La arquitectura de Move Prover es la siguiente:

1. Recibir archivos fuente de Move como entrada, incluyendo especificaciones del programa.
2. El analizador extrae la especificación, y el compilador compila el código fuente en bytecode.
3. Convertir a un modelo de objeto validador.
4. Traducir a un lenguaje intermedio de Boogie.
5. El sistema de verificación Boogie genera las condiciones de verificación.
6. El solucionador Z3 verifica si la fórmula SMT es insatisfacible.
7. Generar un informe de diagnóstico y restaurar a errores a nivel de código fuente.

Move utiliza el Lenguaje de Especificación Move para describir especificaciones, que es un subconjunto del lenguaje Move.

Move Prover es una herramienta útil que ayuda a los desarrolladores a garantizar la corrección de los contratos inteligentes y a reducir el riesgo de transacciones.

![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(

Resumen

El lenguaje Move se destaca en el diseño de seguridad, considerando de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad. Sacrifica parte de la flexibilidad para reforzar la verificación de tipos y la 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, adaptándose mejor a las necesidades de gestión de seguridad de los activos en blockchain.

El lenguaje Move puede evitar eficazmente las vulnerabilidades comunes del EVM, como la reentrada, el desbordamiento y la inyección, pero los problemas de autorización, lógica y desbordamiento de enteros grandes aún requieren la atención de los desarrolladores. Aunque Move considera de manera integral la seguridad, se recomienda utilizar servicios de auditoría de empresas de seguridad de terceros y dejar la redacción y verificación de código normativo en manos de un equipo de seguridad profesional.

![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(