Análise Profunda da Segurança da Linguagem Move: Características da Linguagem, Mecanismos de Execução e Auditoria Automatizada

Introdução

A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em ambientes de blockchain que implementam o MoveVM. Ela foi criada levando em consideração várias questões de segurança relacionadas a blockchain e contratos inteligentes, e se baseia em parte no design de segurança da linguagem RUST. Como uma linguagem de contratos inteligentes de nova geração, cuja principal característica é a segurança, qual é a segurança do Move? Ele pode evitar ameaças de segurança comuns que ocorrem em máquinas virtuais de contratos, como EVM e WASM, a nível de linguagem ou mecanismos relacionados? Existe alguma questão de segurança própria?

Este artigo abordará a questão da segurança da linguagem Move a partir de três aspectos: características da linguagem, mecanismo de funcionamento e ferramentas de verificação.

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

Escrever código correto é difícil, e mesmo após múltiplos testes, não há garantia de que o código esteja completamente livre de falhas. Ao interagir com código não confiável, torna-se ainda mais difícil escrever código que mantenha atributos de segurança essenciais. Existem várias técnicas que podem impor segurança em tempo de execução, como sandbox, isolamento de processos, bloqueios de objetos e outros padrões de programação; também é possível especificar segurança estática em tempo de compilação, como tipos estáticos obrigatórios ou verificações de asserção.

Às vezes, também se pode recorrer a ferramentas de análise semântica e análise estática para garantir que o código cumpra as regras de segurança, mesmo quando interage com código não confiável, mantendo certas especificações lógicas prováveis inalteradas.

Esses esquemas parecem bons, pois podem evitar sobrecargas em tempo de execução e detectar problemas de segurança antecipadamente. Mas, infelizmente, a segurança obtida por esses métodos em linguagens de programação é extremamente limitada, principalmente por dois motivos: primeiro, elas geralmente possuem características que não podem ser analisadas estaticamente, como dispatch dinâmico, mutabilidade compartilhada e lógica não linear, como reflexão, que violam as regras de invariantes de segurança, oferecendo uma ampla superfície de ataque para hackers. Em segundo lugar, a maioria das linguagens de programação é difícil de estender com ferramentas estáticas relacionadas à segurança ou com linguagens de especificação altamente expressivas. Embora essas duas extensões sejam importantes, podem ser definidas antecipadamente.

Ao contrário de muitas linguagens de programação existentes, a linguagem Move foi projetada desde o início para suportar a escrita de programas que interagem de forma segura com código não confiável, ao mesmo tempo que suporta validação estática. A Move possui essas características de segurança porque abandonou toda lógica não linear baseada em considerações de flexibilidade, não suporta despacho dinâmico e também não suporta chamadas externas recursivas, mas usa conceitos como genéricos, armazenamento global e recursos para implementar alguns padrões de programação alternativos. Por exemplo, a Move omite as características de agendamento dinâmico e chamadas recursivas, que em outras linguagens de contratos inteligentes resultam em vulnerabilidades de reentrada dispendiosas.

Para melhor compreender as características da linguagem Move, vamos ver um programa de exemplo:

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

const ADMIN: endereço = @0x1;

struct Coin tem chave, armazena {
    valor: u64
}

struct Info tem chave {
    total_supply: u64
}

módulo de especificação {
    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, 0);
    mover_para(conta, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin acquires Info {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Moeda { valor: quantia }
}

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

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

}

a) módulo(Module): Cada módulo Move é composto por uma série de definições de tipos de estrutura e processos. Os módulos podem importar definições de tipos e chamar processos declarados em outros módulos. O nome totalmente qualificado do módulo começa com o endereço da conta de 16 bytes que armazena o código do módulo. O endereço da conta serve como espaço de nomes para distinguir módulos com o mesmo nome.

b) Estruturas(: Este módulo define duas estruturas, Coin e Info. Coin representa os tokens alocados ao usuário, e Info registra o total de tokens. Ambas as estruturas são definidas como tipos de recurso, podendo ser armazenadas em um armazenamento global persistente de chave/valor.

c) processo)function(: o código define um processo de inicialização, um processo seguro e um processo inseguro. O processo de inicialização deve ser chamado antes de criar o Coin, para inicializar o valor total_supply do Info singleton como zero. signer é um tipo especial que representa um usuário validado pela lógica externa do Move. A asserção garante que apenas a conta de administrador designada pode chamar este processo. O processo de mint permite que o administrador crie novos tokens, também com controle de acesso. O processo value_mut aceita uma referência mutável do Coin e retorna uma referência mutável ao campo value.

A estrutura do contrato é semelhante a outras linguagens de contratos inteligentes, mas os tipos de recursos e o armazenamento global são mecanismos-chave para armazenamento e segurança de recursos na linguagem Move.

O armazenamento global permite que programas Move armazenem dados persistentes, que só podem ser lidos e escritos de forma programática pelo módulo que os possui, mas que estão armazenados em um livro-razão público, podendo ser visualizados pelos usuários de outros módulos. Cada chave no armazenamento global é composta por um nome de tipo totalmente qualificado e o endereço da conta que armazena o valor desse tipo. Embora o armazenamento global seja compartilhado entre todos os módulos, cada módulo tem acesso exclusivo de leitura e escrita às chaves que declara.

O módulo que declara o tipo de recurso pode: • Publicar valores no armazenamento global através do comando move_to • Remover o valor do armazenamento global através do comando move_from • Obter uma referência ao valor armazenado globalmente através da instrução borrow_global_mut

O módulo pode impor restrições ao armazenamento global que controla. Por exemplo, garantir que apenas o endereço da conta ADMIN possa possuir a estrutura do tipo Info, implementando um processo de inicialização que usa move_to no tipo Info e impõe a condição prévia de que move_to seja chamado no endereço ADMIN.

As seguintes são duas características de verificação estática que garantem a segurança do código deste módulo: redução de invariantes e validador de bytecode.

a) Verificação de invariantes ) Verificação de restrições (: A linha 10 do módulo indica a verificação estática do invariantes — a soma dos campos de valor de todos os objetos Coin no sistema deve ser igual ao campo total_value do objeto Info armazenado no endereço ADMIN. Invariante é um termo da verificação formal que representa a conservação do estado. Essa propriedade de conservação se aplica a todos os potenciais clientes do módulo.

b) Verificador de Bytecode: tipos de segurança e linearização são os principais domínios de verificação do verificador de bytecode. Embora outros módulos não possam acessar a unidade de armazenamento global controlada por 0x1::TestCoin::Coin, eles podem usar esse tipo em suas próprias declarações de processos e estruturas.

Move tem um verificador de bytecode ) que impõe um sistema de tipos ao nível do bytecode (, permitindo que o proprietário do módulo previna resultados indesejados. Apenas os módulos que declaram o tipo de estrutura Coin podem: • Criar um valor do tipo Coin • "Desempacotar" o valor do tipo Coin nos seus campos componentes • Obter uma referência ao campo Coin através de um empréstimo mutável ou imutável ao estilo rust

O validador também força a estrutura a ser linear por padrão, para garantir que a cópia e a destruição sejam prevenidas linearmente fora do módulo que declara a estrutura. Além disso, o validador também realizará verificações obrigatórias em alguns tipos de problemas comuns de memória.

O processo de detecção é principalmente dividido em três categorias:

1. Verificação de validade de estrutura: garantir a integridade do bytecode, detectar referências ilegais de erro, entidades de recursos duplicadas e assinaturas de tipo ilegais, etc.
2. Detecção semântica da lógica do processo: inclui erros de tipo de parâmetro, índices de loop, índices nulos e definição de variáveis duplicadas, entre outros.
3. Erro ao conectar, chamada interna ilegal do processo, ou fluxo de declaração e definição de ligação não correspondem.

O validador primeiro cria o CFG) do grafo de controle de fluxo(, em seguida, verifica o alcance de acesso do chamador na pilha, garantindo que o chamador do contrato não possa acessar o espaço da pilha do chamador. Ao mesmo tempo, para verificar os tipos, cada pilha de Value mantém uma pilha de Type correspondente.

A seguir estão as verificações de recursos e de referências. A verificação de recursos analisa principalmente restrições como não duplicar, não ser destruído e ter uma propriedade obrigatória. A verificação de referências combina análise dinâmica e estática, utilizando um mecanismo de verificação de empréstimos semelhante ao sistema de tipos Rust.

Por fim, é necessário verificar novamente se os objetos de link e as declarações correspondem, bem como o controle de acesso do processo.

![Análise de Segurança do Move: O Mudador de Jogo da Linguagem de Contratos Inteligentes])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(

) 2. Mecanismo de funcionamento do Move

Primeiro, o programa Move é executado em uma máquina virtual, e durante a execução não pode acessar a memória do sistema. Isso permite que o Move seja executado de forma segura em um ambiente não confiável, sem ser comprometido ou abusado.

Em segundo lugar, o programa Move é executado na pilha. O armazenamento global é dividido em memória ### pilha ( e variáveis globais ) pilha (. A memória é um armazenamento de primeira ordem, cujas unidades não podem armazenar ponteiros que apontam para unidades de memória. As variáveis globais são usadas para armazenar ponteiros que apontam para unidades de memória, mas a maneira de indexação é diferente. Ao acessar variáveis globais, o código fornece o endereço e o tipo vinculado a esse endereço. Essa divisão simplifica a operação, tornando a semântica da linguagem Move mais fácil de formalizar.

Instruções de bytecode Move são executadas em um interpretador baseado em pilha. A máquina virtual baseada em pilha é fácil de implementar e controlar, exige menos do ambiente de hardware e é adequada para cenários de blockchain. Em comparação com um interpretador baseado em registradores, o interpretador baseado em pilha torna mais fácil controlar e detectar operações de cópia e movimentação entre variáveis.

Em Move, o valor definido como recurso só pode ser movido de forma destrutiva, tornando inválido o local de armazenamento que salvou esse valor anteriormente, mas certos valores, como inteiros, podem ser copiados.

Quando o programa Move é executado na pilha, seu estado é representado por um quádruplo ⟨C, M, G, S⟩, composto pela pilha de chamadas )C(, memória )M(, variáveis globais )G( e operandos )S(. A pilha também mantém uma tabela de funções ) para o próprio módulo ( para resolver as instruções que contêm o corpo da função.

A pilha de chamadas contém todas as informações de contexto e números de instrução da execução do processo. Ao executar a instrução Call, um novo objeto de pilha de chamadas é criado, os parâmetros da chamada são armazenados na memória e nas variáveis globais, e então o interpretador executa as instruções do novo contrato. Ao encontrar uma instrução de ramificação, ocorre um salto estático dentro deste processo. A dependência de processos dentro do módulo é acíclica, e como o módulo não possui atribuição dinâmica, isso reforça a imutabilidade das chamadas de função durante a execução: o quadro de chamada do processo deve ser adjacente, evitando a possibilidade de reentrada. A chamada return finaliza a chamada, e o valor de retorno é colocado no topo da pilha.

O estudo do código do MoveVM revela que o MoveVM separa a lógica do processo de armazenamento de dados e da pilha de chamadas ), o que é a maior diferença em relação ao EVM. No EVM, a implementação do token ERC20 requer que toda a lógica esteja escrita em um único contrato e registre o estado de cada usuário, enquanto no MoveVM, o estado do usuário ( é armazenado de forma independente nos recursos ) sob o endereço da conta, e as chamadas de programa devem estar em conformidade com as regras de autorização e as regras obrigatórias sobre recursos. Embora isso sacrifique certa flexibilidade, contribui para a segurança e a eficiência de execução (, resultando em um grande aumento na execução concorrente ).

( 3. Mover Prover

Por fim, vamos conhecer a ferramenta de auditoria automática auxiliar Move prover fornecida pelo Move.

Move Prover é uma ferramenta de verificação formal baseada em raciocínio. Ela usa uma linguagem formal para descrever o comportamento do programa e utiliza algoritmos de raciocínio para validar se o programa atende às expectativas, ajudando os desenvolvedores a garantir a correção dos contratos inteligentes e a reduzir o risco de transações. Em suma, a verificação formal é o método matemático para provar que um sistema está livre de bugs.

Atualmente, os algoritmos de verificação automática de software mais utilizados são baseados em resolutores de teoria da satisfação, )SMT solver(. O SMT solver é, na verdade, um resolutor de fórmulas. Os algoritmos de verificação de software de nível superior dividem os objetivos de verificação em fórmulas, que são entregues ao SMT solver para resolução, com base nos resultados para uma análise adicional, e, finalmente, relatam se os objetivos de verificação são válidos ou se uma contraexemplo é encontrado.

O algoritmo de verificação básica é a verificação dedutiva )deductive verification(, e existem outros algoritmos de verificação, como a verificação de modelo limitado, o método k-indutivo, a abstração de predicados e a abstração de caminhos, entre outros.

O Move Prover utiliza um algoritmo de verificação dedutiva para validar se o programa está de acordo com o esperado. Isso significa que o Move Prover pode inferir o comportamento do programa com base em informações conhecidas, garantindo que corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa e a reduzir o trabalho manual de testes.

A arquitetura geral do Move Prover é a seguinte:

Primeiro, o Move Prover recebe arquivos de origem Move contendo a especificação de entrada do programa )specification###. O Move Parser extrai a especificação do código-fonte. O compilador Move compila o arquivo de origem em bytecode, que é convertido em um modelo de objeto de provador (Prover Object Model) junto com o sistema de especificação.

O modelo é traduzido para a linguagem intermediária Boogie. O código Boogie é passado para o sistema de verificação Boogie para "geração de condições de verificação". As condições de verificação são passadas para o solucionador Z3 (, um solucionador SMT desenvolvido pela Microsoft ).

Após a entrada do VC no Z3, o verificador verifica se o código do programa da fórmula SMT ( atende à especificação ) ou se é insatisfazível. Se sim, isso indica que a especificação é válida. Caso contrário, um modelo que satisfaz as condições é gerado, convertido de volta para o formato Boogie e um relatório de diagnóstico é emitido. O relatório de diagnóstico é restaurado para erros de nível de código-fonte semelhantes aos erros padrão do compilador.

![Move安\u003c/info\u003e\u003c/coin\u003e\u003c/info\u003e\u003c/coin\u003e