Análise da segurança da linguagem Move: o revolucionário das linguagens de contratos inteligentes
Introdução
A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em ambientes de blockchain que implementam o MoveVM. Seu design leva em consideração muitas questões de segurança relacionadas a blockchains e contratos inteligentes, e se inspira em alguns princípios de design de segurança da linguagem Rust. Como uma nova geração de linguagem de contratos inteligentes com foco principal na segurança, qual é a segurança do Move? Pode ela evitar ameaças de segurança comuns em máquinas virtuais de contratos como EVM e WASM, seja a nível de linguagem ou através de mecanismos relacionados? Existem problemas de segurança específicos associados ao Move?
Este artigo discutirá a questão da segurança da linguagem Move a partir de três níveis: características da linguagem, mecanismo de funcionamento e ferramentas de verificação.
1. Características de segurança da linguagem Move
Ao contrário de muitas linguagens de programação existentes, a linguagem Move foi projetada para suportar interações seguras com códigos não confiáveis e também para permitir a verificação estática. Move abandonou a lógica não linear baseada em considerações de flexibilidade, não suporta despacho dinâmico e chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação alternativo. Por exemplo, Move omite características de despacho dinâmico e chamadas recursivas que poderiam levar a vulnerabilidades de reentrada.
As principais características de segurança do Move incluem:
Módulo: Cada módulo Move é composto por uma série de definições de tipos de estrutura e processos. Os módulos podem importar definições de tipos e chamar processos declarados em outros módulos.
Estrutura: pode ser definida como um tipo de recurso, representando algo que pode ser armazenado em um armazenamento persistente de chave/valor global.
Processo: definiu a inicialização, o processo seguro e o processo inseguro.
Armazenamento Global: permite que programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui.
Verificação de invariantes: suporte a invariantes com verificação estática, garantindo a integridade dos recursos no sistema.
validador de bytecode: impõe o sistema de tipos a nível de bytecode, evitando operações ilegais de módulos de cliente maliciosos.
Através de duas mecânicas, verificação de invariantes e verificador de bytecode, o Move implementa uma dupla garantia de segurança de código em tempo de compilação.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual, e durante a execução não pode acessar a memória do sistema. Isso permite que o Move funcione de forma segura em ambientes não confiáveis, sem ser comprometido ou abusado.
O programa Move é executado na pilha, e o armazenamento global é dividido em duas partes: memória ( heap ) e variáveis globais ( pilha ). A memória é um armazenamento de primeiro nível, cujas unidades não podem armazenar ponteiros que apontam para unidades de memória. As variáveis globais são usadas para armazenar ponteiros que apontam para unidades de memória, mas o modo de indexação é diferente da memória.
As instruções em bytecode do Move são executadas em um interpretador baseado em pilha. A máquina virtual baseada em pilha é fácil de implementar e controlar, requer menos do ambiente de hardware, sendo adequada para cenários de blockchain. Em comparação com um interpretador baseado em registradores, um interpretador baseado em pilha torna as operações de cópia e movimentação entre variáveis mais fáceis de controlar e detectar.
O estado de execução do programa Move é um quádruplo ⟨C, M, G, S⟩, que inclui a pilha de chamadas (C), a memória (M), as variáveis globais (G) e os operandos (S). A pilha também mantém uma tabela de funções para resolver as instruções que contêm os corpos das funções.
O MoveVM separa a lógica do processo de armazenamento de dados e da pilha de chamadas (, que é a maior diferença em relação ao EVM. No MoveVM, os recursos ) sob o endereço da conta de 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. Este design sacrifica certa flexibilidade, mas contribui significativamente para a segurança e a eficiência de execução ), facilitando a execução concorrente (.
![Análise de segurança do Move: a linguagem de contratos inteligentes que muda o jogo])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Mover Prover
Move Prover é uma ferramenta de verificação formal baseada em raciocínio. Ela utiliza uma linguagem formal para descrever o comportamento do programa e algoritmos de raciocínio para verificar se o programa atende às expectativas, ajudando os desenvolvedores a garantir a correção dos contratos inteligentes e a reduzir o risco de transações.
O Move Prover utiliza um algoritmo de verificação dedutiva para validar se o programa está de acordo com as expectativas. Isso significa que pode inferir o comportamento do programa com base nas informações conhecidas, garantindo que corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa e a reduzir a carga de trabalho dos testes manuais.
O fluxo de trabalho do Move Prover é o seguinte:
Receber o arquivo fonte Move como entrada, o arquivo deve definir as normas de entrada do programa.
O Parser Move extrai a especificação do código fonte.
O compilador Move compila os arquivos fonte em bytecode, transformando-os em conjunto com o sistema de especificações em um modelo de objeto validador.
O modelo é traduzido para a linguagem intermediária Boogie.
O código Boogie é enviado para o sistema de verificação Boogie, gerando condições de verificação.
Condições de verificação passadas para o resolvedor Z3 ), o resolvedor SMT desenvolvido pela Microsoft (.
O Z3 verifica se a fórmula SMT é insatisfatível. Se for, isso indica que a especificação é válida; caso contrário, gera um modelo que satisfaz as condições.
Reverta o relatório de diagnóstico para um erro no nível da fonte.
Move utiliza a Move Specification Language para descrever as especificações do sistema. É um subconjunto da linguagem Move, que suporta a descrição estática do comportamento de correção do programa, sem afetar a produção. Pode ser escrito de forma independente como um arquivo de especificação dedicado, separando o código de negócio do código de verificação formal.
Move Prover é uma ferramenta útil que ajuda os desenvolvedores a garantir a correção dos contratos inteligentes. Ela utiliza uma linguagem formal para descrever o comportamento do programa e emprega algoritmos de raciocínio para verificar se o programa está de acordo com as expectativas, ajudando a reduzir os riscos de transação e permitindo que os desenvolvedores implantem contratos inteligentes em ambientes de produção com mais confiança.
![Move segurança análise: contratos inteligentes linguagem do Game Changer])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Resumo
A linguagem Move se destaca muito em termos de design de segurança, oferecendo uma consideração abrangente em características de linguagem, execução de máquina virtual e ferramentas de segurança. As características da linguagem sacrificam parte da flexibilidade, exigindo verificação de tipos e lógica linear, facilitando a automação de verificações de compilação e a verificabilidade formal e segura. O design do MoveVM separa estado e lógica, alinhando-se melhor às necessidades de gerenciamento de segurança de ativos na blockchain.
Em termos de linguagem, o Move pode evitar eficazmente vulnerabilidades comuns do EVM, como reentrada, estouro, injeção 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 dos desenvolvedores. O Move Prover pode não ser eficaz quando a ideia geral é descuidada.
Embora a linguagem Move tenha considerado muitos aspectos de segurança para os programadores, não existe uma linguagem ou programa completamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem serviços de auditoria de empresas de segurança de terceiros e que a parte da especificação do código seja escrita e verificada por empresas de segurança de terceiros.
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.
16 gostos
Recompensa
16
4
Partilhar
Comentar
0/400
DegenRecoveryGroup
· 2h atrás
Tem alguma coisa, o gosto de rust está muito forte.
Análise da segurança da linguagem Move: um novo paradigma para contratos inteligentes
Análise da segurança da linguagem Move: o revolucionário das linguagens de contratos inteligentes
Introdução
A linguagem Move é uma linguagem de contratos inteligentes que pode ser executada em ambientes de blockchain que implementam o MoveVM. Seu design leva em consideração muitas questões de segurança relacionadas a blockchains e contratos inteligentes, e se inspira em alguns princípios de design de segurança da linguagem Rust. Como uma nova geração de linguagem de contratos inteligentes com foco principal na segurança, qual é a segurança do Move? Pode ela evitar ameaças de segurança comuns em máquinas virtuais de contratos como EVM e WASM, seja a nível de linguagem ou através de mecanismos relacionados? Existem problemas de segurança específicos associados ao Move?
Este artigo discutirá a questão da segurança da linguagem Move a partir de três níveis: características da linguagem, mecanismo de funcionamento e ferramentas de verificação.
1. Características de segurança da linguagem Move
Ao contrário de muitas linguagens de programação existentes, a linguagem Move foi projetada para suportar interações seguras com códigos não confiáveis e também para permitir a verificação estática. Move abandonou a lógica não linear baseada em considerações de flexibilidade, não suporta despacho dinâmico e chamadas externas recursivas, mas utiliza conceitos como genéricos, armazenamento global e recursos para implementar um modelo de programação alternativo. Por exemplo, Move omite características de despacho dinâmico e chamadas recursivas que poderiam levar a vulnerabilidades de reentrada.
As principais características de segurança do Move incluem:
Módulo: Cada módulo Move é composto por uma série de definições de tipos de estrutura e processos. Os módulos podem importar definições de tipos e chamar processos declarados em outros módulos.
Estrutura: pode ser definida como um tipo de recurso, representando algo que pode ser armazenado em um armazenamento persistente de chave/valor global.
Processo: definiu a inicialização, o processo seguro e o processo inseguro.
Armazenamento Global: permite que programas Move armazenem dados persistentes, que só podem ser lidos e escritos programaticamente pelo módulo que os possui.
Verificação de invariantes: suporte a invariantes com verificação estática, garantindo a integridade dos recursos no sistema.
validador de bytecode: impõe o sistema de tipos a nível de bytecode, evitando operações ilegais de módulos de cliente maliciosos.
Através de duas mecânicas, verificação de invariantes e verificador de bytecode, o Move implementa uma dupla garantia de segurança de código em tempo de compilação.
2. Mecanismo de funcionamento do Move
O programa Move é executado em uma máquina virtual, e durante a execução não pode acessar a memória do sistema. Isso permite que o Move funcione de forma segura em ambientes não confiáveis, sem ser comprometido ou abusado.
O programa Move é executado na pilha, e o armazenamento global é dividido em duas partes: memória ( heap ) e variáveis globais ( pilha ). A memória é um armazenamento de primeiro nível, cujas unidades não podem armazenar ponteiros que apontam para unidades de memória. As variáveis globais são usadas para armazenar ponteiros que apontam para unidades de memória, mas o modo de indexação é diferente da memória.
As instruções em bytecode do Move são executadas em um interpretador baseado em pilha. A máquina virtual baseada em pilha é fácil de implementar e controlar, requer menos do ambiente de hardware, sendo adequada para cenários de blockchain. Em comparação com um interpretador baseado em registradores, um interpretador baseado em pilha torna as operações de cópia e movimentação entre variáveis mais fáceis de controlar e detectar.
O estado de execução do programa Move é um quádruplo ⟨C, M, G, S⟩, que inclui a pilha de chamadas (C), a memória (M), as variáveis globais (G) e os operandos (S). A pilha também mantém uma tabela de funções para resolver as instruções que contêm os corpos das funções.
O MoveVM separa a lógica do processo de armazenamento de dados e da pilha de chamadas (, que é a maior diferença em relação ao EVM. No MoveVM, os recursos ) sob o endereço da conta de 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. Este design sacrifica certa flexibilidade, mas contribui significativamente para a segurança e a eficiência de execução ), facilitando a execução concorrente (.
![Análise de segurança do Move: a linguagem de contratos inteligentes que muda o jogo])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. Mover Prover
Move Prover é uma ferramenta de verificação formal baseada em raciocínio. Ela utiliza uma linguagem formal para descrever o comportamento do programa e algoritmos de raciocínio para verificar se o programa atende às expectativas, ajudando os desenvolvedores a garantir a correção dos contratos inteligentes e a reduzir o risco de transações.
O Move Prover utiliza um algoritmo de verificação dedutiva para validar se o programa está de acordo com as expectativas. Isso significa que pode inferir o comportamento do programa com base nas informações conhecidas, garantindo que corresponda ao comportamento esperado. Isso ajuda a garantir a correção do programa e a reduzir a carga de trabalho dos testes manuais.
O fluxo de trabalho do Move Prover é o seguinte:
Move utiliza a Move Specification Language para descrever as especificações do sistema. É um subconjunto da linguagem Move, que suporta a descrição estática do comportamento de correção do programa, sem afetar a produção. Pode ser escrito de forma independente como um arquivo de especificação dedicado, separando o código de negócio do código de verificação formal.
Move Prover é uma ferramenta útil que ajuda os desenvolvedores a garantir a correção dos contratos inteligentes. Ela utiliza uma linguagem formal para descrever o comportamento do programa e emprega algoritmos de raciocínio para verificar se o programa está de acordo com as expectativas, ajudando a reduzir os riscos de transação e permitindo que os desenvolvedores implantem contratos inteligentes em ambientes de produção com mais confiança.
![Move segurança análise: contratos inteligentes linguagem do Game Changer])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. Resumo
A linguagem Move se destaca muito em termos de design de segurança, oferecendo uma consideração abrangente em características de linguagem, execução de máquina virtual e ferramentas de segurança. As características da linguagem sacrificam parte da flexibilidade, exigindo verificação de tipos e lógica linear, facilitando a automação de verificações de compilação e a verificabilidade formal e segura. O design do MoveVM separa estado e lógica, alinhando-se melhor às necessidades de gerenciamento de segurança de ativos na blockchain.
Em termos de linguagem, o Move pode evitar eficazmente vulnerabilidades comuns do EVM, como reentrada, estouro, injeção 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 dos desenvolvedores. O Move Prover pode não ser eficaz quando a ideia geral é descuidada.
Embora a linguagem Move tenha considerado muitos aspectos de segurança para os programadores, não existe uma linguagem ou programa completamente seguro. Recomenda-se que os desenvolvedores de contratos inteligentes Move utilizem serviços de auditoria de empresas de segurança de terceiros e que a parte da especificação do código seja escrita e verificada por empresas de segurança de terceiros.