Análise da segurança da linguagem Move

A linguagem Move, como uma nova geração de linguagens de contratos inteligentes, considerou plenamente as questões de segurança da blockchain e dos contratos inteligentes desde o seu design inicial. Este artigo analisará a segurança da linguagem Move a partir de 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 principais características de segurança:

• Abandonou a atribuição dinâmica, chamadas externas recursivas e outras lógicas não lineares, evitando vulnerabilidades como a reentrada.
• Utilizar tipos de recursos e mecanismos de armazenamento global para implementar a gestão segura de armazenamento e recursos
• Através da redução de invariantes e do verificador de bytecode, realizar uma verificação de segurança dupla durante a compilação.

Abaixo está um exemplo simples de contrato Move:

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

const ADMIN: endereço = @0x1;

struct Coin tem chave {
    valor: u64
}

struct Info tem chave {
    total_supply: u64  
}

invariável para todo addr: endereço onde existe<coin>(addr):
    global\u003cinfo\u003e(ADMIN).total_supply \u003e= global\u003ccoin\u003e(addr).value;

fun público inicializar(conta: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    mover_para(conta, Info { total_supply: 0 });
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let supply = borrow_global_mut<info>(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    Moeda { valor: quantia }
}

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

}

Move garante a segurança do código através da redução de invariantes e do verificador de bytecode:

1. Invariante de soma: utilizado para verificar se a soma dos valores de todos os objetos Coin no sistema deve ser igual ao total_supply em Info.

2. Verificador de bytecode: verificação de tipo obrigatória e lógica linear, para prevenir a criação, cópia ou destruição ilegal de recursos.

2. Mecanismo de funcionamento do Move

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

• Não é possível acessar a memória do sistema em tempo de execução, garantindo uma execução segura em ambientes não confiáveis.
• Utiliza um interpretador em pilha para executar instruções de bytecode, fácil de implementar e controlar
• Separar o armazenamento de dados da pilha de chamadas, aumentando a segurança e a eficiência de execução
• Os recursos só podem ser movidos de forma destrutiva, não podem ser copiados

O estado de execução do programa Move é composto por um quádruplo ⟨C, M, G, S⟩:

• C: Pilha de Chamadas
• M: memória ( pilha )
• G: variável global ( pilha )
• S: Operando

Este design separa o estado do usuário da lógica do programa, melhorando a segurança e a eficiência da execução concorrente.

3. Mover Prover

Move Prover é uma ferramenta de verificação formal, utilizada para garantir a correção dos contratos inteligentes. O seu fluxo de trabalho é o seguinte:

1. Receber o arquivo de origem Move e as especificações como entrada
2. Extrair a norma e compilar em bytecode
3. Converter para o modelo de objeto do validador
4. Traduzir para a linguagem intermediária Boogie
5. Gerar condições de verificação
6. Usar o solucionador Z3 para verificar a fórmula
7. Gerar relatório de diagnóstico

Move Prover usa a Move Specification Language para descrever as especificações de programas. Esta linguagem é um subconjunto do Move, podendo ser escrita independentemente do código de negócios.

Resumo

A linguagem Move considerou amplamente a segurança em termos de características da linguagem, execução da máquina virtual e ferramentas de segurança. Pode evitar eficazmente vulnerabilidades comuns como reentrada e estouro, mas ainda é necessário prestar atenção a questões de autenticação e lógica. Recomenda-se que os desenvolvedores utilizem serviços de auditoria de terceiros e que a redação das especificações seja deixada para empresas de segurança, a fim de aumentar ainda mais a segurança dos contratos.