A linguagem Move, como uma nova geração de linguagem de contratos inteligentes, considerou desde o início as questões de segurança relacionadas à blockchain e contratos inteligentes. Este artigo irá explorar a segurança da linguagem Move sob 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 abandonou a lógica não linear baseada em flexibilidade, não suporta dispatch dinâmico e chamadas externas recursivas, mas utiliza conceitos como generics, armazenamento global, recursos, entre outros, para implementar um modelo de programação alternativo. Esses designs ajudam a evitar vulnerabilidades de segurança como reentrâncias.
Os principais componentes da linguagem Move incluem:
Módulo: composto por definições de tipos de estrutura e processos, pode importar definições de tipos de outros módulos e chamar processos de outros módulos.
Estruturas: podem ser definidas como tipos de recursos, armazenados na loja de chave-valor global.
Processo: definir as funções do módulo, podendo incluir processos de inicialização, seguros e inseguros.
O mecanismo de armazenamento global da linguagem Move permite que os módulos armazenem dados persistentes e tenham acesso exclusivo de leitura e escrita aos tipos de recursos que declaram. Este mecanismo ajuda a impor restrições de segurança.
Duas importantes características de verificação estática da linguagem Move:
Verificação de invariantes: definição da conservação do estado do sistema através de uma linguagem de especificação.
Validador de bytecode: execução forçada de tipos seguros e linearização, prevenindo operações ilegais.
2. Mecanismo de operação do Move
O programa Move é executado em uma máquina virtual, não podendo acessar diretamente a memória do sistema. A execução do programa é baseada em pilha, com o armazenamento global dividido em memória ( pilha ) e variáveis globais ( pilha ).
O estado de execução da Move VM é composto pela pilha de chamadas, memória, variáveis globais e operações. As suas características incluem:
Salto estático, evitando a distribuição dinâmica
Pilhas de chamada adjacentes, para evitar reentrada
Separação de armazenamento de dados e pilha de chamadas
Este design melhora a segurança e a eficiência de execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal que utiliza algoritmos de verificação dedutiva para validar se um programa está em conformidade com o esperado. Seu fluxo de trabalho:
Receber o arquivo fonte Move e as normas
Compilar para bytecode e modelo de objeto do validador
Converter para a linguagem intermediária Boogie
Gerar condições de verificação
Verificação com o solucionador Z3
Gerar relatório de diagnóstico
A Linguagem de Especificação de Movimento é usada para descrever as especificações do comportamento do programa, podendo ser escrita independentemente do código de negócios.
Resumo
A linguagem Move considera de forma abrangente as características da linguagem, a execução da máquina virtual e as ferramentas de segurança, podendo efetivamente evitar muitas vulnerabilidades comuns. No entanto, ainda se recomenda o uso de serviços de auditoria de segurança de terceiros, e que a escrita e validação de código em conformidade seja realizada por empresas de segurança.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
17 gostos
Recompensa
17
8
Partilhar
Comentar
0/400
HashBard
· 7h atrás
ainda tem exploits... teatro de segurança no seu melhor, para ser honesto
Ver originalResponder0
AirdropHarvester
· 18h atrás
bull批 Justo a segurança em primeiro lugar!
Ver originalResponder0
CryptoNomics
· 18h atrás
*suspiro* mais um L1 a tentar a verificação formal... estatisticamente insignificante sem uma análise adequada do equilíbrio de Nash na minha opinião
Ver originalResponder0
ForumMiningMaster
· 18h atrás
Gosto deste tipo de ativo seguro.
Ver originalResponder0
DegenGambler
· 18h atrás
A verificação estática é suficiente?
Ver originalResponder0
ponzi_poet
· 18h atrás
Ainda tem que ver a performance específica, estático é estático.
Ver originalResponder0
fork_in_the_road
· 18h atrás
Ainda a escrever solidity? Rápido, entra numa posição Move
Ver originalResponder0
DaoTherapy
· 18h atrás
Finalmente encontrei uma linguagem de contrato confiável
Análise completa da segurança da linguagem Move: das características às ferramentas de verificação
Análise da segurança da linguagem Move
A linguagem Move, como uma nova geração de linguagem de contratos inteligentes, considerou desde o início as questões de segurança relacionadas à blockchain e contratos inteligentes. Este artigo irá explorar a segurança da linguagem Move sob 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 abandonou a lógica não linear baseada em flexibilidade, não suporta dispatch dinâmico e chamadas externas recursivas, mas utiliza conceitos como generics, armazenamento global, recursos, entre outros, para implementar um modelo de programação alternativo. Esses designs ajudam a evitar vulnerabilidades de segurança como reentrâncias.
Os principais componentes da linguagem Move incluem:
Módulo: composto por definições de tipos de estrutura e processos, pode importar definições de tipos de outros módulos e chamar processos de outros módulos.
Estruturas: podem ser definidas como tipos de recursos, armazenados na loja de chave-valor global.
Processo: definir as funções do módulo, podendo incluir processos de inicialização, seguros e inseguros.
O mecanismo de armazenamento global da linguagem Move permite que os módulos armazenem dados persistentes e tenham acesso exclusivo de leitura e escrita aos tipos de recursos que declaram. Este mecanismo ajuda a impor restrições de segurança.
Duas importantes características de verificação estática da linguagem Move:
Verificação de invariantes: definição da conservação do estado do sistema através de uma linguagem de especificação.
Validador de bytecode: execução forçada de tipos seguros e linearização, prevenindo operações ilegais.
2. Mecanismo de operação do Move
O programa Move é executado em uma máquina virtual, não podendo acessar diretamente a memória do sistema. A execução do programa é baseada em pilha, com o armazenamento global dividido em memória ( pilha ) e variáveis globais ( pilha ).
O estado de execução da Move VM é composto pela pilha de chamadas, memória, variáveis globais e operações. As suas características incluem:
Este design melhora a segurança e a eficiência de execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal que utiliza algoritmos de verificação dedutiva para validar se um programa está em conformidade com o esperado. Seu fluxo de trabalho:
A Linguagem de Especificação de Movimento é usada para descrever as especificações do comportamento do programa, podendo ser escrita independentemente do código de negócios.
Resumo
A linguagem Move considera de forma abrangente as características da linguagem, a execução da máquina virtual e as ferramentas de segurança, podendo efetivamente evitar muitas vulnerabilidades comuns. No entanto, ainda se recomenda o uso de serviços de auditoria de segurança de terceiros, e que a escrita e validação de código em conformidade seja realizada por empresas de segurança.