A linguagem Move, como uma nova geração de linguagem de contratos inteligentes, considerou desde o início a questão da segurança na blockchain e nos contratos inteligentes. Este artigo irá explorar a segurança da linguagem Move a partir de três níveis: 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 possui as seguintes principais características de segurança:
Abandonou a lógica não linear, não suporta dispatch dinâmico e chamadas externas recursivas
Implementar padrões de programação alternativos utilizando conceitos como genéricos, armazenamento global, recursos, etc.
Design modular, cada módulo é composto por tipo de estrutura e definição de processo
O tipo de recurso e o mecanismo de armazenamento global garantem a segurança do armazenamento e dos recursos
Implementação de verificação de segurança em tempo de compilação de invariantes e validadores de bytecode
O verificador de bytecode realiza principalmente três tipos de verificações:
Verificação da legalidade da estrutura
Detecção semântica da lógica do processo
Detecção de erros ao conectar
Através desses mecanismos, o Move consegue garantir uma alta segurança já na fase de compilação.
2. Mecanismo de operação 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 operação de arrays.
Diferente do EVM, o MoveVM separa o armazenamento de dados da pilha de chamadas. O estado do usuário é armazenado de forma independente, e as chamadas de programas devem cumprir regras de permissões e recursos. Este design melhora a segurança e a eficiência da 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 corresponde às expectativas. O seu processo de verificação é o seguinte:
Receber o arquivo fonte Move e as especificações
Compilar para bytecode e modelo de objeto validador
Traduzir para a linguagem intermediária Boogie
Gerar condições de verificação
Verificar com o solucionador Z3
Gerar relatório de diagnóstico
A Move Specification Language é usada para descrever sistemas de especificação, sendo um subconjunto da linguagem Move.
De um modo geral, o Move Prover é uma ferramenta de segurança poderosa, mas não pode substituir completamente a auditoria manual. Recomenda-se que os desenvolvedores ainda utilizem serviços de auditoria de segurança de terceiros e deixem a parte da especificação a cargo de empresas de segurança.
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.
Análise da segurança da linguagem Move: características da linguagem, mecanismo de execução e Verificação formal
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 a questão da segurança na blockchain e nos contratos inteligentes. Este artigo irá explorar a segurança da linguagem Move a partir de três níveis: 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 possui as seguintes principais características de segurança:
O verificador de bytecode realiza principalmente três tipos de verificações:
Através desses mecanismos, o Move consegue garantir uma alta segurança já na fase de compilação.
2. Mecanismo de operação 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 operação de arrays.
Diferente do EVM, o MoveVM separa o armazenamento de dados da pilha de chamadas. O estado do usuário é armazenado de forma independente, e as chamadas de programas devem cumprir regras de permissões e recursos. Este design melhora a segurança e a eficiência da 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 corresponde às expectativas. O seu processo de verificação é o seguinte:
A Move Specification Language é usada para descrever sistemas de especificação, sendo um subconjunto da linguagem Move.
De um modo geral, o Move Prover é uma ferramenta de segurança poderosa, mas não pode substituir completamente a auditoria manual. Recomenda-se que os desenvolvedores ainda utilizem serviços de auditoria de segurança de terceiros e deixem a parte da especificação a cargo de empresas de segurança.