Este artigo é um envio da comunidade. O autor é David Tarditi, vice-presidente de engenharia da CertiK, uma empresa de auditoria de contratos inteligentes da Web3.
As opiniões neste artigo são do colaborador/autor e não refletem necessariamente as da Binance Academy.
DR
A verificação formal de contratos inteligentes garante que eles estejam livres de bugs, vulnerabilidades e outros comportamentos não intencionais. Envolve um especialista humano apresentando a lógica do contrato inteligente como declarações matemáticas e, em seguida, executando-as através de um processo automatizado que verifica a lógica real em relação aos modelos do comportamento esperado do contrato. A combinação de verificação formal e 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 um blockchain que são executados automaticamente quando determinadas condições são atendidas. Eles podem variar de simples a extremamente complexos e podem deter ativos no valor de milhões ou até bilhões de dólares.
As vulnerabilidades de segurança no código do contrato inteligente podem ter consequências devastadoras, incluindo o roubo de todos os ativos mantidos por um contrato inteligente. Em 2021, o formador de mercado automatizado (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 US$ 80 milhões em recompensas não merecidas devido a um erro de um único caractere. Em 2022, US$ 320 milhões foram roubados da ponte Wormhole devido a um bug em um de seus contratos inteligentes.
É importante acertar o programa de contrato inteligente na primeira vez. Os contratos inteligentes são de código aberto, o que significa que o código fica disponível publicamente assim que o contrato é implantado. Se um hacker encontrar um bug, ele poderá tirar vantagem dele imediatamente. Além disso, corrigir vulnerabilidades de segurança ao longo do tempo não é uma opção, já que o código de um contrato inteligente normalmente não pode ser modificado após a implantação.
Como funciona a verificação de contrato inteligente?
A verificação formal de contratos inteligentes funciona apresentando a lógica e o comportamento desejado dos contratos inteligentes como declarações matemáticas. Os auditores usam então 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 lógicos.
Usando provadores automatizados de teoremas ou verificadores de modelos 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 inteligente de contrato é importante
O uso do raciocínio matemático ajuda a garantir que os contratos inteligentes verificados formalmente estejam livres de bugs, vulnerabilidades e outros comportamentos não intencionais. Também ajuda a aumentar a confiança no contrato, uma vez que as suas propriedades foram rigorosamente comprovadas como corretas.
Abaixo estão alguns exemplos de como a verificação inteligente de contratos ajudou a prevenir perdas financeiras significativas e outros resultados desastrosos.
Uniswap
Uniswap é um AMM bem 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 levado à drenagem de fundos do Uniswap V1.
Balanceador
O Balancer V2 também é um AMM que foi formalmente verificado. A verificação formal encontrou e corrigiu um cálculo incorreto de taxas envolvendo a funcionalidade de empréstimo instantâneo no contrato inteligente, o que poderia ter tornado a exchange vulnerável a roubo.
Lua Segura
O SafeMoon V1 continha um bug sutil encontrado por verificação formal após sua implantação. Era possível ao proprietário renunciar à propriedade do contrato e depois readquiri-lo, se certas operações fossem realizadas antes da renúncia à propriedade.
Este bug foi perdido na maioria das auditorias manuais de garfos SafeMoon V1 porque encontrá-lo exigiu a análise de combinações específicas de valores de variáveis do programa. Isso é algo fácil de ser ignorado pelos humanos e fácil de ser percebido 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 propriedades desejadas. Isso torna mais fácil identificar e corrigir possíveis erros ou bugs. É especialmente útil para encontrar problemas complexos e sutis que podem ser difíceis de detectar através da inspeção manual.
A auditoria manual envolve a revisão especializada do código, design e implantação de um contrato. O auditor utiliza sua experiência e conhecimento para identificar riscos de segurança e avaliar a postura geral de segurança do contrato. Eles também podem confirmar se o processo de verificação formal foi executado corretamente e verificar quaisquer problemas que possam não ser detectáveis por ferramentas automatizadas.
A combinação de verificação formal e 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 de defesa profunda à segurança que aproveita as capacidades únicas de humanos e máquinas.
Considerações finais
Para garantir a segurança dos contratos inteligentes, é essencial utilizar tanto a verificação formal como a auditoria manual para garantir uma avaliação abrangente e completa da postura de segurança de um contrato inteligente.
Embora a verificação formal possa consumir muitos recursos, é um investimento que vale a pena para contratos com factores de elevado valor ou de alto risco. Em última análise, é vital priorizar a segurança e garantir que os contratos inteligentes estejam livres de bugs, vulnerabilidades e comportamentos não intencionais.
Leitura adicional
O que são contratos inteligentes?
O que é uma auditoria de segurança de contrato inteligente?
Isenção de responsabilidade e aviso de risco: Este conteúdo é apresentado a você “como está” apenas para fins informativos gerais e educacionais, sem representação ou garantia de qualquer tipo. Não deve ser interpretado como aconselhamento financeiro, jurídico ou outro aconselhamento profissional, nem tem a intenção de recomendar a compra de qualquer produto ou serviço específico. Você deve procurar aconselhamento de consultores profissionais apropriados. Quando o artigo for contribuído por um contribuidor terceirizado, observe que as opiniões expressas pertencem ao contribuidor terceirizado e não refletem necessariamente as da Binance Academy. Por favor, leia nosso aviso completo aqui para obter mais detalhes. Os preços dos ativos digitais podem ser voláteis. O valor do seu investimento pode diminuir ou aumentar e você pode não recuperar o valor investido. Você é o único responsável por suas decisões de investimento e a Binance Academy não se responsabiliza por quaisquer perdas que você possa incorrer. Este material não deve ser interpretado como aconselhamento financeiro, jurídico ou outro aconselhamento profissional. Para obter mais informações, consulte nossos Termos de Uso e Aviso de Risco.
