Análise de segurança da linguagem Move: o revolucionário da nova geração de contratos inteligentes

A linguagem Move, como uma nova linguagem de contratos inteligentes, considerou plenamente as questões de segurança da blockchain e dos contratos inteligentes desde o seu design inicial, e se inspirou em alguns princípios de design de segurança da linguagem Rust. Este artigo irá explorar a segurança da linguagem Move a partir de três aspectos: características da linguagem, mecanismo de execução e ferramentas de verificação.

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

A linguagem Move foi projetada para abrir mão de muitas lógicas não lineares baseadas em flexibilidade, não suportando chamadas externas dinâmicas e recursivas, mas introduzindo conceitos como genéricos, armazenamento global, recursos, entre outros, para implementar um modo de programação alternativo. Essas características ajudam a evitar vulnerabilidades comuns em outras linguagens de contratos inteligentes, como reentrância.

Os principais componentes da linguagem Move incluem:

• Módulo (: composto por uma série de tipos de estrutura e definições de processo
• Estruturas )Structs(: podem ser definidas como tipos de recursos, armazenados em um armazenamento chave/valor global persistente.
• 过程)function(: definir as funcionalidades específicas do contrato

Os dois conceitos importantes da linguagem Move são o tipo de recurso e o armazenamento global. O armazenamento global permite que programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui, mas que estão armazenados em um livro-razão público para visualização. O tipo de recurso garante o acesso exclusivo ao armazenamento global.

A linguagem Move garante a segurança do código em tempo de compilação através de duas mecânicas: verificação de invariantes e um validador de bytecode.

• Verificação de invariantes: a conservação do estado do sistema definida através de uma linguagem de especificação.
• Verificador de bytecode: realiza verificação de tipo seguro e linearização, incluindo verificação de validade de estruturas, detecção semântica de lógica de processo e verificação de erros em tempo de ligação.

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

2. Mecanismo de operação 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 garante a execução segura em ambientes não confiáveis.

O programa Move é executado na pilha, e seu estado é composto pela pilha de chamadas, memória, variáveis globais e operações. As instruções em bytecode do Move são executadas em um interpretador baseado em pilha, o que facilita a cópia e o controle de movimentação entre variáveis.

O Move VM separa o armazenamento de dados e a pilha de chamadas, o que é muito diferente do EVM. O estado do usuário é armazenado de forma independente, e as chamadas de programa devem cumprir regras de permissão e recursos, aumentando a segurança e a eficiência de execução, sacrificando uma certa flexibilidade.

![Análise de segurança do Move: um divisor de águas na 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 fornecida pela linguagem Move, que utiliza algoritmos de verificação dedutiva para validar se o programa está de acordo com as expectativas. O fluxo de trabalho é o seguinte:

1. Receber o arquivo fonte Move e as especificações como entrada
2. Extrair especificações e compilar o arquivo fonte em bytecode
3. Converter para o modelo de objeto validador
4. Traduzir para a linguagem intermediária Boogie
5. Gerar condições de verificação
6. Use o solucionador Z3 para verificar a satisfatibilidade da fórmula
7. Gerar relatório de diagnóstico

Move Prover utiliza a Move Specification Language para descrever sistemas de especificação, sendo um subconjunto da linguagem Move.

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

Resumo

A linguagem Move considera amplamente a segurança em termos de características da linguagem, execução da máquina virtual e ferramentas de segurança. Ela pode evitar efetivamente vulnerabilidades comuns como reentrância, estouro e injeção, mas ainda não consegue evitar completamente problemas de autenticação e lógica. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem serviços de auditoria de segurança de terceiros e contratem a redação de código de especificação de validaçã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-f7cd11fef1c66709b219e1a1e8d2e4da.webp(