Verificação formal em contratos inteligentes

A verificação formal de contratos inteligentes é uma tendência emergente no espaço da criptomoeda focada na redução das instâncias de bugs e vulnerabilidades de contratos inteligentes que levaram a vários hacks de alto perfil e preocupações de segurança endêmicas.

A verificação formal tem uma ampla variedade de aplicações em relação a sistemas de hardware e software. Tornou-se extremamente importante à medida que a complexidade dos sistemas aumenta, especialmente com o hardware. Em redes de blockchain, a litania de vulnerabilidades e explorações de contratos inteligentes levou à necessidade de programação e auditoria de contratos inteligentes.

Verificação formal em contratos inteligentes

Antecedentes da Verificação Formal

Usos de verificação formal métodos formais para verificar se o design de um sistema de hardware ou software atende ou não a um conjunto específico de propriedades. Os métodos formais são um tipo particular de técnica matemática para a especificação, desenvolvimento e verificação de sistemas de hardware e software. O uso de métodos formais para provar ou refutar a correção dos algoritmos pretendidos é conhecido como verificação formal.

Martin Davis é creditado por desenvolver a primeira prova matemática gerada por computador em 1954. O conceito começou a ganhar força na década de 1960 para verificar a exatidão de programas de computador em linguagens antigas como Pascal e Java. Seguindo alguns bugs de computador de alto perfil, como o Bug Pentium FDIV em 1994, o sentimento de que a verificação formal precisava ser onipresente começou a crescer.

O teste de um sistema de software ou hardware pode ser dividido em duas fases gerais:

  1. Validação
  2. Verificação

A validação é determinar se o produto atende às necessidades do usuário.

A verificação está testando se o produto está ou não em conformidade com as especificações.

A verificação consiste em produzir um modelo matemático abstrato que se correlaciona com as especificações de design do produto (ou seja, algoritmo, chip de hardware), enquanto os métodos formais usados ​​para gerar o modelo derivam principalmente de fundamentos teóricos da ciência da computação.

O uso de verificação formal tornou-se extremamente importante em sistemas de hardware, onde é usado por quase todos os principais fabricantes de hardware para garantir a robustez de seus produtos. No entanto, seu uso não é tão predominante em software quanto em hardware, o que é atribuído principalmente à natureza comercial da fabricação de hardware.

No entanto, essa dinâmica está começando a mudar com o advento de blockchains e criptomoedas, onde transferências consideráveis ​​de valor são executadas de forma autônoma em uma rede descentralizada. Com mais valor em jogo do que os sistemas tradicionais, a exatidão dos contratos inteligentes tornou-se uma preocupação premente.

UMA breve história de exploits de contratos inteligentes é tudo o que precisamos para entender as consequências de vulnerabilidades simples no código do contrato.

Por que usá-lo para contratos inteligentes?

De acordo com um recente estude executado em quase 1 milhão de contratos inteligentes Ethereum, 34.200 deles foram marcados como vulneráveis, em 10 segundos por contrato. Esse número surpreendente foi alcançado analisando vulnerabilidades de rastreamento de contratos inteligentes, incluindo:

  • Encontrar contratos que bloqueiam fundos indefinidamente
  • Contratos que vazam fundos descuidadamente para usuários arbitrários
  • Contratos que podem ser cancelados por qualquer pessoa

Junto com a complexidade lógica geral e a novidade associada à programação de contratos inteligentes para blockchains, sua natureza imutável – uma vez que estão comprometidos com a blockchain – torna as vulnerabilidades potencialmente muito mais prejudiciais.

Brian Marick e Daejun Park fornecem um excelente análise de vulnerabilidades de contratos inteligentes e como a verificação formal pode ajudar a mitigar suas instâncias. Basicamente, existem duas maneiras pelas quais um desenvolvedor pode não conseguir o que deseja de um contrato inteligente.

  1. Intenção mal compreendida
  2. Cometer um erro ao implementar essa intenção

Muitos desses erros padrão podem levar a enormes somas de fundos bloqueados, como com o Carteira paridade ou com Ethereum exploit de envio recursivo no Incidente DAO. A verificação formal é usada como uma forma de confirmar matematicamente que vulnerabilidades específicas não levarão a vetores de exploração prejudiciais.

Uma especificação formal é usada como a saída ou resultado preciso que um contrato inteligente está procurando e que um computador pode verificar. A verificação subsequentemente ocorre uma vez que o contrato compila para o bytecode e a verificação formal prova que o bytecode compilado implementa a especificação. No entanto, realizar verificações formais manualmente é um processo árduo e às vezes vem com seus próprios erros. Mesmo a verificação de resultados de provas formais pode vir com suas nuances.

Ferramentas como o Coq Proof Assistant foram desenvolvidos para ajudar a facilitar as provas mecanizadas sobre as propriedades dos programas e são atualmente usados ​​por várias criptomoedas emergentes com as linguagens que usam embutidas no Coq.

Embora a auditoria inteligente de contratos forneça uma camada muito necessária de garantia por meio de revisões de código, a verificação formal de contratos inteligentes pode ajudar a reduzir os casos de vulnerabilidades por meio de análises matemáticas adicionais. Com os contratos inteligentes se tornando mais prevalentes, parece natural que a aplicação de verificação formal se torne mais difundida na indústria.

Aplicações Atuais de Verificação Formal

Várias plataformas já estão integrando a verificação formal ou planejam fazê-lo em breve. Avaliar a proteção e a proteção de contratos inteligentes que operam dentro dessas plataformas será vital para medir sua eficácia em conter vulnerabilidades críticas.

Zilliqa

Zilliqa é uma blockchain de alto rendimento projetada para hospedar aplicativos descentralizados (dapps) escalonáveis ​​e seguros. Vários dos desenvolvedores técnicos por trás do Zilliqa foram os autores do estudo anterior que descobriu as milhares de fraquezas de contratos inteligentes.

Zilliqa

Zilliqa usa uma nova linguagem de programação chamada Scilla, projetada por membros da equipe Zilliqa e alguns outros afiliados. Scilla é uma linguagem de nível intermediário que está embutida no Coq Proof Assistant. Destina-se a ser um alvo de tradução para linguagens de nível superior para realizar análise e verificação antes que os contratos sejam compilados para bytecode.

Tezos

Tezos é escrito em OCaml e sua linguagem de contrato inteligente é Michelson, baseada em OCaml. OCaml foi selecionado por causa de suas ofertas de programação funcional de velocidade, sintaxe e semântica inequívoca e recursos para implementar provas formais. Tezos também usa o Coq Proof Assistant para facilitar a verificação formal de contratos inteligentes.

Guia Tezos

Arthur Breitman – o cofundador da Tezos – postou detalhes sobre a verificação de alguns Contratos de Michelson em Coq, incluindo um contrato multi-sig em sua testnet no ano passado. Tezos foi lançado recentemente, portanto, sua aplicação de verificação formal deve fornecer um indicador excelente para o estado de segurança aprimorada de contratos inteligentes usando o método. Levará algum tempo para se desenvolverem explorações que afetaram os contratos do Solidity em Tezos, mas avaliar o quão seguros se tornam os contratos inteligentes em Tezos pode ser um indicativo de uma tendência contínua.

Cardano

Cardano é escrito em Haskell e sua linguagem de contrato inteligente é Plutus, que é baseada em Haskell.

Guia Cardano

Cardano é projetado com uma camada de computação Cardano (CCL) que consiste em 2 camadas:

  1. Uma máquina virtual especificada formalmente e uma estrutura de linguagem
  2. Linguagens formalmente especificadas que facilitam a verificação do código de contrato inteligente

O objetivo é criar um ambiente que agilize o processo de garantir que um contrato funcione conforme projetado, sem vulnerabilidades catastróficas. Notavelmente, Cardano não usa um design de pilha limitada como o EVM de Ethereum, então não se preocupar com o fluxo aritmético da pilha permite que ele verifique formalmente os contratos inteligentes com muito mais facilidade.

Ethereum

A Ethereum pesquisa há algum tempo a incorporação da verificação formal, com diversos projetos investigando seu potencial. Uma dessas publicações, “Tornando os contratos inteligentes mais inteligentes,”Se concentra em bugs de contrato inteligentes e sugere maneiras de mitigá-los, incluindo a melhoria da semântica operacional do Ethereum para promover a verificação formal.

Guia Ethereum

Limites de gás em Ethereum tornam isso desafiador para implementar a verificação formal. Além disso, a única maneira de saber o significado de um programa Solidity é compilá-lo em bytecode. O compilador muda rapidamente, portanto, as ferramentas de verificação também precisam se ajustar à taxa de mudança. Considerando a rede estabelecida e a história da Ethereum, a verificação formal de contratos inteligentes em Ethereum aparentemente forneceria o melhor indicador de sua eficácia na mitigação de vulnerabilidades se a verificação formal se tornasse amplamente usada na rede.

Conclusão

A verificação formal é uma tarefa altamente complexa e árdua. Apesar disso, ele se tornou um padrão universal na indústria de hardware e provavelmente continuará ganhando força no mercado de software. Blockchains e redes de criptomoedas – onde transferências de alto valor são comuns – seguramente acelerarão esse efeito. Medir o impacto positivo da verificação formal de contratos inteligentes provavelmente levará vários anos para se desdobrar, pois estamos apenas vendo o início do que deve se tornar uma tendência muito mais ampla na indústria.

Mike Owergreen Administrator
Sorry! The Author has not filled his profile.
follow me