Análise da segurança da linguagem Move

A linguagem Move, como uma nova geração de linguagens de contratos inteligentes, tem a segurança como sua principal característica. Este artigo analisa a segurança da linguagem Move em três níveis: características da linguagem, mecanismo de execução e ferramentas de validação.

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

A linguagem Move foi projetada tendo em conta a segurança de blockchain e contratos inteligentes, referindo-se ao design de segurança da linguagem Rust. Ao contrário de muitas linguagens de programação existentes, o Move abandona a lógica não linear baseada na flexibilidade, não suporta despachos dinâmicos e chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação alternativo.

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

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

• Estruturas (Structs): podem ser definidas como tipos de recurso, armazenados em armazenamento global de chave/valor.

• Processo (Função ): define a inicialização, processos seguros e processos inseguros.

• 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 conservação do estado do sistema.

• Verificador de bytecode: aplica um sistema de tipos a nível de bytecode, prevenindo operações ilegais.

2. Mecanismo de funcionamento do Move

O programa Move é executado em uma máquina virtual e não pode acessar diretamente a memória do sistema. O programa é executado na pilha, e o armazenamento global é dividido em memória (, heap ) e variáveis globais (, pilha ).

As instruções de bytecode do Move são executadas em um interpretador baseado em pilha. O estado do programa é composto pela pilha de chamadas, memória, variáveis globais e operações. Os valores de recursos só podem ser movidos de forma destrutiva, certos valores (, como inteiros ), podem ser copiados.

MoveVM separa o armazenamento de dados da pilha de chamadas, ao contrário do EVM. Este design traz grandes melhorias em segurança e eficiência de execução, mas sacrifica um certo grau de flexibilidade.

3. Mover Prover

Move Prover é uma ferramenta de verificação formal que utiliza algoritmos de verificação dedutiva para validar se o programa está de acordo com as expectativas. O seu fluxo de trabalho é o seguinte:

1. Receber o arquivo fonte Move e as especificações como entrada
2. Extração de especificações, compilar arquivos de origem para bytecode
3. Converter para o modelo de objeto validador
4. Traduza para a língua intermediária Boogie
5. Gerar condições de verificação
6. Usar o resolvedor Z3 para verificar fórmulas SMT
7. Gerar relatório de diagnóstico

Move Specification Language é usado para descrever especificações, sendo um subconjunto da linguagem Move. É possível escrever especificações de forma independente, sem afetar o código de produção.

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é as ferramentas de segurança. Ela pode evitar de forma eficaz vulnerabilidades comuns no EVM, como reentrância e estouro, mas ainda é necessário ter atenção a problemas como autenticação e lógica.

Embora o Move tenha grandes vantagens em termos de segurança, não existe uma linguagem ou programa completamente seguro. Recomenda-se que os desenvolvedores ainda utilizem auditorias de segurança de terceiros e que o código normativo seja escrito e verificado por uma equipe de segurança profissional.