Análise de segurança da linguagem Move: um mudador de regras para a linguagem de contratos inteligentes

A linguagem Move é uma linguagem de contratos inteligentes que pode ser compilada e executada em ambientes de blockchain que implementam o MoveVM. Desde o seu nascimento, considerou várias questões de segurança relacionadas a blockchains e contratos inteligentes, e se baseou em algumas das concepções de segurança da linguagem RUST. Como uma linguagem de contratos inteligentes da nova geração com segurança como principal característica, qual é a segurança do Move? Pode evitar ameaças de segurança comuns encontradas em máquinas virtuais de contratos como EVM e WASM em nível de linguagem ou por meio de mecanismos relacionados? Existem riscos de segurança específicos associados a ela?

Este artigo discutirá as questões de segurança da linguagem Move em três níveis: características da linguagem, mecanismos de operação e ferramentas de validação.

1. Características de segurança da linguagem Move

Ao contrário de muitas linguagens de programação existentes, o objetivo de design da linguagem Move é suportar a escrita de programas que possam interagir com código não confiável de forma segura, ao mesmo tempo em que suporta a verificação estática. Para alcançar esse objetivo, o Move abandonou a lógica não linear baseada em flexibilidade, não suporta despacho dinâmico e chamadas externas recursivas, mas introduz conceitos como genéricos, armazenamento global e recursos para implementar um padrão de programação alternativo. Por exemplo, o Move omite características de despacho dinâmico e chamadas recursivas, características que em outras linguagens de contratos inteligentes podem levar a vulnerabilidades de reentrada dispendiosas.

As características de segurança principais do Move incluem:

1. módulo (Module): Cada módulo Move é composto por uma série de definições de tipos de estrutura e processos. Os módulos podem importar definições de tipos declaradas em outros módulos e chamar processos.

2. Estruturas(: podem ser definidas como tipos de recursos, representando o que pode ser armazenado em um armazenamento global persistente de chave/valor.

3. 过程)Função(: definir a lógica de comportamento do módulo.

4. Armazenamento global: permite que os programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui.

5. Verificação de invariantes: é possível definir invariantes de verificação estática para garantir a conservação do estado do sistema.

6. Verificador de bytecode: impõe um sistema de tipos a nível de bytecode, prevenindo operações ilegais.

Move garante a segurança do código em tempo de compilação através dessas características. Em seguida, vamos analisar o mecanismo de funcionamento do Move e ver como o MoveVM garante a segurança em tempo de execução.

![Análise de segurança do Move: a mudança de jogo da linguagem de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(

2. Mecanismo de funcionamento do Move

Os programas Move são executados em máquinas virtuais e, durante a execução, não podem acessar a memória do sistema, o que permite que os Move sejam executados de forma segura em ambientes não confiáveis. Os programas Move são executados na pilha, e o armazenamento global é dividido em duas partes: memória ) heap ( e variáveis globais ) pilha (. A memória é um armazenamento de primeira ordem e não pode armazenar ponteiros que apontam para unidades de memória. As variáveis globais são usadas para armazenar ponteiros que apontam para unidades de memória, mas a maneira de indexação é diferente da memória.

As instruções de bytecode do Move são executadas em um interpretador baseado em pilha. A máquina virtual baseada em pilha é fácil de implementar e controlar, exige menos do ambiente de hardware e é adequada para cenários de blockchain. Em comparação com um interpretador baseado em registradores, um interpretador baseado em pilha é mais fácil de controlar e detectar a cópia e o movimento entre variáveis.

Durante a execução do programa Move, seu estado é representado pelo quádruplo ⟨C, M, G, S⟩, que inclui: a pilha de chamadas )C(, a memória )M(, as variáveis globais )G( e os operandos )S(. A pilha também mantém a tabela de funções ) do próprio módulo ( para resolver as instruções que contêm o corpo da função.

O MoveVM separa a lógica de processo de armazenamento de dados e a pilha de chamadas ), que é a maior diferença em relação ao EVM. No MoveVM, os recursos ( sob o endereço da conta de estado do usuário ) são armazenados de forma independente, e as chamadas de programa devem cumprir regras de força relacionadas a permissões e recursos. Embora isso sacrifique certa flexibilidade, ajuda a melhorar a segurança e a eficiência de execução (, resultando em um grande avanço na execução concorrente ).

3. Mover Prover

Move Prover é uma ferramenta de verificação formal baseada em raciocínio. Ela utiliza uma linguagem formal para descrever o comportamento do programa e usa algoritmos de raciocínio para verificar se o programa está em conformidade com as expectativas, ajudando os desenvolvedores a garantir a correção dos contratos inteligentes, reduzindo assim o risco de transações.

O Move Prover utiliza um algoritmo de verificação dedutiva para validar se o programa está em conformidade com as expectativas. Isso significa que o Move Prover pode inferir o comportamento do programa com base em informações conhecidas e garantir que ele corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa, reduzindo a carga de trabalho dos testes manuais.

O fluxo de trabalho do Move Prover é o seguinte:

1. Receber o arquivo fonte Move como entrada, o qual deve configurar a especificação de entrada do programa (specification).

2. O Parser Move extrai a especificação do código-fonte.

3. O compilador Move compila o arquivo fonte em bytecode, transformando-o juntamente com o sistema de especificações em um modelo de objeto de provador (Prover Object Model).

4. Traduzir o modelo para a linguagem intermediária Boogie.

5. O sistema de verificação Boogie realiza a "geração de condições de verificação"(verification condition generation).

6. Transmitir as condições de verificação para o solucionador Z3 (, o solucionador SMT desenvolvido pela Microsoft ).

7. O Z3 verifica se o código do programa SMT ( satisfaz a especificação ) ou se é insatisfazível.

8. Se não for satisfatório, indica que a norma é válida; caso contrário, gera um modelo que satisfaz as condições, converte de volta para o formato Boogie e publica o relatório de diagnóstico.

9. Restaurar o relatório de diagnóstico para erros a nível de código fonte.

Move utiliza a Move Specification Language para descrever sistemas de especificação. Esta linguagem é um subconjunto do Move, suportando a descrição estática do comportamento de correção do programa, sem afetar a produção. É possível escrever separadamente documentos de especificação dedicados, separando o código de negócio do código de verificação formal.

Move Prover é uma ferramenta útil que ajuda os desenvolvedores a garantir a correção dos contratos inteligentes. Ela usa uma linguagem formal para descrever o comportamento do programa e emprega algoritmos de raciocínio para verificar se o programa atende às expectativas. Isso ajuda a reduzir o risco de transações, permitindo que os desenvolvedores implantem contratos inteligentes em ambientes de produção com mais confiança.

4. Resumo

A linguagem Move é excepcional em termos de design de segurança, considerando de forma abrangente as características da linguagem, a execução da máquina virtual e as ferramentas de segurança. As características da linguagem sacrificam parte da flexibilidade, forçando a verificação de tipos e a lógica linear, facilitando a automação da verificação de compilação e a validação formal, além de garantir segurança verificável. O design do MoveVM separa estado e lógica, alinhando-se melhor às necessidades de gestão segura de ativos na blockchain.

Em termos de linguagem, o Move pode evitar efetivamente vulnerabilidades comuns no EVM, como reentrância, estouro, injeção de Call/DeleGateCall, entre outras. No entanto, problemas como autenticação, lógica de código e estouro de estruturas de inteiros grandes ainda requerem atenção dos desenvolvedores. O Move Prover pode não funcionar quando a compreensão geral é negligenciada.

Apesar de a linguagem Move considerar muitos aspectos de segurança para os programadores, não existe uma linguagem completamente segura, nem programas totalmente seguros. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem serviços de auditoria de empresas de segurança de terceiros e deleguem a elaboração e validação da parte de especificação do código a empresas de segurança de terceiros.