Análise da segurança da linguagem Move: o inovador dos contratos inteligentes
A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em um ambiente de blockchain que implementa o MoveVM. Desde o seu design inicial, considerou várias questões de segurança relacionadas a blockchains e contratos inteligentes, e se inspirou em algumas ideias de design de segurança da linguagem Rust. Como uma nova geração de linguagem de contratos inteligentes com segurança como característica principal, qual é a segurança do Move? Pode evitar ameaças de segurança comuns de máquinas virtuais de contratos como EVM e WASM a nível de linguagem ou através de mecanismos relacionados? Existem riscos de segurança únicos na própria linguagem Move?
Este artigo discutirá a questão da segurança da linguagem Move a partir de três perspectivas: características linguísticas, mecanismo de execução e ferramentas de verificação.
1. Recursos de segurança da linguagem Move
Ao contrário de muitas linguagens de programação existentes, o objetivo do design da linguagem Move é suportar a escrita de programas que possam interagir de forma segura com código não confiável, ao mesmo tempo que suporta a verificação estática. A forma como o Move atinge esse objetivo é abandonando toda a lógica não linear baseada em considerações de flexibilidade, não suportando despacho dinâmico, nem chamadas externas recursivas, mas utilizando conceitos como genéricos, armazenamento global, recursos, entre outros, para implementar alguns padrões de programação alternativos.
Aqui estão algumas características de segurança chave da linguagem Move:
Modular: Cada módulo Move é composto por uma série de tipos de estrutura e definições de processos. Os módulos podem importar tipos declarados em outros módulos e chamar seus processos.
Tipo de recurso: A estrutura definida pela sintaxe has key é o tipo de recurso, que pode ser armazenado em armazenamento de chave-valor global persistente.
Armazenamento global: permite que os programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui, mas que podem ser visualizados por outros módulos no livro público.
Sistema de tipos estáticos: Move possui um poderoso sistema de tipos estáticos que pode capturar muitos erros em tempo de compilação.
Tipos lineares: o tipo de recurso é por padrão um tipo linear, evitando que seja copiado ou destruído implicitamente.
Invariante de redução: é possível definir invariantes de conservação de estado, utilizados para verificação formal.
Verificador de bytecode: impõe um sistema de tipos a nível de bytecode, prevenindo comportamentos maliciosos.
Essas características constroem a base de segurança da linguagem Move, permitindo que ela evite muitas vulnerabilidades comuns em contratos inteligentes.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual e não pode acessar a memória do sistema durante a execução, garantindo a execução segura em ambientes não confiáveis.
Move utiliza um interpretador baseado em pilha para executar instruções de bytecode. Seu estado é composto pela pilha de chamadas, memória, variáveis globais e pilha de operandos. Este design facilita o controle e a detecção da cópia e movimentação entre variáveis.
O MoveVM separa o armazenamento de dados e a pilha de chamadas, que é a sua maior diferença em relação ao EVM. Os recursos sob o endereço da conta do estado do usuário ( são armazenados de forma independente ), e as chamadas de programa devem cumprir regras obrigatórias relacionadas a permissões e recursos. Esse design sacrifica certa flexibilidade, mas aumenta significativamente a segurança e a eficiência da execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal da linguagem Move, que utiliza algoritmos de verificação dedutiva para validar se um programa corresponde ao comportamento esperado. Ela pode inferir o comportamento do programa com base em informações conhecidas, garantindo que ele corresponda ao esperado, ajudando a garantir a correção do programa e a reduzir a carga de trabalho de testes manuais.
O fluxo de trabalho do Move Prover é o seguinte:
Receber o arquivo fonte Move como entrada, o qual deve conter as especificações do programa.
Extrair a especificação e compilar o arquivo de origem em bytes.
Converter o padrão e o código de bytes em um modelo de objeto de validador.
Traduzir o modelo para a linguagem intermediária Boogie.
O sistema de verificação Boogie gera condições de verificação.
O resolvedor Z3 verifica se as condições de validação são atendidas.
Gerar relatórios de diagnóstico e converter em erros de nível de código-fonte.
A Linguagem de Especificação Move é utilizada para descrever as especificações dos programas, sendo um subconjunto da linguagem Move. Ela suporta a descrição estática do comportamento correto dos programas, sem afetar o código de produção. As especificações podem ser escritas de forma independente, facilitando a separação entre o código de negócios e o código de verificação.
4. Resumo
A linguagem Move tem um design excepcional em termos de segurança, considerando de forma abrangente desde as características da linguagem, a execução da máquina virtual até as ferramentas de segurança. Sacrificou parte da flexibilidade, reforçando a verificação de tipos e a lógica linear, facilitando a automação da verificação de compilação e da validação formal. O design do MoveVM separa o estado da lógica, alinhando-se melhor às necessidades de gestão de segurança de ativos em blockchain.
A linguagem Move pode evitar eficazmente as vulnerabilidades comuns no EVM, como reentrância, estouro, injeções 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 dos desenvolvedores. Embora o Move tenha considerado cuidadosamente a segurança para os programadores, não existe uma linguagem ou programa absolutamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem os serviços de auditoria de empresas de segurança de terceiros e deixem a elaboração e validação de códigos normativos a cargo de equipas de segurança profissionais.
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.
17 Curtidas
Recompensa
17
5
Repostar
Compartilhar
Comentário
0/400
OptionWhisperer
· 07-15 10:34
Vai diretamente ao Preço do chão para ver o movimento
Ver originalResponder0
NftCollectors
· 07-14 08:08
Move esta armadilha de segurança não é inferior à proporção áurea da arte bizantina, do ponto de vista da história da arte Blockchain, é completamente um marco.
Ver originalResponder0
BearMarketSurvivor
· 07-14 03:19
A segurança é uma boa conversa fiada.
Ver originalResponder0
ForkTongue
· 07-14 03:08
Há novos brinquedos para escrever contratos?
Ver originalResponder0
FancyResearchLab
· 07-14 03:05
Mais uma nova armadilha que o Luban gosta. Teoricamente, é bastante seguro.
Análise de segurança da linguagem Move: o novo padrão para desenvolvimento de contratos inteligentes
Análise da segurança da linguagem Move: o inovador dos contratos inteligentes
A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em um ambiente de blockchain que implementa o MoveVM. Desde o seu design inicial, considerou várias questões de segurança relacionadas a blockchains e contratos inteligentes, e se inspirou em algumas ideias de design de segurança da linguagem Rust. Como uma nova geração de linguagem de contratos inteligentes com segurança como característica principal, qual é a segurança do Move? Pode evitar ameaças de segurança comuns de máquinas virtuais de contratos como EVM e WASM a nível de linguagem ou através de mecanismos relacionados? Existem riscos de segurança únicos na própria linguagem Move?
Este artigo discutirá a questão da segurança da linguagem Move a partir de três perspectivas: características linguísticas, mecanismo de execução e ferramentas de verificação.
1. Recursos de segurança da linguagem Move
Ao contrário de muitas linguagens de programação existentes, o objetivo do design da linguagem Move é suportar a escrita de programas que possam interagir de forma segura com código não confiável, ao mesmo tempo que suporta a verificação estática. A forma como o Move atinge esse objetivo é abandonando toda a lógica não linear baseada em considerações de flexibilidade, não suportando despacho dinâmico, nem chamadas externas recursivas, mas utilizando conceitos como genéricos, armazenamento global, recursos, entre outros, para implementar alguns padrões de programação alternativos.
Aqui estão algumas características de segurança chave da linguagem Move:
Modular: Cada módulo Move é composto por uma série de tipos de estrutura e definições de processos. Os módulos podem importar tipos declarados em outros módulos e chamar seus processos.
Tipo de recurso: A estrutura definida pela sintaxe has key é o tipo de recurso, que pode ser armazenado em armazenamento de chave-valor global persistente.
Armazenamento global: permite que os programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui, mas que podem ser visualizados por outros módulos no livro público.
Sistema de tipos estáticos: Move possui um poderoso sistema de tipos estáticos que pode capturar muitos erros em tempo de compilação.
Tipos lineares: o tipo de recurso é por padrão um tipo linear, evitando que seja copiado ou destruído implicitamente.
Invariante de redução: é possível definir invariantes de conservação de estado, utilizados para verificação formal.
Verificador de bytecode: impõe um sistema de tipos a nível de bytecode, prevenindo comportamentos maliciosos.
Essas características constroem a base de segurança da linguagem Move, permitindo que ela evite muitas vulnerabilidades comuns em contratos inteligentes.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual e não pode acessar a memória do sistema durante a execução, garantindo a execução segura em ambientes não confiáveis.
Move utiliza um interpretador baseado em pilha para executar instruções de bytecode. Seu estado é composto pela pilha de chamadas, memória, variáveis globais e pilha de operandos. Este design facilita o controle e a detecção da cópia e movimentação entre variáveis.
O MoveVM separa o armazenamento de dados e a pilha de chamadas, que é a sua maior diferença em relação ao EVM. Os recursos sob o endereço da conta do estado do usuário ( são armazenados de forma independente ), e as chamadas de programa devem cumprir regras obrigatórias relacionadas a permissões e recursos. Esse design sacrifica certa flexibilidade, mas aumenta significativamente a segurança e a eficiência da execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal da linguagem Move, que utiliza algoritmos de verificação dedutiva para validar se um programa corresponde ao comportamento esperado. Ela pode inferir o comportamento do programa com base em informações conhecidas, garantindo que ele corresponda ao esperado, ajudando a garantir a correção do programa e a reduzir a carga de trabalho de testes manuais.
O fluxo de trabalho do Move Prover é o seguinte:
A Linguagem de Especificação Move é utilizada para descrever as especificações dos programas, sendo um subconjunto da linguagem Move. Ela suporta a descrição estática do comportamento correto dos programas, sem afetar o código de produção. As especificações podem ser escritas de forma independente, facilitando a separação entre o código de negócios e o código de verificação.
4. Resumo
A linguagem Move tem um design excepcional em termos de segurança, considerando de forma abrangente desde as características da linguagem, a execução da máquina virtual até as ferramentas de segurança. Sacrificou parte da flexibilidade, reforçando a verificação de tipos e a lógica linear, facilitando a automação da verificação de compilação e da validação formal. O design do MoveVM separa o estado da lógica, alinhando-se melhor às necessidades de gestão de segurança de ativos em blockchain.
A linguagem Move pode evitar eficazmente as vulnerabilidades comuns no EVM, como reentrância, estouro, injeções 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 dos desenvolvedores. Embora o Move tenha considerado cuidadosamente a segurança para os programadores, não existe uma linguagem ou programa absolutamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem os serviços de auditoria de empresas de segurança de terceiros e deixem a elaboração e validação de códigos normativos a cargo de equipas de segurança profissionais.