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 várias questões de segurança em seu design. Este artigo analisará 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 possui as seguintes características de segurança:

• Abandonou a lógica não linear, como a alocação dinâmica e chamadas externas recursivas, evitando vulnerabilidades como a reentrada.
• Implementar padrões de programação seguros utilizando conceitos como generics, armazenamento global, recursos, entre outros.
• Design modular, cada módulo é composto por tipos de estrutura e definições de processo.
• A estrutura pode ser definida como um tipo de recurso, armazenado no armazenamento global de chave-valor.
• O armazenamento global permite a persistência de dados, que só podem ser acessados pelos módulos que os possuem.
• Utilizar a redução de invariantes e o verificador de bytecode para verificações estáticas

O verificador de bytecode realiza principalmente:

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

Através desses mecanismos, a linguagem Move pode garantir a segurança do código durante a compilação.

2. Mecanismo de funcionamento do Move

O programa Move é executado em uma máquina virtual, com principais características incluindo:

• Não é possível acessar a memória do sistema, pode ser executado com segurança em ambientes não confiáveis
• Executar na pilha, a memória global é dividida em memória ( pilha ) e variáveis globais ( pilha )
• Executar instruções de bytecode usando um interpretador baseado em pilha
• O valor dos recursos só pode ser movido de forma destrutiva, não pode ser copiado
• O estado do programa é composto pela pilha de chamadas, memória, variáveis globais e um array de operações.
• A pilha de chamadas contém o contexto de execução, suportando saltos estáticos
• Armazenamento de dados e pilha de chamadas separados, aumentando a segurança e a eficiência da execução

3. Mover Prover

Move Prover é uma ferramenta de verificação formal que pode realizar auditoria automatizada:

• Usar um algoritmo de verificação dedutiva para validar a correção do programa
• Receber o arquivo de origem Move e as especificações como entrada
• Converter o código para a linguagem intermediária Boogie
• Usar o solucionador Z3 SMT para verificar se a especificação é válida
• Suporte para a especificação da linguagem Move Specification Language
• Pode escrever documentos de especificação de forma independente, sem afetar o código de negócios

Move Prover pode ajudar os desenvolvedores a garantir a correção dos contratos inteligentes, reduzindo o risco de transações.

Resumo

A linguagem Move considera amplamente a segurança, incluindo características da linguagem, execução da máquina virtual e ferramentas de segurança. Ela pode efetivamente evitar vulnerabilidades comuns como reentrância e estouro, mas ainda é necessário prestar atenção a problemas como autenticação e lógica. Recomenda-se utilizar serviços de auditoria de empresas de segurança terceirizadas e que profissionais escrevam código de especificação de validação.