El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en entornos de blockchain que implementan MoveVM. Nació considerando muchos problemas de seguridad de blockchain y contratos inteligentes, y se basó en parte en el diseño de seguridad del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación que tiene como característica principal la seguridad, ¿cuál es realmente la seguridad de Move? ¿Puede evitar en el nivel del lenguaje o a través de mecanismos relacionados las amenazas de seguridad comunes en máquinas virtuales de contratos como EVM y WASM? ¿Existen problemas de seguridad particulares en sí mismo?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de funcionamiento y herramientas de verificación.
1. Características de seguridad del lenguaje Move
Es difícil escribir código correcto, y incluso después de múltiples pruebas, no se puede garantizar que el código esté completamente libre de vulnerabilidades. Es aún más complicado escribir código que mantenga las propiedades de seguridad clave al interactuar con código no confiable. Existen muchas técnicas que pueden hacer cumplir la seguridad en tiempo de ejecución, como sandboxing, aislamiento de procesos, bloqueo de objetos y otros patrones de programación; también se puede especificar seguridad estática en tiempo de compilación, como tipos estáticos obligatorios o verificaciones de aserciones.
A veces también se pueden utilizar herramientas de análisis semántico y análisis estático para asegurar que el código cumpla con las reglas de seguridad, incluso cuando interactúa con código no confiable, se pueden mantener ciertas invariantes lógicas demostrables.
Estas soluciones parecen buenas, pueden evitar sobrecargas en tiempo de ejecución y detectar problemas de seguridad de antemano. Pero, lamentablemente, la seguridad que los lenguajes de programación obtienen a través de estos métodos es extremadamente limitada, principalmente por dos razones: primero, a menudo tienen características que no pueden ser analizadas utilizando herramientas de análisis estático, como la dispatch dinámica, la mutabilidad compartida y la reflexión, que violan las reglas de invarianza de seguridad, proporcionando a los hackers una amplia superficie de ataque. Segundo, la mayoría de los lenguajes de programación son difíciles de extender con herramientas estáticas relacionadas con la seguridad o lenguajes de especificación expresiva. A pesar de que ambas extensiones son importantes, pueden ser definidas de antemano.
A diferencia de muchos lenguajes de programación existentes, el lenguaje Move fue diseñado teniendo en cuenta el soporte para escribir programas que interactúen de manera segura con código no confiable, al mismo tiempo que admite la verificación estática. Move tiene estas características de seguridad porque ha abandonado toda lógica no lineal basada en consideraciones de flexibilidad, no admite despacho dinámico y tampoco llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de programación dinámica y las llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes pueden dar lugar a costosas vulnerabilidades de reentrada.
Para entender mejor las características del lenguaje Move, veamos un programa de ejemplo:
mover
módulo 0x1::TestCoin {
usar 0x1::signer;
const ADMIN: address = @0x1;
struct Coin tiene clave, almacena {
valor: u64
}
struct Info tiene la clave {
total_supply: u64
}
módulo de especificación {
invariante para todo addr: dirección donde existe<coin>(addr):
global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}
public fun initialize(account: &signer) {
assert!(signer::address_of(account) == ADMIN, 0);
mover_a(cuenta, Info { suministro_total: 0 })
}
public fun mint(account: &signer, amount: u64): Coin acquires Info {
assert!(signer::address_of(account) == ADMIN, 0);
let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
supply.total_supply = supply.total_supply + amount;
Moneda { valor: cantidad }
}
public fun value(coin: &Coin): u64 {
coin.value
}
public fun value_mut(coin: &mut Coin): &mut u64 {
&mut coin.value
}
}
a) Módulo(: Cada módulo Move está compuesto por una serie de tipos de estructura y definiciones de procesos. Los módulos pueden importar definiciones de tipos y llamar a procesos declarados en otros módulos. El nombre completo del módulo comienza con la dirección de cuenta de 16 bytes que almacena el código del módulo. La dirección de la cuenta se utiliza como espacio de nombres para distinguir módulos con el mismo nombre.
b) Estructuras): Este módulo define dos estructuras Coin e Info. Coin representa los tokens asignados a los usuarios, Info registra la cantidad total de tokens. Ambas estructuras se definen como tipos de recursos y se pueden almacenar en un almacenamiento clave/valor global persistente.
c( proceso)función): el código define un proceso de inicialización, un proceso seguro y un proceso no seguro. Antes de crear Coin, se debe llamar al proceso de inicialización para establecer el valor total_supply de la instancia Info en cero. signer es un tipo especial que representa a un usuario validado por la lógica externa de Move. La aserción asegura que solo la cuenta de administrador designada puede llamar a este proceso. El proceso mint permite al administrador crear nuevos tokens, también con control de acceso. El proceso value_mut acepta una referencia mutable de Coin y devuelve una referencia mutable al campo value.
La estructura del contrato es similar a otros lenguajes de contratos inteligentes, pero los tipos de recursos y el almacenamiento global son mecanismos clave para la seguridad del almacenamiento y los recursos en el lenguaje Move.
El almacenamiento global permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos por el módulo que los posee de manera programática, pero se almacenan en un libro mayor público, donde los usuarios de otros módulos pueden verlos. Cada clave en el almacenamiento global está compuesta por un nombre de tipo completamente calificado y la dirección de la cuenta que almacena el valor de ese tipo. Aunque el almacenamiento global se comparte entre todos los módulos, cada módulo tiene acceso exclusivo de lectura y escritura a las claves que declara.
El módulo que declara el tipo de recurso puede:
• Publicar valores en el almacenamiento global mediante la instrucción move_to
• Eliminar el valor del almacenamiento global mediante la instrucción move_from
• Obtener una referencia al valor en el almacenamiento global a través de la instrucción borrow_global_mut
El módulo puede imponer restricciones en el almacenamiento global que controla. Por ejemplo, asegurar que solo la dirección de la cuenta ADMIN pueda poseer la estructura de tipo Info, implementado a través de la definición del proceso initialize, que utiliza move_to en el tipo Info y aplica la condición previa de que move_to se llame en la dirección ADMIN.
Las siguientes son dos características de verificación estática que garantizan la seguridad del código de este módulo: reducción invariante y verificador de bytecode.
a( Comprobación de invariante ) Verificación de la especificación ): La línea 10 del módulo indica la invariante de la comprobación estática: la suma de los campos de valor de todos los objetos Coin en el sistema debe ser igual al campo total_value del objeto Info almacenado en la dirección ADMIN. La invariante es un término en la verificación formal que indica la conservación del estado. Esta propiedad de conservación se aplica a todos los posibles clientes del módulo.
b( Verificador de bytecode: los tipos de seguridad y la linealización son el alcance principal de la verificación del bytecode. Aunque otros módulos no pueden acceder a la unidad de almacenamiento global controlada por 0x1::TestCoin::Coin, pueden utilizar este tipo en sus propias declaraciones de procesos y estructuras.
Move tiene un verificador de bytecode ) que impone un sistema de tipos a nivel de bytecode ), permitiendo a los propietarios de módulos prevenir resultados no deseados. Solo los módulos que declaran el tipo de estructura Coin pueden:
• Crear un valor de tipo Coin
• Desempaquetar el valor del tipo de moneda "Coin" en sus campos componentes
• Obtener una referencia al campo Coin a través de un préstamo mutable o inmutable al estilo de rust
El validador también impone que la estructura predeterminada sea lineal, para garantizar que se evite linealmente la copia y destrucción fuera del módulo que declara la estructura. Al mismo tiempo, el validador también realizará chequeos forzados sobre algunos tipos de problemas comunes de memoria.
El proceso de detección se divide principalmente en tres categorías:
1( Verificación de la validez de la estructura: garantizar la integridad del bytecode, detectar referencias ilegales de errores, entidades de recursos duplicadas y firmas de tipo ilegales, etc.
2) Detección semántica de la lógica del proceso: incluye errores de tipo de parámetro, índices de bucle, índices nulos y variables definidas repetidamente.
3) Error al vincular, llamada interna ilegal al proceso, o flujo de declaración y definición de enlace no coincidentes.
El validador primero crea el gráfico de flujo de control CFG), luego verifica el alcance de acceso del llamador en la pila, asegurando que el llamador del contrato no pueda acceder al espacio de pila del llamador. Al mismo tiempo, para verificar tipos, cada pila de Value mantiene su correspondiente pila de Type.
A continuación se encuentran las comprobaciones de recursos y referencias. La verificación de recursos se centra principalmente en restricciones como no doble gasto, no destrucción y pertenencia obligatoria. La verificación de referencias combina análisis dinámico y estático, utilizando un mecanismo de comprobación de préstamos similar al sistema de tipos de Rust.
Por último, se debe realizar una verificación de los enlaces, revisando si los objetos de enlace y las declaraciones coinciden, así como el control de acceso del proceso.
![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(
) 2. Mecanismo de funcionamiento de Move
Primero, el programa Move se ejecuta en una máquina virtual y no puede acceder a la memoria del sistema durante la ejecución. Esto permite que Move se ejecute de manera segura en un entorno no confiable, sin ser destruido o abusado.
En segundo lugar, el programa Move se ejecuta en la pila. El almacenamiento global se divide en memoria (, pila ) y variables globales ###. La memoria es un almacenamiento de primer nivel, cuyas unidades no pueden almacenar punteros que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, pero el método de indexación es diferente. Al acceder a las variables globales, el código proporciona una dirección y un tipo asociado a esa dirección. Esta división simplifica las operaciones y hace que la semántica del lenguaje Move sea más fácil de formalizar.
Las instrucciones de bytecode Move se ejecutan en un intérprete basado en pila. La máquina virtual basada en pila es fácil de implementar y controlar, requiere menos del entorno de hardware y es adecuada para escenarios de blockchain. En comparación con un intérprete basado en registros, un intérprete basado en pila facilita el control y la detección de copias y movimientos entre variables.
En Move, los valores definidos como recursos solo pueden ser movidos de manera destructiva (, haciendo que la ubicación de almacenamiento que guardaba previamente ese valor sea inválida ), pero ciertos valores (, como los enteros ), pueden ser copiados.
Cuando el programa Move se ejecuta en la pila, su estado es un cuádruple ⟨C, M, G, S⟩, compuesto por la pila de llamadas (C), la memoria (M), las variables globales (G) y los operandos (S). La pila también mantiene una tabla de funciones ( del módulo en sí ) para analizar las instrucciones que contienen el cuerpo de la función.
La pila de llamadas contiene toda la información contextual y los números de instrucción de la ejecución del proceso. Al ejecutar la instrucción Call, se crea un nuevo objeto de pila de llamadas, se almacenan los parámetros de llamada en la memoria y en las variables globales, y luego el intérprete ejecuta las instrucciones del nuevo contrato. Cuando se encuentra una instrucción de bifurcación, se produce un salto estático dentro de este proceso. La dependencia de los procedimientos dentro del módulo es acíclica, y dado que no hay asignación dinámica en el módulo, se refuerza la inmutabilidad de las llamadas a funciones durante la ejecución: el marco de llamada del proceso procedure debe ser adyacente, evitando así la posibilidad de reentrada. La llamada return finaliza la llamada, colocando el valor de retorno en la parte superior de la pila.
El estudio del código de MoveVM revela que MoveVM separa la lógica del proceso de almacenamiento de datos y la pila de llamadas (, lo cual es la mayor diferencia con EVM. En EVM, la implementación del token ERC20 requiere que la lógica esté escrita en un único contrato y que se registre el estado de cada usuario, mientras que en MoveVM, el estado del usuario ) se almacena de forma independiente bajo la dirección de la cuenta (, y las llamadas al programa deben cumplir con reglas de autorización y reglas obligatorias sobre los recursos. Aunque esto sacrifica cierta flexibilidad, ayuda a lograr un gran aumento en la seguridad y la eficiencia de ejecución ), lo que permite una ejecución concurrente (.
![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
) 3. Mover Prover
Por último, conozcamos la herramienta de auditoría automatizada asistida que ofrece Move, Move prover.
Move Prover es una herramienta de verificación formal basada en la inferencia. Utiliza un lenguaje formal para describir el comportamiento del programa y algoritmos de inferencia para verificar si el programa cumple con lo esperado, ayudando a los desarrolladores a garantizar la corrección de los contratos inteligentes y reducir el riesgo de transacciones. En pocas palabras, la verificación formal consiste en usar métodos matemáticos para probar que el sistema está libre de errores.
Los algoritmos de verificación automática de software más utilizados actualmente se basan en el solucionador SMT (. El solucionador SMT es, en realidad, un solucionador de fórmulas. Los algoritmos de verificación de software de nivel superior descomponen el objetivo de verificación en fórmulas, que se entregan al solucionador SMT para su resolución, analizan más a fondo según los resultados y finalmente informan si el objetivo de verificación se cumple o si se encuentra un contraejemplo.
El algoritmo de verificación básica es la verificación deductiva )deductive verification(, y hay otros algoritmos de verificación como la verificación de modelos acotados, el método de inducción k, la abstracción de predicados y la abstracción de caminos, entre otros.
Move Prover utiliza un algoritmo de verificación deductiva para validar si un programa cumple con las expectativas. Esto significa que Move Prover puede inferir el comportamiento del programa según la información conocida, asegurando que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reduce la carga de trabajo de las pruebas manuales.
La arquitectura general de Move Prover es la siguiente:
Primero, Move Prover recibe archivos fuente de Move que contienen la especificación de entrada del programa )specification###. Move Parser extrae la especificación del código fuente. El compilador de Move compila el archivo fuente en bytecode, que junto con el sistema de especificaciones se convierte en el modelo de objeto del verificador (Prover Object Model).
El modelo se traduce al lenguaje intermedio Boogie. El código Boogie se pasa al sistema de verificación Boogie para realizar la "generación de condiciones de verificación". Las condiciones de verificación se pasan al solucionador Z3 (, un solucionador SMT desarrollado por Microsoft ).
Después de que VC se pase a Z3, el verificador comprueba si el código del programa de la fórmula SMT ( cumple con la especificación ) y si es insatisfacible. Si es así, se indica que la especificación es válida. De lo contrario, se genera un modelo que satisface las condiciones, se convierte de nuevo al formato Boogie y se emite un informe de diagnóstico. El informe de diagnóstico se restaura a errores a nivel de código fuente similares a los errores estándar de compiladores.
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.
17 me gusta
Recompensa
17
5
Republicar
Compartir
Comentar
0/400
SchrodingerAirdrop
· 08-09 21:11
move aún no es lo suficientemente seguro, créeme
Ver originalesResponder0
DataBartender
· 08-07 02:38
Otra vez están exagerando sobre move.
Ver originalesResponder0
AirdropHarvester
· 08-07 02:29
¿Moverse? Suena complicado, tan difícil de aprender como Rust.
Ver originalesResponder0
MoneyBurner
· 08-07 02:28
De nuevo intentan engañarme para introducir una posición y ver la nueva cadena pública, la última vez perdí mucho.
Ver originalesResponder0
StableNomad
· 08-07 02:28
hmm otro lenguaje "seguro"... me recuerda a solana en 2021, la verdad
Análisis profundo de la seguridad del lenguaje Move: características del lenguaje, mecanismo de ejecución y auditoría automatizada
Introducción
El lenguaje Move es un lenguaje de contratos inteligentes que se puede ejecutar en entornos de blockchain que implementan MoveVM. Nació considerando muchos problemas de seguridad de blockchain y contratos inteligentes, y se basó en parte en el diseño de seguridad del lenguaje RUST. Como un lenguaje de contratos inteligentes de nueva generación que tiene como característica principal la seguridad, ¿cuál es realmente la seguridad de Move? ¿Puede evitar en el nivel del lenguaje o a través de mecanismos relacionados las amenazas de seguridad comunes en máquinas virtuales de contratos como EVM y WASM? ¿Existen problemas de seguridad particulares en sí mismo?
Este artículo explorará los problemas de seguridad del lenguaje Move desde tres aspectos: características del lenguaje, mecanismo de funcionamiento y herramientas de verificación.
1. Características de seguridad del lenguaje Move
Es difícil escribir código correcto, y incluso después de múltiples pruebas, no se puede garantizar que el código esté completamente libre de vulnerabilidades. Es aún más complicado escribir código que mantenga las propiedades de seguridad clave al interactuar con código no confiable. Existen muchas técnicas que pueden hacer cumplir la seguridad en tiempo de ejecución, como sandboxing, aislamiento de procesos, bloqueo de objetos y otros patrones de programación; también se puede especificar seguridad estática en tiempo de compilación, como tipos estáticos obligatorios o verificaciones de aserciones.
A veces también se pueden utilizar herramientas de análisis semántico y análisis estático para asegurar que el código cumpla con las reglas de seguridad, incluso cuando interactúa con código no confiable, se pueden mantener ciertas invariantes lógicas demostrables.
Estas soluciones parecen buenas, pueden evitar sobrecargas en tiempo de ejecución y detectar problemas de seguridad de antemano. Pero, lamentablemente, la seguridad que los lenguajes de programación obtienen a través de estos métodos es extremadamente limitada, principalmente por dos razones: primero, a menudo tienen características que no pueden ser analizadas utilizando herramientas de análisis estático, como la dispatch dinámica, la mutabilidad compartida y la reflexión, que violan las reglas de invarianza de seguridad, proporcionando a los hackers una amplia superficie de ataque. Segundo, la mayoría de los lenguajes de programación son difíciles de extender con herramientas estáticas relacionadas con la seguridad o lenguajes de especificación expresiva. A pesar de que ambas extensiones son importantes, pueden ser definidas de antemano.
A diferencia de muchos lenguajes de programación existentes, el lenguaje Move fue diseñado teniendo en cuenta el soporte para escribir programas que interactúen de manera segura con código no confiable, al mismo tiempo que admite la verificación estática. Move tiene estas características de seguridad porque ha abandonado toda lógica no lineal basada en consideraciones de flexibilidad, no admite despacho dinámico y tampoco llamadas externas recursivas, sino que utiliza conceptos como genéricos, almacenamiento global y recursos para implementar algunos patrones de programación alternativos. Por ejemplo, Move omite las características de programación dinámica y las llamadas recursivas, las cuales en otros lenguajes de contratos inteligentes pueden dar lugar a costosas vulnerabilidades de reentrada.
Para entender mejor las características del lenguaje Move, veamos un programa de ejemplo:
mover módulo 0x1::TestCoin { usar 0x1::signer;
}
a) Módulo(: Cada módulo Move está compuesto por una serie de tipos de estructura y definiciones de procesos. Los módulos pueden importar definiciones de tipos y llamar a procesos declarados en otros módulos. El nombre completo del módulo comienza con la dirección de cuenta de 16 bytes que almacena el código del módulo. La dirección de la cuenta se utiliza como espacio de nombres para distinguir módulos con el mismo nombre.
b) Estructuras): Este módulo define dos estructuras Coin e Info. Coin representa los tokens asignados a los usuarios, Info registra la cantidad total de tokens. Ambas estructuras se definen como tipos de recursos y se pueden almacenar en un almacenamiento clave/valor global persistente.
c( proceso)función): el código define un proceso de inicialización, un proceso seguro y un proceso no seguro. Antes de crear Coin, se debe llamar al proceso de inicialización para establecer el valor total_supply de la instancia Info en cero. signer es un tipo especial que representa a un usuario validado por la lógica externa de Move. La aserción asegura que solo la cuenta de administrador designada puede llamar a este proceso. El proceso mint permite al administrador crear nuevos tokens, también con control de acceso. El proceso value_mut acepta una referencia mutable de Coin y devuelve una referencia mutable al campo value.
La estructura del contrato es similar a otros lenguajes de contratos inteligentes, pero los tipos de recursos y el almacenamiento global son mecanismos clave para la seguridad del almacenamiento y los recursos en el lenguaje Move.
El almacenamiento global permite que los programas Move almacenen datos persistentes, los cuales solo pueden ser leídos y escritos por el módulo que los posee de manera programática, pero se almacenan en un libro mayor público, donde los usuarios de otros módulos pueden verlos. Cada clave en el almacenamiento global está compuesta por un nombre de tipo completamente calificado y la dirección de la cuenta que almacena el valor de ese tipo. Aunque el almacenamiento global se comparte entre todos los módulos, cada módulo tiene acceso exclusivo de lectura y escritura a las claves que declara.
El módulo que declara el tipo de recurso puede: • Publicar valores en el almacenamiento global mediante la instrucción move_to • Eliminar el valor del almacenamiento global mediante la instrucción move_from • Obtener una referencia al valor en el almacenamiento global a través de la instrucción borrow_global_mut
El módulo puede imponer restricciones en el almacenamiento global que controla. Por ejemplo, asegurar que solo la dirección de la cuenta ADMIN pueda poseer la estructura de tipo Info, implementado a través de la definición del proceso initialize, que utiliza move_to en el tipo Info y aplica la condición previa de que move_to se llame en la dirección ADMIN.
Las siguientes son dos características de verificación estática que garantizan la seguridad del código de este módulo: reducción invariante y verificador de bytecode.
a( Comprobación de invariante ) Verificación de la especificación ): La línea 10 del módulo indica la invariante de la comprobación estática: la suma de los campos de valor de todos los objetos Coin en el sistema debe ser igual al campo total_value del objeto Info almacenado en la dirección ADMIN. La invariante es un término en la verificación formal que indica la conservación del estado. Esta propiedad de conservación se aplica a todos los posibles clientes del módulo.
b( Verificador de bytecode: los tipos de seguridad y la linealización son el alcance principal de la verificación del bytecode. Aunque otros módulos no pueden acceder a la unidad de almacenamiento global controlada por 0x1::TestCoin::Coin, pueden utilizar este tipo en sus propias declaraciones de procesos y estructuras.
Move tiene un verificador de bytecode ) que impone un sistema de tipos a nivel de bytecode ), permitiendo a los propietarios de módulos prevenir resultados no deseados. Solo los módulos que declaran el tipo de estructura Coin pueden: • Crear un valor de tipo Coin • Desempaquetar el valor del tipo de moneda "Coin" en sus campos componentes • Obtener una referencia al campo Coin a través de un préstamo mutable o inmutable al estilo de rust
El validador también impone que la estructura predeterminada sea lineal, para garantizar que se evite linealmente la copia y destrucción fuera del módulo que declara la estructura. Al mismo tiempo, el validador también realizará chequeos forzados sobre algunos tipos de problemas comunes de memoria.
El proceso de detección se divide principalmente en tres categorías: 1( Verificación de la validez de la estructura: garantizar la integridad del bytecode, detectar referencias ilegales de errores, entidades de recursos duplicadas y firmas de tipo ilegales, etc. 2) Detección semántica de la lógica del proceso: incluye errores de tipo de parámetro, índices de bucle, índices nulos y variables definidas repetidamente. 3) Error al vincular, llamada interna ilegal al proceso, o flujo de declaración y definición de enlace no coincidentes.
El validador primero crea el gráfico de flujo de control CFG), luego verifica el alcance de acceso del llamador en la pila, asegurando que el llamador del contrato no pueda acceder al espacio de pila del llamador. Al mismo tiempo, para verificar tipos, cada pila de Value mantiene su correspondiente pila de Type.
A continuación se encuentran las comprobaciones de recursos y referencias. La verificación de recursos se centra principalmente en restricciones como no doble gasto, no destrucción y pertenencia obligatoria. La verificación de referencias combina análisis dinámico y estático, utilizando un mecanismo de comprobación de préstamos similar al sistema de tipos de Rust.
Por último, se debe realizar una verificación de los enlaces, revisando si los objetos de enlace y las declaraciones coinciden, así como el control de acceso del proceso.
![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(
) 2. Mecanismo de funcionamiento de Move
Primero, el programa Move se ejecuta en una máquina virtual y no puede acceder a la memoria del sistema durante la ejecución. Esto permite que Move se ejecute de manera segura en un entorno no confiable, sin ser destruido o abusado.
En segundo lugar, el programa Move se ejecuta en la pila. El almacenamiento global se divide en memoria (, pila ) y variables globales ###. La memoria es un almacenamiento de primer nivel, cuyas unidades no pueden almacenar punteros que apunten a unidades de memoria. Las variables globales se utilizan para almacenar punteros que apuntan a unidades de memoria, pero el método de indexación es diferente. Al acceder a las variables globales, el código proporciona una dirección y un tipo asociado a esa dirección. Esta división simplifica las operaciones y hace que la semántica del lenguaje Move sea más fácil de formalizar.
Las instrucciones de bytecode Move se ejecutan en un intérprete basado en pila. La máquina virtual basada en pila es fácil de implementar y controlar, requiere menos del entorno de hardware y es adecuada para escenarios de blockchain. En comparación con un intérprete basado en registros, un intérprete basado en pila facilita el control y la detección de copias y movimientos entre variables.
En Move, los valores definidos como recursos solo pueden ser movidos de manera destructiva (, haciendo que la ubicación de almacenamiento que guardaba previamente ese valor sea inválida ), pero ciertos valores (, como los enteros ), pueden ser copiados.
Cuando el programa Move se ejecuta en la pila, su estado es un cuádruple ⟨C, M, G, S⟩, compuesto por la pila de llamadas (C), la memoria (M), las variables globales (G) y los operandos (S). La pila también mantiene una tabla de funciones ( del módulo en sí ) para analizar las instrucciones que contienen el cuerpo de la función.
La pila de llamadas contiene toda la información contextual y los números de instrucción de la ejecución del proceso. Al ejecutar la instrucción Call, se crea un nuevo objeto de pila de llamadas, se almacenan los parámetros de llamada en la memoria y en las variables globales, y luego el intérprete ejecuta las instrucciones del nuevo contrato. Cuando se encuentra una instrucción de bifurcación, se produce un salto estático dentro de este proceso. La dependencia de los procedimientos dentro del módulo es acíclica, y dado que no hay asignación dinámica en el módulo, se refuerza la inmutabilidad de las llamadas a funciones durante la ejecución: el marco de llamada del proceso procedure debe ser adyacente, evitando así la posibilidad de reentrada. La llamada return finaliza la llamada, colocando el valor de retorno en la parte superior de la pila.
El estudio del código de MoveVM revela que MoveVM separa la lógica del proceso de almacenamiento de datos y la pila de llamadas (, lo cual es la mayor diferencia con EVM. En EVM, la implementación del token ERC20 requiere que la lógica esté escrita en un único contrato y que se registre el estado de cada usuario, mientras que en MoveVM, el estado del usuario ) se almacena de forma independiente bajo la dirección de la cuenta (, y las llamadas al programa deben cumplir con reglas de autorización y reglas obligatorias sobre los recursos. Aunque esto sacrifica cierta flexibilidad, ayuda a lograr un gran aumento en la seguridad y la eficiencia de ejecución ), lo que permite una ejecución concurrente (.
![Análisis de seguridad de Move: el cambio de juego del lenguaje de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
) 3. Mover Prover
Por último, conozcamos la herramienta de auditoría automatizada asistida que ofrece Move, Move prover.
Move Prover es una herramienta de verificación formal basada en la inferencia. Utiliza un lenguaje formal para describir el comportamiento del programa y algoritmos de inferencia para verificar si el programa cumple con lo esperado, ayudando a los desarrolladores a garantizar la corrección de los contratos inteligentes y reducir el riesgo de transacciones. En pocas palabras, la verificación formal consiste en usar métodos matemáticos para probar que el sistema está libre de errores.
Los algoritmos de verificación automática de software más utilizados actualmente se basan en el solucionador SMT (. El solucionador SMT es, en realidad, un solucionador de fórmulas. Los algoritmos de verificación de software de nivel superior descomponen el objetivo de verificación en fórmulas, que se entregan al solucionador SMT para su resolución, analizan más a fondo según los resultados y finalmente informan si el objetivo de verificación se cumple o si se encuentra un contraejemplo.
El algoritmo de verificación básica es la verificación deductiva )deductive verification(, y hay otros algoritmos de verificación como la verificación de modelos acotados, el método de inducción k, la abstracción de predicados y la abstracción de caminos, entre otros.
Move Prover utiliza un algoritmo de verificación deductiva para validar si un programa cumple con las expectativas. Esto significa que Move Prover puede inferir el comportamiento del programa según la información conocida, asegurando que coincida con el comportamiento esperado. Esto ayuda a garantizar la corrección del programa y reduce la carga de trabajo de las pruebas manuales.
La arquitectura general de Move Prover es la siguiente:
Primero, Move Prover recibe archivos fuente de Move que contienen la especificación de entrada del programa )specification###. Move Parser extrae la especificación del código fuente. El compilador de Move compila el archivo fuente en bytecode, que junto con el sistema de especificaciones se convierte en el modelo de objeto del verificador (Prover Object Model).
El modelo se traduce al lenguaje intermedio Boogie. El código Boogie se pasa al sistema de verificación Boogie para realizar la "generación de condiciones de verificación". Las condiciones de verificación se pasan al solucionador Z3 (, un solucionador SMT desarrollado por Microsoft ).
Después de que VC se pase a Z3, el verificador comprueba si el código del programa de la fórmula SMT ( cumple con la especificación ) y si es insatisfacible. Si es así, se indica que la especificación es válida. De lo contrario, se genera un modelo que satisface las condiciones, se convierte de nuevo al formato Boogie y se emite un informe de diagnóstico. El informe de diagnóstico se restaura a errores a nivel de código fuente similares a los errores estándar de compiladores.
![Move安\u003c/info\u003e\u003c/coin\u003e\u003c/info\u003e\u003c/coin\u003e