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:
Definir as especificações e propriedades desejadas de um contrato em linguagem formal.
Traduzir o código do contrato em uma representação formal, como modelos matemáticos ou uma representação lógica.
Usar provadores de teoremas automatizados ou verificadores de modelo para validar as especificações e propriedades do contrato.
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.