Análise de segurança da linguagem Move: os revolucionários dos contratos inteligentes

A linguagem Move é uma linguagem de contratos inteligentes que pode ser compilada e executada em ambientes de blockchain que implementam o MoveVM. Como uma linguagem de contratos inteligentes de nova geração com segurança como uma das suas principais características, qual é o seu nível de segurança? Será capaz de evitar as ameaças de segurança comuns em máquinas virtuais de contratos como EVM e WASM? Este artigo explorará a questão da segurança da linguagem Move a partir de três perspectivas: características da linguagem, mecanismo de execução e ferramentas de verificação.

1. As características de segurança da linguagem Move

Ao contrário de muitas linguagens de programação existentes, a linguagem Move foi projetada para suportar interações seguras com código não confiável e também para suportar validação estática. Move abandonou a lógica não linear baseada em considerações de flexibilidade, não suporta despacho dinâmico e chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação alternativo.

Segue um exemplo de implementação de um ativo de token na linguagem Move:

mover módulo 0x1::TestCoin { use 0x1::signer;

const ADMIN: address = @0x1;

struct Coin tem chave, armazena { 
    valor: u64
}

struct Info tem chave {
    total_supply: u64  
}

módulo spec {
    invariante para todo addr: endereço onde existe<coin>(addr):
        global\u003cinfo\u003e(ADMIN).total_supply \u003e= global\u003ccoin\u003e(addr).value;
}

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(conta, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let coin = Coin { value: amount };
    let info = borrow_global_mut\u003cinfo\u003e(ADMIN);
    info.total_supply = info.total_supply + amount;
    moeda
}

public fun value(coin: &Coin): u64 {
    coin.value  
}

}

Este exemplo demonstra algumas características de segurança chave da linguagem Move:

1. Modularidade: cada módulo Move é composto por definições de tipos de estrutura e processos, podendo importar definições de tipos de outros módulos e chamar processos de outros módulos.

2. Tipo de recurso: Estruturas definidas como tipos de recurso através da chave has ou da marcação store podem ser armazenadas no armazenamento global persistente de chave-valor.

3. Armazenamento Global: permite que programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelos módulos que os possuem, mas que podem ser visualizados por outros módulos no livro público.

4. Controle de Acesso: O controle de acesso a operações críticas pode ser realizado através de afirmações e outros métodos.

5. Redução de invariantes: invariantes estáticos podem ser definidos para verificação formal.

6. Verificação de bytecode: inclui verificação de tipo de segurança e linearização, prevenindo operações ilegais sobre tipos de recursos.

Essas características garantem a segurança da linguagem Move em tempo de compilação.

2. Mecanismo de Funcionamento do Move

O programa Move é executado em uma máquina virtual, não pode acessar a memória do sistema e pode ser executado com segurança em ambientes não confiáveis.

O programa Move é executado na pilha, e o armazenamento global é dividido em memória ( pilha ) e variáveis globais ( pilha ). A memória não pode armazenar ponteiros que apontam para unidades de memória, e as variáveis globais são usadas para armazenar ponteiros que apontam para unidades de memória.

As instruções de bytecode do Move são executadas em um interpretador de pilha, o que facilita a implementação e o controle, sendo adequado para cenários de blockchain. Os valores do tipo de recurso só podem ser movidos de forma destrutiva.

O estado de execução do programa Move é um quádruplo ⟨C, M, G, S⟩, que inclui a pilha de chamadas, a memória, as variáveis globais e os operandos. Durante a execução, a chamada de função cria novos objetos de pilha de chamadas, enquanto as instruções de ramificação realizam saltos estáticos, evitando a despachagem dinâmica.

O MoveVM separa o armazenamento de dados e a pilha de chamadas, ao contrário do design do EVM. Embora esse design sacrifique a flexibilidade, ele melhora a segurança e a eficiência de execução.

3. Mover Prover

Move Prover é uma ferramenta de verificação formal baseada em raciocínio, que utiliza uma linguagem formal para descrever o comportamento do programa e algoritmos de raciocínio para verificar se o programa está de acordo com as expectativas.

A arquitetura do Move Prover é a seguinte:

1. Receber arquivos de origem Move como entrada, incluindo as especificações do programa.
2. O analisador extrai a especificação, o compilador compila o código-fonte em bytecode.
3. Converter para o modelo de objeto validador.
4. Traduzir para a linguagem intermediária Boogie.
5. O sistema de verificação Boogie gera condições de verificação.
6. O solucionador Z3 verifica se a fórmula SMT é insatisfatível.
7. Gerar relatório de diagnóstico e restaurar para erros a nível de código fonte.

Move usa a Move Specification Language para descrever especificações, que é um subconjunto da linguagem Move.

Move Prover é uma ferramenta útil que ajuda os desenvolvedores a garantir a correção dos contratos inteligentes e a reduzir o risco de transações.

Resumo

A linguagem Move é excepcional em design de segurança, considerando de forma abrangente características da linguagem, execução da máquina virtual e ferramentas de segurança. Ela sacrifica parte da flexibilidade, reforçando a verificação de tipos e lógica linear, facilitando a verificação de compilação e a validação formal. O MoveVM separa estado da lógica, alinhando-se melhor às necessidades de gestão de segurança de ativos em blockchain.

A linguagem Move pode efetivamente evitar vulnerabilidades comuns do EVM, como reentrância, estouro e injeção, mas problemas como autenticação, lógica e estouro de inteiros grandes ainda precisam da atenção dos desenvolvedores. Embora o Move considere a segurança de forma abrangente, ainda é recomendável utilizar serviços de auditoria de empresas de segurança terceirizadas e deixar a codificação e verificação de normas nas mãos de equipes de segurança profissionais.