Análisis de la seguridad del lenguaje Move

El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de próxima generación, consideró desde su diseño inicial los problemas de seguridad de la blockchain y los contratos inteligentes. Este artículo explorará la seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismos de funcionamiento y herramientas de verificación.

1. Características de seguridad del lenguaje Move

El lenguaje Move ha abandonado la lógica no lineal basada en la flexibilidad, no admite la distribución dinámica ni las llamadas externas recursivas, y utiliza conceptos como genéricos, almacenamiento global, recursos, entre otros, para implementar un modelo de programación alternativo. Este diseño ayuda a evitar vulnerabilidades de seguridad como la reentrada.

Los principales componentes del lenguaje Move incluyen:

• Módulo: compuesto por definiciones de tipo de estructura y proceso, puede importar definiciones de tipo de otros módulos y llamar a procesos de otros módulos.

• Estructura: se puede definir como un tipo de recurso, almacenado en el almacenamiento clave-valor global.

• Proceso: definir la funcionalidad del módulo, que puede incluir procesos de inicialización, seguros y no seguros.

El mecanismo de almacenamiento global del lenguaje Move permite a los módulos almacenar datos persistentes y tener acceso exclusivo de lectura y escritura a los tipos de recursos que declaran. Este mecanismo ayuda a hacer cumplir las restricciones de seguridad.

Las dos características importantes de comprobación estática del lenguaje Move:

1. Verificación de invariante: Definición de la conservación del estado del sistema a través de un lenguaje de especificación.

2. Verificador de bytecode: impone tipos seguros y linealización, evitando 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. La ejecución del programa se basa en pilas, la memoria global se divide en memoria ( pila ) y variables globales ( pila ).

El estado de ejecución de Move VM está compuesto por la pila de llamadas, la memoria, las variables globales y el conjunto de operaciones. Sus características incluyen:

• Salto estático, evitar la dispatch dinámica
• Llamada de pila adyacente, prevenir reentrada
• Separación de almacenamiento de datos y pila de llamadas

Este diseño mejora la seguridad y la eficiencia de ejecución.

3. Mover Prover

Move Prover es una herramienta de verificación formal que utiliza algoritmos de verificación deductiva para comprobar si un programa cumple con las expectativas. Su flujo de trabajo:

1. Recibir el archivo fuente de Move y las especificaciones
2. Compilar a bytecode y modelo de objeto del validador
3. Convertir a un lenguaje intermedio Boogie
4. Generar condiciones de verificación
5. Verificación usando el solucionador Z3
6. Generar informe de diagnóstico

El lenguaje de especificación de movimiento se utiliza para describir las especificaciones del comportamiento del programa, y se puede escribir de forma independiente del código de negocio.

Resumen

El lenguaje Move tiene en cuenta de manera integral las características del lenguaje, la ejecución de la máquina virtual y las herramientas de seguridad, lo que puede evitar eficazmente muchas vulnerabilidades comunes. Sin embargo, se recomienda utilizar servicios de auditoría de seguridad de terceros y que una empresa de seguridad complete la redacción y verificación del código conforme.