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

El lenguaje Move, como un nuevo tipo de lenguaje de contratos inteligentes, tuvo en cuenta desde su diseño inicial los problemas de seguridad de la blockchain y los contratos inteligentes, y se basó en algunas ideas de diseño de seguridad del lenguaje Rust. Este artículo explorará 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, en su diseño, ha abandonado mucha lógica no lineal basada en la flexibilidad, no soporta llamadas externas dinámicas y recursivas, sino que introduce conceptos como genéricos, almacenamiento global y recursos para implementar un modelo de programación alternativo. Estas características ayudan a evitar vulnerabilidades comunes en otros lenguajes de contratos inteligentes, como la reentrada.

Los principales componentes del lenguaje Move incluyen:

• Módulo (: compuesto por una serie de tipos de estructura y definiciones de procesos
• Estructuras ): se pueden definir como tipos de recursos, almacenados en un almacenamiento de clave/valor global persistente.
• proceso ( función ): definir las funciones específicas del contrato

Los dos conceptos importantes del lenguaje Move son el tipo de recurso y el almacenamiento global. El almacenamiento global permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos programáticamente por el módulo que los posee, pero se almacenan en un libro mayor público para su visualización. El tipo de recurso asegura el acceso exclusivo al almacenamiento global.

El lenguaje Move garantiza la seguridad del código en el momento de la compilación a través de dos mecanismos: la verificación de invariantes y el verificador de bytecode.

• Comprobación de invariante: definición de la conservación del estado del sistema a través de un lenguaje de especificación
• Verificador de bytecode: realiza la verificación de tipos de seguridad y linealización, incluyendo la verificación de la validez de estructuras, la detección semántica de la lógica del proceso y la verificación de errores en tiempo de enlace, entre otros.

2. Mecanismo de funcionamiento de Move

El programa Move se ejecuta en una máquina virtual, y durante su ejecución no puede acceder a la memoria del sistema, lo que garantiza una ejecución segura en un entorno no confiable.

El programa Move se ejecuta en la pila, y su estado está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Las instrucciones de bytecode de Move se ejecutan en un intérprete de pila, lo que facilita la copia y el control del movimiento entre variables.

Move VM separa el almacenamiento de datos y la pila de llamadas, lo cual es muy diferente de EVM. El estado del usuario se almacena de forma independiente, las llamadas a los programas deben cumplir con las reglas de permisos y recursos, mejorando la seguridad y la eficiencia de ejecución a costa de cierta flexibilidad.

3. Mover Prover

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

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

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

Resumen

El lenguaje Move ha tenido en cuenta de manera integral la seguridad en características del lenguaje, ejecución en máquinas virtuales y herramientas de seguridad. Puede evitar eficazmente vulnerabilidades comunes como la reentrada, desbordamientos e inyecciones, pero aún no puede evitar completamente problemas de autenticación y lógica. Se recomienda a los desarrolladores de contratos inteligentes de Move utilizar servicios de auditoría de seguridad de terceros y encargar la redacción de código de especificación de verificación.