Análise abrangente da segurança da linguagem Move: características, mecanismos e ferramentas de verificação

robot
Geração do resumo em andamento

Análise da segurança da linguagem Move

Introdução

Move é uma linguagem de contrato inteligente que pode ser executada em um ambiente de blockchain que implemente o MoveVM. Desde o seu nascimento, considerou vários problemas de segurança relacionados a blockchain e contratos inteligentes, e se inspirou em algumas das concepções de segurança da linguagem RUST. Como uma linguagem de contrato inteligente de nova geração com segurança como uma das suas principais características, qual é a segurança do Move? Pode evitar ameaças de segurança comuns em máquinas virtuais de contratos, como EVM e WASM, a nível de linguagem ou através de mecanismos relacionados? Existe alguma vulnerabilidade de segurança única associada a ela?

Este artigo irá explorar a questão da segurança da linguagem Move a partir de três níveis: características linguísticas, mecanismos de execução e ferramentas de validação.

Análise de segurança do Move: O divisor de águas da linguagem de contratos inteligentes

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

Ao contrário de muitas linguagens de programação existentes, o Move foi projetado para suportar interações seguras com códigos não confiáveis e também para suportar validação estática. O Move possui essas características de segurança porque abandona a lógica não linear baseada em considerações de flexibilidade, não suporta despachos dinâmicos e também não suporta chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global, recursos, entre outros, para implementar padrões de programação alternativos. Por exemplo, o Move omite características de despacho dinâmico e chamadas recursivas que poderiam levar a vulnerabilidades de reentrada.

As principais características de segurança do Move incluem:

  1. Módulo(Module): Cada módulo Move é composto por uma série de definições de tipos de estrutura e processos. O módulo pode importar definições de tipos declaradas em outros módulos e chamar seus processos.

  2. Estruturas(: pode ser definida como um tipo de recurso, representando algo que pode ser armazenado em um armazenamento persistente de chave/valor global.

  3. processo ) função (: definir a funcionalidade específica do módulo.

  4. Armazenamento global: permite que os programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui.

  5. Verificação de invariantes: invariantes estáticos definíveis que garantem a integridade dos recursos no sistema.

  6. Verificador de bytecode: valida tipos de segurança e linearização, evitando que valores sensíveis sejam criados, modificados ou destruídos ilegalmente.

![Análise de segurança do Move: O Game Changer da linguagem de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

2. Mecanismo de funcionamento do Move

O programa Move é executado na máquina virtual e não pode acessar diretamente a memória do sistema. O programa é executado na pilha, e o armazenamento global é dividido em duas partes: memória ) heap ( e variáveis globais ) stack (.

As instruções de bytecode do Move são executadas em um interpretador baseado em pilha, uma abordagem que é fácil de implementar e controlar, com requisitos de hardware relativamente baixos, adequada para cenários de blockchain. Ao mesmo tempo, em comparação com um interpretador baseado em registradores, o interpretador baseado em pilha é mais fácil de controlar e detectar a cópia e o movimento entre variáveis.

Durante a execução, o estado do programa Move é composto pela pilha de chamadas, memória, variáveis globais e operações. A pilha de chamadas contém todas as informações de contexto da execução do processo. Ao executar a instrução Call, um novo objeto da pilha de chamadas é criado. Ao encontrar uma instrução de ramificação, ocorre um salto estático dentro do processo.

Ao contrário do EVM, o MoveVM separa o armazenamento de dados e a pilha de chamadas, sendo mais adequado para as necessidades de gestão de segurança de ativos na blockchain. Este design proporciona um grande aumento na segurança e eficiência de execução.

![Análise de segurança do Move: O Game Changer da linguagem de contratos inteligentes])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

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 o esperado. Pode ajudar os desenvolvedores a garantir a correção de contratos inteligentes, reduzindo o risco de transações.

Move Prover utiliza um algoritmo de verificação dedutiva para inferir o comportamento do programa com base nas informações disponíveis, garantindo que corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa e a reduzir a carga de trabalho dos testes manuais.

O fluxo de trabalho do Move Prover é o seguinte:

  1. Receber o arquivo fonte Move como entrada
  2. Extrair a especificação e compilar em bytecode
  3. Converter para o modelo de objeto validador
  4. Traduzir para a linguagem intermediária Boogie
  5. Gerar condições de verificação
  6. Usar o solucionador Z3 para verificar fórmulas SMT
  7. Gerar relatório de diagnóstico e restaurar para erros a nível de código-fonte

A Move Specification Language é usada para descrever sistemas de especificação, sendo um subconjunto da linguagem Move, que suporta a descrição estática do comportamento de correção dos programas.

No geral, o Move Prover é uma ferramenta muito útil que pode ajudar os desenvolvedores a garantir a correção dos contratos inteligentes, reduzir os riscos de transação e aumentar a confiança na implementação de contratos inteligentes.

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

4. Resumo

A linguagem Move é excelente em design de segurança, considerando de forma abrangente as características da linguagem, a execução da máquina virtual e a camada de ferramentas de segurança. Ela sacrifica parte da flexibilidade, impondo verificação de tipos e lógica linear, facilitando a verificação de compilação e validação formal. O MoveVM separa estado de lógica, sendo mais adequado às necessidades de gestão de segurança de ativos em blockchain.

A linguagem Move pode evitar eficazmente vulnerabilidades comuns no EVM, como reentrância, estouro, injeção de Call/DeleGateCall, entre outras. No entanto, problemas como autenticação, lógica de código e estouro de estruturas de inteiros grandes ainda requerem atenção adicional por parte dos desenvolvedores. Embora o Move Prover ofereça verificação formal, não pode compensar falhas no design geral.

Apesar de a Move ter feito muitas considerações em termos de segurança, não existe uma linguagem ou programa completamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move continuem a utilizar os serviços de auditoria de empresas de segurança de terceiros e que a redação e verificação de partes das normas sejam deixadas a equipas de segurança profissionais.

Ver original
Esta página pode conter conteúdo de terceiros, que é fornecido apenas para fins informativos (não para representações/garantias) e não deve ser considerada como um endosso de suas opiniões pela Gate nem como aconselhamento financeiro ou profissional. Consulte a Isenção de responsabilidade para obter detalhes.
  • Recompensa
  • 5
  • Compartilhar
Comentário
0/400
MEVHunterWangvip
· 07-07 06:21
Move é seguro, mas não é bonito
Ver originalResponder0
SybilAttackVictimvip
· 07-07 00:29
move excelente
Ver originalResponder0
AirdropSweaterFanvip
· 07-07 00:29
A segurança é um buraco que nunca se resolve.
Ver originalResponder0
YieldWhisperervip
· 07-07 00:24
já vi esta apresentação de segurança antes... ainda estou à espera daquela cadeia 'inhackeável' perfeita smh
Ver originalResponder0
StableGeniusDegenvip
· 07-07 00:19
move parece confiável, hmm
Ver originalResponder0
  • Marcar
Faça trade de criptomoedas em qualquer lugar e a qualquer hora
qrCode
Escaneie o código para baixar o app da Gate
Comunidade
Português (Brasil)
  • 简体中文
  • English
  • Tiếng Việt
  • 繁體中文
  • Español
  • Русский
  • Français (Afrique)
  • Português (Portugal)
  • Bahasa Indonesia
  • 日本語
  • بالعربية
  • Українська
  • Português (Brasil)