Análise da segurança da linguagem Move

Introdução

Move é uma linguagem de contratos inteligentes que pode ser compilada e executada em ambientes de blockchain que implementam o MoveVM. Desde o seu design inicial, considerou diversos problemas de segurança relacionados a blockchain e contratos inteligentes, e se inspirou em algumas ideias de design de segurança da linguagem RUST. Como uma nova geração de linguagem de contratos inteligentes com segurança como uma de suas principais características, qual é a segurança do Move? Será que pode evitar ameaças de segurança comuns das máquinas virtuais de contratos, como EVM e WASM, a nível de linguagem ou através de mecanismos relacionados? Existem problemas de segurança específicos do Move?

Este artigo irá explorar a questão da segurança da linguagem Move a partir de três níveis: características da linguagem, mecanismo de execução e ferramentas de verificação.

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

Escrever código sem falhas é difícil, mesmo após múltiplos testes, não há garantias totais. Ao interagir com código não confiável, escrever código que mantenha propriedades de segurança essenciais é ainda mais desafiador. Existem várias técnicas para impor segurança em tempo de execução, como sandboxing, isolamento de processos, bloqueios de objetos e outros padrões de programação; também é possível especificar segurança estática em tempo de compilação, como tipos estáticos obrigatórios ou verificações de assertivas.

Às vezes, também se pode recorrer a ferramentas de análise semântica e análise estática para garantir que o código esteja em conformidade com as regras de segurança, mesmo ao interagir com código não confiável, mantendo certas propriedades lógicas prováveis. Esses métodos parecem bons, pois podem evitar sobrecargas em tempo de execução e detectar problemas de segurança antecipadamente. No entanto, a segurança obtida por meio desses métodos nas linguagens de programação é extremamente limitada, principalmente por duas razões: primeiro, elas geralmente têm características linguísticas que são difíceis de analisar com ferramentas de análise estática, como despacho dinâmico, mutabilidade compartilhada e reflexão, que são lógicas não lineares, essas características violam as regras de invariantes de segurança, oferecendo aos atacantes uma ampla superfície de ataque. Em segundo lugar, a maioria das linguagens de programação é difícil de expandir para suportar ferramentas estáticas relacionadas à segurança ou linguagens de redução expressivas, embora essas duas expansões sejam importantes.

A linguagem Move foi projetada para suportar a interação segura com código não confiável e também para permitir a verificação estática. Ela possui essas características de segurança porque abandona toda lógica não linear baseada em considerações de flexibilidade, não suporta despacho dinâmico e também não suporta chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global e recursos para implementar alguns padrões de programação alternativos. Por exemplo, o 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 custosas.

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

• Modular: 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.

• Estruturas: podem definir estruturas de tipos de recurso, usadas para representar dados que podem ser armazenados no armazenamento global de chave/valor.

• Processo: definiu processos de inicialização, seguros e inseguros. Os processos podem ter restrições de controlo de acesso.

• Armazenamento Global: permite armazenar dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui.

• Verificação de invariantes: É possível definir invariantes para verificação estática, garantindo a integridade dos recursos no sistema.

• Validador de bytecode: aplica um sistema de tipos a nível de bytecode, evitando que recursos sejam criados, desempacotados ou referenciados de forma inadequada.

Essas características permitem que o Move ofereça uma forte garantia de segurança tanto em tempo de compilação quanto em tempo de execução.

2. Mecanismo de funcionamento do Move

O programa Move é executado em uma máquina virtual, o que impede o acesso direto à memória do sistema, garantindo que ele possa ser executado de forma segura em ambientes não confiáveis.

O Move utiliza um modelo de execução em pilha. O armazenamento global é dividido em duas partes: memória ( pilha ) e variáveis globais ( pilha ). A memória é um armazenamento de primeira ordem, 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, acessando através de endereços e tipos.

O Move utiliza um interpretador baseado em pilha para executar instruções de bytecode, uma abordagem que é fácil de implementar e controlar, com baixos requisitos de hardware, adequada para cenários de blockchain. Em comparação com um interpretador baseado em registradores, o interpretador baseado em pilha é mais fácil de controlar e detectar a cópia e o movimento entre variáveis.

O estado em tempo de execução do programa Move é um quádruplo ⟨C, M, G, S⟩, que inclui a pilha de chamadas (C), a memória (M), as variáveis globais (G) e a pilha de operandos (S). A pilha de chamadas contém informações de contexto da execução do processo e o número da instrução. Ao executar a instrução Call, um novo objeto de pilha de chamadas é criado, armazenando parâmetros e executando as instruções do novo contrato. Quando encontra uma instrução de ramificação, realiza um salto estático dentro do processo.

O MoveVM separa o armazenamento de dados e a pilha de chamadas, que é a sua principal diferença em relação ao EVM. No Move, 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 estar de acordo com as regras de permissão e recursos. Este design sacrifica certa flexibilidade, mas melhora a segurança e a eficiência da execução.

![Análise de Segurança do Move: O Mudador de Jogo 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 pode ajudar os desenvolvedores a garantir a correção dos contratos inteligentes, reduzindo o risco de transações. Ela utiliza uma linguagem formal para descrever o comportamento do programa e valida, através de algoritmos de raciocínio, se o programa está em conformidade com o esperado.

Move Prover utiliza algoritmos de verificação dedutiva para inferir o comportamento do programa com base nas informações conhecidas, garantindo que corresponda às expectativas. Isso ajuda a assegurar a correção do programa e a reduzir a carga de trabalho de testes manuais.

O fluxo de trabalho do Move Prover é o seguinte:

1. Receber o arquivo fonte Move como entrada, que contém a especificação do programa
2. O analisador extrai a gramática, o compilador compila o código-fonte em bytecode
3. Gerar modelo de objeto validador
4. Traduzir o modelo para a linguagem intermediária Boogie
5. O sistema de verificação Boogie gera condições de verificação
6. Passar as condições de verificação para o solucionador Z3 verificar
7. Gerar relatório de diagnóstico e converter em erro a nível de código-fonte

Move fornece a Move Specification Language para descrever especificações, que é um subconjunto da linguagem Move e suporta a descrição estática do comportamento de correção do programa. As especificações podem ser escritas independentemente do código de negócios.

Move Prover é uma ferramenta poderosa que pode ajudar os desenvolvedores a garantir a correção dos contratos inteligentes, reduzindo o risco de transações. Ele utiliza métodos formais para verificar se o programa atende às expectativas, aumentando a confiança dos desenvolvedores na implementação de contratos inteligentes.

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

Resumo

A linguagem Move considerou de forma abrangente a segurança, oferecendo fortes garantias desde as características da linguagem, a execução da máquina virtual até as ferramentas de segurança. Sacrificou certa flexibilidade, impondo verificação de tipo e lógica linear, o que favorece a automação da verificação de compilação e validação formal. O design do MoveVM separa o estado da lógica, alinhando-se melhor às necessidades de gestão de segurança de ativos em blockchain.

A linguagem Move pode evitar efetivamente vulnerabilidades comuns no EVM, como reentrância, estouro, injeção de Call/DelegateCall, entre outras. No entanto, problemas de autenticação, lógica de código e estouro de estruturas de inteiros grandes ainda exigem atenção adicional dos desenvolvedores. Embora o Move Prover seja poderoso, ele não pode evitar completamente descuidos no design geral.

Embora o Move tenha considerado muitos aspectos de segurança, não existem linguagens e programas totalmente seguros. Recomenda-se que os desenvolvedores de contratos inteligentes Move ainda utilizem os serviços de auditoria de empresas de segurança de terceiros e deixem a redação e a verificação de partes da norma a cargo de uma equipe de segurança profissional.

![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-f7cd11fef1c66709b219e1a1e8d2e4da.webp(