Análisis de la seguridad del lenguaje Move

El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de próxima generación, consideró plenamente los problemas de seguridad de la blockchain y los contratos inteligentes desde su diseño inicial. 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 tiene las siguientes características de seguridad principales:

• Se abandonó la asignación dinámica, las llamadas externas recursivas y otras lógicas no lineales, evitando vulnerabilidades como la reentrada.
• Utilizar tipos de recursos y mecanismos de almacenamiento global para lograr una gestión segura de almacenamiento y recursos
• A través de la reducción de invariantes y el verificador de bytecode, se realizan dobles comprobaciones de seguridad en el momento de la compilación

A continuación se muestra un ejemplo sencillo de contrato Move:

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

const ADMIN: address = @0x1;

struct Coin tiene clave {
    valor: u64
}

struct Info tiene la clave {
    total_supply: u64  
}

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);
    mover_a(cuenta, Info { suministro_total: 0 });
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    Moneda { valor: cantidad }
}

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

}

Move garantiza la seguridad del código a través de la reducción de invariante y el verificador de bytecode:

1. Invariante de reducción: se utiliza para verificar que la suma de los valores de todos los objetos Coin en el sistema debe ser igual a total_supply en Info.

2. Validador de bytecode: verificación de tipos obligatoria y lógica lineal, previene la creación, copia o destrucción ilegal de recursos.

2. Mecanismo de funcionamiento de Move

El programa Move se ejecuta en una máquina virtual y tiene las siguientes características:

• No se puede acceder a la memoria del sistema en tiempo de ejecución, garantizando un funcionamiento seguro en entornos no confiables.
• Utiliza un intérprete basado en pilas para ejecutar instrucciones de bytecode, fácil de implementar y controlar
• Separar el almacenamiento de datos y la pila de llamadas, mejorando la seguridad y la eficiencia de la ejecución
• Los recursos solo pueden ser movidos de manera destructiva, no pueden ser copiados

El estado de ejecución del programa Move está compuesto por un cuádruple ⟨C, M, G, S⟩:

• C: Pila de llamadas
• M: memoria ( pila )
• G: Variable global ( pila )
• S:operando

Este diseño separa el estado del usuario de la lógica del programa, mejorando la seguridad y la eficiencia en la ejecución concurrente.

3. Mover Prover

Move Prover es una herramienta de verificación formal, diseñada para asegurar la corrección de los contratos inteligentes. Su flujo de trabajo es el siguiente:

1. Recibir el archivo fuente Move y las especificaciones como entrada
2. Extraer especificaciones y compilar en bytecode
3. Convertir a modelo de objeto de validador
4. Traducir al lenguaje intermedio de Boogie
5. Generar condiciones de verificación
6. Usar el solucionador Z3 para verificar la fórmula
7. Generar informe de diagnóstico

Move Prover utiliza el Lenguaje de Especificación Move para describir las especificaciones del programa. Este lenguaje es un subconjunto de Move y se puede escribir independientemente del código de negocio.

Resumen

El lenguaje Move ha considerado de manera integral la seguridad en términos de características del lenguaje, ejecución de la máquina virtual y herramientas de seguridad. Puede evitar eficazmente vulnerabilidades comunes como la reentrada y el desbordamiento, pero aún se deben tener en cuenta problemas de autenticación y lógica. Se recomienda a los desarrolladores utilizar servicios de auditoría de terceros y dejar la redacción de las especificaciones a empresas de seguridad, para mejorar aún más la seguridad del contrato.