Análise da Segurança da Linguagem Move: Quebra de Paradigma na Nova Geração de Contratos Inteligentes
A linguagem Move é uma linguagem de contratos inteligentes projetada para ambientes de blockchain, com características de segurança únicas. Este artigo explora 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. Características de segurança da linguagem Move
A linguagem Move abandonou características que eram flexíveis, mas inseguras, como a despachação dinâmica e chamadas externas recursivas, adotando conceitos como genéricos, armazenamento global e recursos para implementar um padrão de programação alternativo. Esses designs ajudam a evitar vulnerabilidades comuns, como a reentrada.
O mecanismo central de segurança do Move inclui:
Módulo: cada módulo é composto por tipos de estrutura e definições de processo, podendo importar definições de tipo de outros módulos e invocar seus processos.
Estruturas: podem ser definidas como tipos de recurso, armazenados no armazenamento de chave-valor global.
Processo: define a funcionalidade e a lógica do contrato.
Armazenamento global: permite o armazenamento persistente de dados, que só podem ser lidos e escritos de forma programática pelo módulo proprietário.
Verificação de invariantes: define a conservação do estado do sistema através de uma linguagem de especificação.
Validador de bytecode: impõe um sistema de tipos ao nível do bytecode, prevenindo operações ilegais em valores sensíveis.
2. Mecanismo de execução do Move
O programa Move é executado na máquina virtual e não pode acessar diretamente a memória do sistema. O MoveVM utiliza um interpretador baseado em pilha para executar instruções de bytecode, separando a gestão de dados armazenados e da pilha de chamadas.
O estado do programa Move é composto por uma pilha de chamadas, memória, variáveis globais e uma matriz de operações. Durante a execução, a pilha de chamadas salva informações de contexto, e o salto estático evita a despachagem dinâmica, aumentando assim a imutabilidade das chamadas de função.
Este design separa o estado do usuário (, os recursos ) e a lógica do programa, melhorando 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 está em conformidade com as expectativas. O seu fluxo de trabalho é o seguinte:
Receber o arquivo fonte Move e a especificação
Compilar para bytecode e modelo de objeto de validador
Converter para a linguagem intermediária Boogie
Gerar condições de verificação
Usar o solucionador Z3 para verificar a satisfatibilidade da fórmula
Gerar relatório de diagnóstico
A Linguagem de Especificação Move é utilizada para descrever as especificações de comportamento dos programas, podendo ser escrita independentemente do código de negócios. Isso fornece uma via adicional de validação para empresas de segurança de terceiros.
Resumo
A linguagem Move foi projetada com uma forte consideração pela segurança, com otimizações abrangentes desde as características da linguagem, a execução da máquina virtual até as ferramentas de verificação. Ela pode evitar efetivamente vulnerabilidades comuns como reentrância e estouro, mas ainda é necessário prestar atenção a questões de segurança em aspectos como autenticação e lógica.
Embora o Move ofereça uma boa segurança, recomenda-se que os desenvolvedores ainda utilizem serviços de auditoria de terceiros e considerem delegar a redação e verificação das normas a uma equipe de segurança profissional, para aumentar ainda mais a segurança dos contratos inteligentes.
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.
11 gostos
Recompensa
11
9
Partilhar
Comentar
0/400
DaoResearcher
· 07-23 18:12
Citando o terceiro capítulo do artigo de governança do Vitalik, este design em pilha é mais seguro do que o EVM em mais de 67% dos casos.
Ver originalResponder0
ShibaOnTheRun
· 07-23 17:08
Auditoria, auditoria, ainda é preciso auditar, huh?
Ver originalResponder0
BearMarketSurvivor
· 07-23 03:14
move tão poderoso? Aprenda a usá-lo
Ver originalResponder0
NullWhisperer
· 07-23 01:37
teoricamente seguro, ainda precisa de testes de penetração... típica confiança excessiva em métodos formais, para ser honesto
Análise das características de segurança da linguagem Move: criando um ambiente de desenvolvimento de contratos inteligentes mais seguro
Análise da Segurança da Linguagem Move: Quebra de Paradigma na Nova Geração de Contratos Inteligentes
A linguagem Move é uma linguagem de contratos inteligentes projetada para ambientes de blockchain, com características de segurança únicas. Este artigo explora 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. Características de segurança da linguagem Move
A linguagem Move abandonou características que eram flexíveis, mas inseguras, como a despachação dinâmica e chamadas externas recursivas, adotando conceitos como genéricos, armazenamento global e recursos para implementar um padrão de programação alternativo. Esses designs ajudam a evitar vulnerabilidades comuns, como a reentrada.
O mecanismo central de segurança do Move inclui:
Módulo: cada módulo é composto por tipos de estrutura e definições de processo, podendo importar definições de tipo de outros módulos e invocar seus processos.
Estruturas: podem ser definidas como tipos de recurso, armazenados no armazenamento de chave-valor global.
Processo: define a funcionalidade e a lógica do contrato.
Armazenamento global: permite o armazenamento persistente de dados, que só podem ser lidos e escritos de forma programática pelo módulo proprietário.
Verificação de invariantes: define a conservação do estado do sistema através de uma linguagem de especificação.
Validador de bytecode: impõe um sistema de tipos ao nível do bytecode, prevenindo operações ilegais em valores sensíveis.
2. Mecanismo de execução do Move
O programa Move é executado na máquina virtual e não pode acessar diretamente a memória do sistema. O MoveVM utiliza um interpretador baseado em pilha para executar instruções de bytecode, separando a gestão de dados armazenados e da pilha de chamadas.
O estado do programa Move é composto por uma pilha de chamadas, memória, variáveis globais e uma matriz de operações. Durante a execução, a pilha de chamadas salva informações de contexto, e o salto estático evita a despachagem dinâmica, aumentando assim a imutabilidade das chamadas de função.
Este design separa o estado do usuário (, os recursos ) e a lógica do programa, melhorando 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 está em conformidade com as expectativas. O seu fluxo de trabalho é o seguinte:
A Linguagem de Especificação Move é utilizada para descrever as especificações de comportamento dos programas, podendo ser escrita independentemente do código de negócios. Isso fornece uma via adicional de validação para empresas de segurança de terceiros.
Resumo
A linguagem Move foi projetada com uma forte consideração pela segurança, com otimizações abrangentes desde as características da linguagem, a execução da máquina virtual até as ferramentas de verificação. Ela pode evitar efetivamente vulnerabilidades comuns como reentrância e estouro, mas ainda é necessário prestar atenção a questões de segurança em aspectos como autenticação e lógica.
Embora o Move ofereça uma boa segurança, recomenda-se que os desenvolvedores ainda utilizem serviços de auditoria de terceiros e considerem delegar a redação e verificação das normas a uma equipe de segurança profissional, para aumentar ainda mais a segurança dos contratos inteligentes.