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:
Verificació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: 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:
Recibir el archivo fuente de Move y las especificaciones
Compilar a bytecode y modelo de objeto del validador
Convertir a un lenguaje intermedio Boogie
Generar condiciones de verificación
Verificación usando el solucionador Z3
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.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
17 me gusta
Recompensa
17
8
Compartir
Comentar
0/400
HashBard
· hace8h
todavía hay exploits... teatro de seguridad en su máxima expresión, para ser honesto
Ver originalesResponder0
AirdropHarvester
· hace20h
alcista crítico ¡La seguridad es lo primero!
Ver originalesResponder0
CryptoNomics
· hace20h
*suspiro* yet another L1 attempting formal verification... estadísticamente insignificante sin un análisis adecuado de equilibrio de Nash en mi opinión.
Ver originalesResponder0
ForumMiningMaster
· hace20h
Me gusta este tipo de activos seguros.
Ver originalesResponder0
DegenGambler
· hace20h
¿La revisión estática es suficiente?
Ver originalesResponder0
ponzi_poet
· hace20h
Tendremos que ver el desempeño específico, la estática es solo estática.
Ver originalesResponder0
fork_in_the_road
· hace20h
¿Todavía escribiendo solidity? ¡Rápido, introducir una posición Move!
Ver originalesResponder0
DaoTherapy
· hace20h
Finalmente encontré un lenguaje de contrato confiable.
Análisis completo de la seguridad del lenguaje Move: desde características hasta herramientas de verificación
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:
Verificació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: 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:
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:
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.