Análise de segurança da linguagem Move: inovador no campo dos contratos inteligentes

A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em ambientes de blockchain que suportam MoveVM. Seu design considera várias questões de segurança relacionadas a blockchain e contratos inteligentes, e se inspira em parte nos princípios de design de segurança da linguagem Rust. Como uma nova geração de linguagem de contratos inteligentes com segurança como característica central, qual é a segurança da Move? Ela pode evitar ameaças de segurança comuns associadas a máquinas virtuais de contrato, como EVM e WASM, a nível de linguagem ou através de mecanismos relacionados? A Move apresenta alguma vulnerabilidade de segurança única?

Este artigo discutirá a questão da segurança da linguagem Move a partir de três áreas: características da linguagem, mecanismo de funcionamento e ferramentas de verificação.

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

Ao contrário de muitas linguagens de programação existentes, a linguagem Move tem como objetivo projetar programas que possam interagir de forma segura com código não confiável, ao mesmo tempo que suporta verificação estática. Move abandona a lógica não linear baseada na 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, Move omite as características de despacho dinâmico e chamadas recursivas, que em outras linguagens de contratos inteligentes podem levar a vulnerabilidades de reentrada de alto custo.

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

1. Módulo: 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. Processo: definir a funcionalidade e a lógica do módulo.

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

5. Verificação de invariantes: pode-se definir invariantes de verificação estática, garantindo a conservação do estado do sistema.

6. Verificador de bytecode: aplica o sistema de tipos em nível de bytecode, impedindo operações ilegais.

Através dessas características de segurança, o Move oferece um ambiente de programação mais seguro e confiável para o desenvolvimento de contratos inteligentes.

2. Mecanismo de funcionamento do Move

O programa Move é executado em uma máquina virtual e não pode acessar a memória do sistema durante a execução, o que permite que o Move funcione de forma segura em ambientes não confiáveis.

O programa Move é executado na pilha, e o armazenamento global é dividido em memória ( heap ) e variáveis globais ( pilha ). A memória é um armazenamento de primeira ordem, que não pode armazenar ponteiros para unidades de memória. As variáveis globais são usadas para armazenar ponteiros para unidades de memória, mas o método de indexação é diferente do da memória.

As instruções de bytecode do Move são executadas em um interpretador baseado em pilha. Comparado ao interpretador baseado em registradores, o interpretador baseado em pilha é mais fácil de controlar e detectar operações de cópia e movimentação entre variáveis.

O estado em execução do programa Move é uma quádrupla ⟨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 uma tabela de funções para resolver as instruções que contêm o corpo da função.

O MoveVM separa o armazenamento de dados e a pilha de chamadas de lógica de processo (, que é a principal diferença em relação ao EVM. 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 obrigatórias relacionadas a permissões e recursos. Embora esse design sacrifique certa flexibilidade, ele proporciona um aumento significativo na segurança e na eficiência de execução.

![Análise de segurança do Move: o Game Changer da linguagem de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. Mover Prover

Move Prover é uma ferramenta de verificação formal baseada em raciocínio, que usa uma linguagem formal para descrever o comportamento do programa e um algoritmo de raciocínio para verificar se o programa está de acordo com o esperado. Ela pode ajudar os desenvolvedores a garantir a correção dos contratos inteligentes e a reduzir o risco de transações.

O Move Prover utiliza algoritmos de verificação dedutiva para inferir o comportamento do programa com base em informações conhecidas, garantindo que corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa e a reduzir a carga de trabalho dos testes manuais.

O fluxo de trabalho do Move Prover é o seguinte:

1. Receber o arquivo fonte Move como entrada, que contém as especificações de entrada do programa.

2. A extração de normas do código-fonte pelo Move Parser.

3. O compilador Move compila o arquivo fonte em bytecode, convertendo-o juntamente com o sistema de especificações em um modelo de objeto de validador.

4. O modelo de objeto é traduzido para a linguagem intermediária Boogie.

5. O sistema de verificação Boogie realiza a "geração de condições de verificação" para a entrada.

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

7. Z3 verifica se a fórmula SMT é insatisfatível. Se for, indica que a especificação é válida; caso contrário, gera um modelo que satisfaz as condições.

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

Move utiliza a Move Specification Language para descrever especificações do sistema, que é um subconjunto da linguagem Move, suportando a descrição estática do comportamento de correção do programa, sem impactar a produção. As especificações podem ser escritas de forma independente, facilitando a separação do código de negócios e do código de verificação formal.

Move Prover é uma ferramenta poderosa que ajuda os desenvolvedores a garantir a correção dos contratos inteligentes, reduzindo o risco de transações e aumentando a confiança na implementação de contratos inteligentes em ambientes de produção.

![Análise de segurança do Move: O Game Changer da linguagem de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

4. Resumo

A linguagem Move é excepcional em termos de design de segurança, considerando de forma abrangente desde as características da linguagem, a execução da máquina virtual até o nível das ferramentas de segurança. As características da linguagem sacrificam parte da flexibilidade, com verificação de tipos obrigatória e lógica linear, o que é benéfico para a automação e verificabilidade da verificação de compilação e validação formal. O design da MoveVM separa o estado da lógica, alinhando-se melhor às necessidades de gestão de segurança de ativos em blockchain.

Em termos de linguagem, o Move pode evitar eficazmente vulnerabilidades comuns do 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 números inteiros grandes ainda precisam ser tratados com cautela pelos desenvolvedores. Embora o Move Prover seja poderoso, pode não ter efeito em caso de negligência no design geral.

Apesar de a linguagem Move oferecer várias garantias de segurança aos programadores, não existe uma linguagem ou programa completamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move continuem a utilizar serviços de auditoria de empresas de segurança de terceiros e deixem a redação e verificação da parte de especificação do código a cargo de uma equipe de segurança profissional, para aumentar ainda mais a segurança dos contratos.

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