Análise da segurança da linguagem Move: o revolucionário no campo dos contratos inteligentes

A linguagem Move, como uma nova geração de contratos inteligentes, teve a segurança como um dos principais fatores de consideração desde o seu design inicial. 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 validação.

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

A linguagem Move implementa um padrão de programação seguro ao abrir mão de algumas características de flexibilidade, adotando conceitos como genéricos, armazenamento global e recursos. Suas principais características de segurança incluem:

• Design modular, cada módulo é composto por tipos de estrutura e definições de processo
• Estrutura de tipo de recurso, pode ser armazenada no armazenamento de chave-valor global
• Mecanismo de armazenamento global, permitindo que os módulos acessem de forma exclusiva os recursos que declararam.
• Invariante de redução, utilizado para verificar a conservação do estado do sistema de forma estática
• Verificador de bytecode, impõe segurança de tipo e lógica linear

O verificador de bytecode realiza as seguintes verificações:

1. Verificação de legalidade da estrutura
2. Detecção semântica da lógica do processo
3. Verificação de erros ao ligar

Através desses mecanismos, o Move consegue garantir uma alta segurança de código durante a compilação.

2. Mecanismo de funcionamento do Move

O programa Move é executado na máquina virtual e possui as seguintes características de segurança:

• Não é possível acessar a memória do sistema diretamente
• Executar na pilha, a memória global é dividida em duas partes: memória e variáveis globais.
• Executar instruções de bytecode usando um interpretador baseado em pilha
• O valor dos recursos só pode ser movido de forma destrutiva
• O estado é composto pela pilha de chamadas, memória, variáveis globais e operações.
• Chamada de processo sem dependências circulares, evitando problemas de reentrada
• Armazenamento de dados e pilha de chamadas separadas

Este design apresenta uma grande melhoria tanto em segurança como em eficiência de execução.

3. Mover Prover

Move Prover é uma ferramenta de verificação formal baseada em raciocínio, que pode:

• Usar uma linguagem formal para descrever o comportamento do programa
• Validar a correção do programa através de algoritmos de inferência
• Adotar algoritmos de verificação dedutiva
• Descrever as especificações de verificação usando a linguagem de especificação Move
• Gerar relatório de verificação, indicando problemas potenciais

Move Prover é uma ferramenta de assistência de auditoria automatizada muito útil que pode ajudar os desenvolvedores a aumentar a segurança dos contratos inteligentes.

Resumo

A linguagem Move considera amplamente a segurança em termos de características de linguagem, execução da máquina virtual e ferramentas de segurança. Ela pode evitar efetivamente vulnerabilidades comuns do EVM, como reentrância, estouro, entre outras. No entanto, ainda é necessário prestar atenção a questões de segurança relacionadas à autenticação e ao design lógico.

Embora o Move tenha muitas vantagens em termos de segurança, ainda é recomendável que os desenvolvedores utilizem serviços de auditoria de segurança de terceiros e que o código do protocolo seja escrito e verificado por uma equipe de segurança profissional, a fim de garantir ainda mais a segurança dos contratos inteligentes.