Análisis de la seguridad del lenguaje Move

El lenguaje Move, como un nuevo lenguaje de contratos inteligentes de nueva generación, tuvo en cuenta desde su diseño inicial los problemas de seguridad relacionados con la blockchain y los contratos inteligentes. Este artículo analizará la 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

El lenguaje Move ha descartado muchas características de lenguaje flexibles pero inseguras, como la despachación dinámica, las llamadas externas recursivas, etc., y ha adoptado conceptos como tipos de recursos y almacenamiento global para implementar un modelo de programación seguro.

Las principales características de seguridad de Move incluyen:

• Modular: encapsular y gestionar código y recursos a través de módulos
• Tipo de recurso: utilizado para representar y gestionar activos digitales
• Almacenamiento global: proporciona capacidad de almacenamiento persistente
• Sistema de tipos estático: verificación de tipos en tiempo de compilación
• Lógica lineal: asegurar la unicidad y no replicabilidad de los recursos

Move también proporciona dos mecanismos de verificación estática importantes:

1. Invariantes: se utilizan para declarar y verificar la invarianza del estado del sistema
2. Verificador de bytecode: impone la seguridad de tipos y la lógica lineal a nivel de bytecode.

Estas características y mecanismos pueden detectar y prevenir muchos problemas de seguridad comunes en el momento de la compilació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, garantizando así la seguridad en tiempo de ejecución. MoveVM utiliza una estructura de pila, gestionando por separado el almacenamiento de datos y la pila de llamadas:

• El almacenamiento global se divide en memoria ( pila ) y variables globales ( pila )
• Usar la pila de llamadas para gestionar las llamadas a funciones
• La instrucción se ejecuta en el intérprete de pila
• El valor de los recursos solo puede ser movido, no puede ser copiado
• Llamada a función estática, evitar la dispatch dinámico

Este diseño mejora la eficiencia de ejecución y la seguridad, previniendo eficazmente ataques como el de reentrada.

3. Mover Prover

Move Prover es una herramienta de verificación formal proporcionada por el lenguaje Move, que permite realizar análisis de seguridad automatizados. Utiliza un algoritmo de verificación deductiva para validar la corrección de los programas, basado en las especificaciones escritas en el Lenguaje de Especificación Move.

Flujo de trabajo de Move Prover:

1. Análisis del código fuente y normas de Move
2. Generar modelo de objeto validador
3. Convertir a lenguaje intermedio Boogie
4. Generar condiciones de verificación
5. Verificación con el solucionador SMT Z3
6. Generar informe de resultados de verificación

Move Prover es una poderosa herramienta auxiliar que puede ayudar a los desarrolladores a mejorar la seguridad de los contratos inteligentes.

Resumen

El lenguaje Move ha considerado la seguridad de manera integral en varios niveles, como el diseño del lenguaje, la ejecución de la máquina virtual y las herramientas de verificación. Puede evitar de manera efectiva muchas vulnerabilidades comunes de los contratos inteligentes, pero los desarrolladores aún deben mantenerse alerta y se sugiere utilizar servicios de auditoría de seguridad de terceros para garantizar aún más la seguridad del contrato.