Análisis de la seguridad del lenguaje Move: avances en el nuevo lenguaje de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes diseñado para entornos de blockchain, con características de seguridad únicas. Este artículo explora 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 ha abandonado características más flexibles pero inseguras, como la dispatch dinámica y las llamadas externas recursivas, optando en su lugar por conceptos como genéricos, almacenamiento global y recursos para implementar patrones de programación alternativos. Estos diseños ayudan a evitar vulnerabilidades comunes como la reentrada.
El mecanismo de seguridad central de Move incluye:
Módulo: cada módulo consiste en un tipo de estructura y una definición de proceso, puede importar definiciones de tipo de otros módulos y llamar a sus procesos.
Estructura: puede definirse como un tipo de recurso, almacenado en el almacenamiento de clave-valor global.
Proceso: define las funciones y la lógica del contrato.
Almacenamiento global: permite el almacenamiento persistente de datos, que solo pueden ser leídos y escritos por los módulos que los poseen de manera programática.
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: aplica un sistema de tipos a nivel de bytecode para prevenir operaciones ilegales sobre valores sensibles.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en la máquina virtual y no puede acceder directamente a la memoria del sistema. MoveVM utiliza un intérprete basado en pila para ejecutar instrucciones de bytecode, gestionando por separado el almacenamiento de datos y la pila de llamadas.
El estado del programa Move está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Durante la ejecución, la pila de llamadas guarda información de contexto, el salto estático evita la asignación dinámica, lo que refuerza la inmutabilidad de las llamadas a funciones.
Este diseño separa el estado del usuario (, los recursos ) y la lógica del programa, mejorando 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 los programas cumplen con las expectativas. Su flujo de trabajo es el siguiente:
Recibir el archivo fuente Move y las especificaciones
Compilar en bytecode y modelo de objeto validador
Convertir a lenguaje intermedio Boogie
Generar condiciones de verificación
Utilizar el solucionador Z3 para verificar la satisfacibilidad de la fórmula
Generar informe de diagnóstico
El Lenguaje de Especificación de Movimiento se utiliza para describir las especificaciones del comportamiento de los programas, y se puede escribir de forma independiente del código de negocio. Esto proporciona a las empresas de seguridad de terceros una vía adicional de verificación.
Resumen
El lenguaje Move ha sido diseñado teniendo en cuenta la seguridad, con una optimización integral que abarca desde las características del lenguaje, la ejecución de la máquina virtual hasta las herramientas de verificación. Puede evitar eficazmente vulnerabilidades comunes como reentradas y desbordamientos, pero aún se deben considerar problemas de seguridad en aspectos como la autenticación y la lógica.
Aunque Move ofrece una buena garantía de seguridad, se recomienda que los desarrolladores utilicen servicios de auditoría de terceros y consideren dejar la redacción y verificación de las especificaciones a un equipo de seguridad profesional para mejorar aún más la seguridad de los contratos inteligentes.
Esta página puede contener contenido de terceros, que se proporciona únicamente con fines informativos (sin garantías ni declaraciones) y no debe considerarse como un respaldo por parte de Gate a las opiniones expresadas ni como asesoramiento financiero o profesional. Consulte el Descargo de responsabilidad para obtener más detalles.
8 me gusta
Recompensa
8
5
Compartir
Comentar
0/400
MEVHunterLucky
· 07-20 19:12
Ha llegado otra vez el movimiento de especulación.
Ver originalesResponder0
MEVHunterBearish
· 07-20 19:11
move aún tiene que trepar
Ver originalesResponder0
¯\_(ツ)_/¯
· 07-20 19:11
Pruebas son pruebas, la seguridad es lo primero
Ver originalesResponder0
LowCapGemHunter
· 07-20 19:07
Me voy, me voy. La auditoría sigue siendo la más confiable.
Análisis de las características de seguridad del lenguaje Move: crear un entorno de desarrollo de contratos inteligentes más seguro
Análisis de la seguridad del lenguaje Move: avances en el nuevo lenguaje de contratos inteligentes
El lenguaje Move es un lenguaje de contratos inteligentes diseñado para entornos de blockchain, con características de seguridad únicas. Este artículo explora 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 ha abandonado características más flexibles pero inseguras, como la dispatch dinámica y las llamadas externas recursivas, optando en su lugar por conceptos como genéricos, almacenamiento global y recursos para implementar patrones de programación alternativos. Estos diseños ayudan a evitar vulnerabilidades comunes como la reentrada.
El mecanismo de seguridad central de Move incluye:
Módulo: cada módulo consiste en un tipo de estructura y una definición de proceso, puede importar definiciones de tipo de otros módulos y llamar a sus procesos.
Estructura: puede definirse como un tipo de recurso, almacenado en el almacenamiento de clave-valor global.
Proceso: define las funciones y la lógica del contrato.
Almacenamiento global: permite el almacenamiento persistente de datos, que solo pueden ser leídos y escritos por los módulos que los poseen de manera programática.
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: aplica un sistema de tipos a nivel de bytecode para prevenir operaciones ilegales sobre valores sensibles.
2. Mecanismo de funcionamiento de Move
El programa Move se ejecuta en la máquina virtual y no puede acceder directamente a la memoria del sistema. MoveVM utiliza un intérprete basado en pila para ejecutar instrucciones de bytecode, gestionando por separado el almacenamiento de datos y la pila de llamadas.
El estado del programa Move está compuesto por la pila de llamadas, la memoria, las variables globales y las operaciones. Durante la ejecución, la pila de llamadas guarda información de contexto, el salto estático evita la asignación dinámica, lo que refuerza la inmutabilidad de las llamadas a funciones.
Este diseño separa el estado del usuario (, los recursos ) y la lógica del programa, mejorando 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 los programas cumplen con las expectativas. Su flujo de trabajo es el siguiente:
El Lenguaje de Especificación de Movimiento se utiliza para describir las especificaciones del comportamiento de los programas, y se puede escribir de forma independiente del código de negocio. Esto proporciona a las empresas de seguridad de terceros una vía adicional de verificación.
Resumen
El lenguaje Move ha sido diseñado teniendo en cuenta la seguridad, con una optimización integral que abarca desde las características del lenguaje, la ejecución de la máquina virtual hasta las herramientas de verificación. Puede evitar eficazmente vulnerabilidades comunes como reentradas y desbordamientos, pero aún se deben considerar problemas de seguridad en aspectos como la autenticación y la lógica.
Aunque Move ofrece una buena garantía de seguridad, se recomienda que los desarrolladores utilicen servicios de auditoría de terceros y consideren dejar la redacción y verificación de las especificaciones a un equipo de seguridad profesional para mejorar aún más la seguridad de los contratos inteligentes.