O que é a verificação formal de contratos inteligentes?
P√°gina Inicial
Artigos
O que é a verificação formal de contratos inteligentes?

O que é a verificação formal de contratos inteligentes?

Avançado
Publicado em Mar 2, 2023Atualizado em Jul 12, 2023
5m

Este artigo é um envio da comunidade. O autor é David Tarditi, vice-presidente de engenharia da CertiK, empresa de auditoria de contratos inteligentes da Web3.

TL;DR

A verifica√ß√£o formal de contratos inteligentes garante que eles estejam livres de bugs, vulnerabilidades e outros comportamentos indesejados. O processo envolve um especialista humano que apresenta a l√≥gica do contrato inteligente como declara√ß√Ķes matem√°ticas e, em seguida, as executa por meio de um processo automatizado que verifica a l√≥gica real referente aos modelos de comportamento esperados do contrato. A combina√ß√£o da verifica√ß√£o formal e da auditoria manual fornece uma avalia√ß√£o abrangente da seguran√ßa de um contrato inteligente.

Introdução

Contratos inteligentes s√£o programas de computador implantados em uma blockchain que s√£o automaticamente executados quando certas condi√ß√Ķes s√£o atendidas. Existem diversos contratos, desde os mais simples at√© os extremamente complexos e eles podem manter ativos no valor de milh√Ķes ou at√© bilh√Ķes de d√≥lares.¬†¬†

Vulnerabilidades de seguran√ßa no c√≥digo de um contrato inteligente podem ter consequ√™ncias devastadoras, incluindo o roubo de todos os ativos mantidos pelo contrato. Em 2021, o automated market maker (AMM) Uranium Finance teve US$ 50 milh√Ķes roubados devido a um √ļnico erro de digita√ß√£o em um contrato inteligente.

Tamb√©m em 2021, a Compound Finance distribuiu indevidamente US$ 80 milh√Ķes em recompensas devido a um erro em um √ļnico caractere. Em 2022, US$ 320 milh√Ķes foram roubados da Wormhole Bridge por causa de um bug em um de seus contratos inteligentes.

√Č importante implementar corretamente o programa de contrato inteligente desde o in√≠cio. Os contratos inteligentes s√£o de c√≥digo aberto (open-source), ou seja, seu c√≥digo fica dispon√≠vel publicamente assim que o contrato √© implantado. Se um hacker encontrar um bug ou uma falha, ele pode, de imediato, se aproveitar disso. Al√©m disso, corrigir vulnerabilidades de seguran√ßa ao longo do tempo n√£o √© uma op√ß√£o, j√° que normalmente n√£o √© poss√≠vel modificar o c√≥digo de um contrato inteligente ap√≥s sua implanta√ß√£o.

Como funciona a verificação de um contrato inteligente?  

A verifica√ß√£o formal de contratos inteligentes funciona apresentando a l√≥gica e o comportamento desejado de contratos inteligentes na forma de declara√ß√Ķes matem√°ticas. Os auditores ent√£o usam ferramentas automatizadas para verificar se essas declara√ß√Ķes est√£o corretas.

O processo envolve:

  1. Definir as especifica√ß√Ķes e propriedades desejadas de um contrato em linguagem formal.

  2. Traduzir o código do contrato em uma representação formal, como modelos matemáticos ou uma representação lógica.

  3. Usar provadores de teoremas automatizados ou verificadores de modelo para validar as especifica√ß√Ķes e propriedades do contrato.

  4. Repetir o processo de verificação para encontrar e corrigir quaisquer erros ou desvios das propriedades desejadas.

Por que a verificação de contratos inteligentes é importante

O uso da matemática ajuda a garantir que os contratos inteligentes formalmente verificados estejam livres de bugs, vulnerabilidades e outros comportamentos indesejados. Através desse processo, também é possível aumentar a confiança no contrato, já que suas propriedades são rigorosamente comprovadas como corretas. 

Abaixo estão alguns exemplos de como a verificação de contratos inteligente ajudou a evitar perdas financeiras significativas e outras consequências desastrosas.  

Uniswap

O Uniswap é um AMM muito conhecido. Quando o contrato inteligente Uniswap V1 foi desenvolvido, ele foi verificado formalmente. Antes de seu lançamento, esta verificação formal encontrou e corrigiu erros de arredondamento que poderiam ter causado a perda total dos fundos do Uniswap V1. 

Balancer

O Balancer V2 também é um AMM que foi verificado formalmente. A verificação formal encontrou e corrigiu um erro no cálculo da taxa de uma funcionalidade de empréstimo (flash loan) no contrato inteligente, o que poderia deixar a corretora vulnerável a roubos.

SafeMoon

O SafeMoon V1 continha um sutil bug que foi encontrado por verifica√ß√£o formal ap√≥s a sua implanta√ß√£o. Atrav√©s desse bug, era poss√≠vel que um propriet√°rio renunciasse √† propriedade do contrato para depois readquiri-lo, caso certas opera√ß√Ķes fossem feitas antes da renuncia.

Este bug n√£o foi notado na maioria das auditorias manuais de forks do SafeMoon V1, pois encontr√°-lo exigia a an√°lise de combina√ß√Ķes espec√≠ficas de valores das vari√°veis do programa. Esse tipo de problema costuma ser algo dif√≠cil para um humano detectar, por√©m facilmente identificado por uma m√°quina.

Como a verificação formal e a auditoria manual funcionam juntas

A verifica√ß√£o formal fornece uma maneira sistem√°tica e automatizada de verificar a l√≥gica e o comportamento de um contrato em rela√ß√£o √†s suas propriedades desejadas. Isso facilita a identifica√ß√£o e corre√ß√£o de poss√≠veis erros ou bugs. √Č um processo especialmente √ļtil para encontrar problemas complexos e sutis que podem ser dif√≠ceis de detectar por meio de inspe√ß√£o manual.

A auditoria manual envolve a revisão especializada do código, design e implantação de um contrato. O auditor usa sua experiência e conhecimento para identificar riscos de segurança e avaliar o comportamento geral de segurança do contrato. Eles também podem confirmar se o processo de verificação formal foi executado corretamente e checar quaisquer problemas possivelmente não detectados por ferramentas automatizadas. 

A combinação da verificação formal e da auditoria manual fornece uma avaliação abrangente e completa da segurança de um contrato inteligente. Isso aumenta as chances de encontrar e corrigir quaisquer vulnerabilidades. O resultado é uma abordagem aprofundada de defesa que se beneficia dos recursos de máquinas e das capacidades exclusivas de humanos. 

Considera√ß√Ķes finais

Para garantir a segurança dos contratos inteligentes, é essencial usar a verificação formal e a auditoria manual, que oferecem uma avaliação abrangente e completa do comportamento e segurança de um contrato inteligente.

Embora a verificação formal possa consumir muitos recursos, é um investimento que vale a pena para contratos com alto valor ou que incluem fatores de alto risco. Afinal, é fundamental priorizar a segurança e garantir que os contratos inteligentes estejam livres de bugs, vulnerabilidades e comportamentos indesejados.

Leituras adicionais

Aviso de Risco e Isen√ß√£o de Responsabilidade: este conte√ļdo √© apresentado a voc√™ ‚Äúno estado em que se encontra‚Äú apenas para fins informativos e educacionais, sem qualquer tipo de garantia. O conte√ļdo n√£o deve ser interpretado como aconselhamento financeiro e n√£o tem o objetivo de recomendar a compra de qualquer produto ou servi√ßo espec√≠fico. Os pre√ßos dos ativos digitais podem ser vol√°teis. O valor do seu investimento pode aumentar ou diminuir e √© poss√≠vel que voc√™ n√£o recupere o valor investido. Voc√™ √© o √ļnico respons√°vel por suas decis√Ķes de investimento e a Binance Academy n√£o se responsabiliza por nenhuma de suas poss√≠veis perdas. Este material n√£o deve ser interpretado como um aconselhamento financeiro.