Análise da segurança da linguagem Move

A linguagem Move, como uma nova geração de linguagem de contratos inteligentes, considerou desde o início as questões de segurança relacionadas à blockchain e contratos inteligentes. Este artigo irá explorar a segurança da linguagem Move sob 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 abandonou a lógica não linear baseada em flexibilidade, não suporta dispatch dinâmico e chamadas externas recursivas, mas utiliza conceitos como generics, armazenamento global, recursos, entre outros, para implementar um modelo de programação alternativo. Esses designs ajudam a evitar vulnerabilidades de segurança como reentrâncias.

Os principais componentes da linguagem Move incluem:

• Módulo: composto por definições de tipos de estrutura e processos, pode importar definições de tipos de outros módulos e chamar processos de outros módulos.

• Estruturas: podem ser definidas como tipos de recursos, armazenados na loja de chave-valor global.

• Processo: definir as funções do módulo, podendo incluir processos de inicialização, seguros e inseguros.

O mecanismo de armazenamento global da linguagem Move permite que os módulos armazenem dados persistentes e tenham acesso exclusivo de leitura e escrita aos tipos de recursos que declaram. Este mecanismo ajuda a impor restrições de segurança.

Duas importantes características de verificação estática da linguagem Move:

1. Verificação de invariantes: definição da conservação do estado do sistema através de uma linguagem de especificação.

2. Validador de bytecode: execução forçada de tipos seguros e linearização, prevenindo operações ilegais.

2. Mecanismo de operação do Move

O programa Move é executado em uma máquina virtual, não podendo acessar diretamente a memória do sistema. A execução do programa é baseada em pilha, com o armazenamento global dividido em memória ( pilha ) e variáveis globais ( pilha ).

O estado de execução da Move VM é composto pela pilha de chamadas, memória, variáveis globais e operações. As suas características incluem:

• Salto estático, evitando a distribuição dinâmica
• Pilhas de chamada adjacentes, para evitar reentrada
• Separação de armazenamento de dados e pilha de chamadas

Este design melhora a segurança e a eficiência de execução.

3. Mover Prover

Move Prover é uma ferramenta de verificação formal que utiliza algoritmos de verificação dedutiva para validar se um programa está em conformidade com o esperado. Seu fluxo de trabalho:

1. Receber o arquivo fonte Move e as normas
2. Compilar para bytecode e modelo de objeto do validador
3. Converter para a linguagem intermediária Boogie
4. Gerar condições de verificação
5. Verificação com o solucionador Z3
6. Gerar relatório de diagnóstico

A Linguagem de Especificação de Movimento é usada para descrever as especificações do comportamento do programa, podendo ser escrita independentemente do código de negócios.

Resumo

A linguagem Move considera de forma abrangente as características da linguagem, a execução da máquina virtual e as ferramentas de segurança, podendo efetivamente evitar muitas vulnerabilidades comuns. No entanto, ainda se recomenda o uso de serviços de auditoria de segurança de terceiros, e que a escrita e validação de código em conformidade seja realizada por empresas de segurança.