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 aos contratos inteligentes. 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. As características de segurança da linguagem Move
A linguagem Move abandonou muitas características flexíveis, mas inseguras, como despacho dinâmico e chamadas externas recursivas, adotando em vez disso conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação seguro.
As principais características de segurança do Move incluem:
Modular: Cada módulo é composto por tipos de estrutura e definições de processos, podendo importar tipos de outros módulos e chamar processos de outros módulos.
Tipo de recurso: O tipo de recurso é definido através da sintaxe has key e pode ser armazenado no armazenamento de chave-valor global.
Armazenamento global: permite o armazenamento persistente de dados, acessível apenas pelos módulos que o possuem.
Controlo de acesso: pode limitar endereços específicos a chamar certos processos.
Invariantes de redução: é possível definir invariantes de verificação estática, garantindo a conservação do estado.
Verificação de bytecode: aplica forçosamente o sistema de tipos a nível de bytecode, prevenindo operações ilegais.
Essas características permitem que o Move suporte a escrita de programas de interação segura e suporte a validação estática.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual e não pode acessar diretamente a memória do sistema. Seu estado é composto pela pilha de chamadas, memória, variáveis globais e pilha de operandos.
Mecanismo de funcionamento principal:
Execução em pilha: fácil de implementar e controlar, adequado para cenários de blockchain.
Linearização de recursos: os recursos só podem ser movidos, não podem ser copiados.
Redirecionamento estático: não suporta despacho dinâmico, evitando problemas de reentrada.
Separação de dados e lógica: O estado do usuário é armazenado separadamente da lógica do programa, aumentando a segurança e a eficiência de execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal baseada em verificação dedutiva, que pode automatizar a auditoria de contratos inteligentes.
Principais características:
Descrever o comportamento do programa usando uma linguagem formal.
Utilizar um solucionador SMT para verificar a correção do programa.
Suporte para a linguagem de especificação Move Specification Language.
Poderá gerar relatórios de erros a nível de código-fonte.
Move Prover ajuda a garantir a correção dos contratos, reduzindo o risco de transações.
Resumo
A linguagem Move fez considerações de segurança abrangentes em termos de características da linguagem, execução da máquina virtual e ferramentas de segurança. Ela pode evitar efetivamente vulnerabilidades comuns como reentrância e estouro, mas ainda requer auditoria de terceiros para garantir a segurança geral. Embora o Move forneça uma boa base de segurança, os desenvolvedores ainda devem permanecer vigilantes para garantir a segurança do código.
Esta página pode conter conteúdos de terceiros, que são fornecidos apenas para fins informativos (sem representações/garantias) e não devem ser considerados como uma aprovação dos seus pontos de vista pela Gate, nem como aconselhamento financeiro ou profissional. Consulte a Declaração de exoneração de responsabilidade para obter mais informações.
19 gostos
Recompensa
19
6
Partilhar
Comentar
0/400
ForeverBuyingDips
· 18h atrás
move bem, é só que não consigo entender
Ver originalResponder0
WagmiWarrior
· 18h atrás
move segurança tão forte, então que vulnerabilidades ainda podem ser Cupões de Recorte?
Ver originalResponder0
SolidityNewbie
· 18h atrás
Embora o move seja seguro, a curva de aprendizado é muito íngreme.
Ver originalResponder0
LiquiditySurfer
· 19h atrás
como é que mover é tão difícil? Não consigo perceber.
Ver originalResponder0
MetaNeighbor
· 19h atrás
Parece um pouco confiável, mas quanto tempo conseguirá durar?
Análise de segurança da linguagem Move: características, mecanismos e ferramentas de verificação
Análise de 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 aos contratos inteligentes. 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. As características de segurança da linguagem Move
A linguagem Move abandonou muitas características flexíveis, mas inseguras, como despacho dinâmico e chamadas externas recursivas, adotando em vez disso conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação seguro.
As principais características de segurança do Move incluem:
Modular: Cada módulo é composto por tipos de estrutura e definições de processos, podendo importar tipos de outros módulos e chamar processos de outros módulos.
Tipo de recurso: O tipo de recurso é definido através da sintaxe has key e pode ser armazenado no armazenamento de chave-valor global.
Armazenamento global: permite o armazenamento persistente de dados, acessível apenas pelos módulos que o possuem.
Controlo de acesso: pode limitar endereços específicos a chamar certos processos.
Invariantes de redução: é possível definir invariantes de verificação estática, garantindo a conservação do estado.
Verificação de bytecode: aplica forçosamente o sistema de tipos a nível de bytecode, prevenindo operações ilegais.
Essas características permitem que o Move suporte a escrita de programas de interação segura e suporte a validação estática.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual e não pode acessar diretamente a memória do sistema. Seu estado é composto pela pilha de chamadas, memória, variáveis globais e pilha de operandos.
Mecanismo de funcionamento principal:
Execução em pilha: fácil de implementar e controlar, adequado para cenários de blockchain.
Linearização de recursos: os recursos só podem ser movidos, não podem ser copiados.
Redirecionamento estático: não suporta despacho dinâmico, evitando problemas de reentrada.
Separação de dados e lógica: O estado do usuário é armazenado separadamente da lógica do programa, aumentando a segurança e a eficiência de execução.
3. Mover Prover
Move Prover é uma ferramenta de verificação formal baseada em verificação dedutiva, que pode automatizar a auditoria de contratos inteligentes.
Principais características:
Move Prover ajuda a garantir a correção dos contratos, reduzindo o risco de transações.
Resumo
A linguagem Move fez considerações de segurança abrangentes em termos de características da linguagem, execução da máquina virtual e ferramentas de segurança. Ela pode evitar efetivamente vulnerabilidades comuns como reentrância e estouro, mas ainda requer auditoria de terceiros para garantir a segurança geral. Embora o Move forneça uma boa base de segurança, os desenvolvedores ainda devem permanecer vigilantes para garantir a segurança do código.