Este artigo é uma contribuição da comunidade. O autor é David Tarditi, vice-presidente de engenharia da Certik, uma empresa de auditoria de contratos inteligentes da Web3.
Resumo
A verificação formal de contratos inteligentes garante que eles estejam livres de bugs, vulnerabilidades e outros comportamentos indesejados. É realizado por 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 em relação aos modelos de comportamento esperados do contrato inteligente. 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 certas condições são atendidas. Eles podem variar de simples a extremamente complexos e podem conter ativos avaliados em milhões ou até bilhões de dólares.
Vulnerabilidades de segurança no código de contratos inteligentes podem ter consequências sérias, incluindo o roubo de todos os ativos do contrato inteligente. Em 2021, o Automated Market Maker (AMM) Uranium Finance sofreu um roubo de US$ 50 milhões devido a um 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 apenas pelo personagem errado. Em 2022, US$ 320 milhões foram roubados da Wormhole Bridge devido a um bug em um de seus contratos inteligentes.
É importante acertar seu software de contrato inteligente desde o início. Os contratos inteligentes são de código aberto, o que significa que, uma vez implantado o contrato, o código fica disponível ao público. Se um hacker encontrar um bug, ele pode explorá-lo imediatamente. Além disso, corrigir vulnerabilidades de segurança não é uma opção sustentável, pois o código do contrato normalmente não pode ser modificado após sua implantação.
Como funciona a verificação de contratos inteligentes?
A verificação formal de contratos inteligentes é feita apresentando a lógica e o comportamento desejado dos contratos como declarações matemáticas. Os auditores então usam ferramentas automatizadas para verificar se as declarações estão corretas.
O processo envolve:
Defina as especificações e propriedades desejadas de um contrato em linguagem formal.
Traduza o código do contrato inteligente em uma representação formal, como modelos matemáticos e lógica.
Use provadores de teoremas automatizados ou verificadores de modelos para validar especificações e propriedades de contratos.
Repita 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
Usar o raciocínio matemático ajuda a garantir que contratos formalmente verificados estejam livres de bugs, vulnerabilidades e outros comportamentos indesejáveis. Também ajuda a aumentar a confiança no contrato, pois suas propriedades foram rigorosamente comprovadas como corretas.
Abaixo estão alguns exemplos de como a verificação de contratos inteligentes ajudou a evitar perdas financeiras significativas e outros resultados sérios.
Uniswap
Uniswap é um AMM bem conhecido. Quando a primeira versão do contrato inteligente Uniswap foi desenvolvida, ela foi formalmente verificada. Antes do lançamento, esta verificação formal encontrou e corrigiu erros de arredondamento que podem ter levado à perda de fundos do Uniswap V1.
Balanceador
O Balancer V2 também é conhecido como um AMM que foi formalmente verificado. A verificação formal encontrou e corrigiu um cálculo de taxa incorreto relacionado à funcionalidade de empréstimo rápido no contrato inteligente, o que poderia ter deixado a bolsa vulnerável a roubo.
Lua Segura
O SafeMoon V1 continha um bug sutil que foi descoberto na verificação formal após a implantação do contrato. Se certas transações fossem feitas antes da renúncia à propriedade do contrato, era possível que o proprietário do contrato renunciasse à propriedade e depois a readquirisse.
Esse bug passou despercebido na maioria das auditorias manuais de bifurcações do SafeMoon V1 porque encontrá-lo exigia a análise de combinações específicas de valores de variáveis do programa. Isso é algo que escapa facilmente ao controle humano, mas é facilmente descoberto 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, facilitando a identificação e a correção de possíveis erros e bugs. É especialmente útil para encontrar problemas complexos e sutis que podem passar despercebidos pela inspeção manual.
A auditoria manual envolve revisão especializada de código, design de contrato e implementação. O auditor usa sua experiência e habilidade para identificar riscos de segurança e avaliar a postura geral de segurança do contrato. Você também pode confirmar se o processo de verificação formal foi concluído corretamente, bem como revisar quaisquer problemas que não sejam 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 do contrato inteligente, aumentando a probabilidade de encontrar e corrigir quaisquer vulnerabilidades que ele possa conter. O resultado é uma abordagem de defesa em profundidade para segurança que aproveita as capacidades únicas de humanos e máquinas.
Conclusões
Para garantir a segurança dos contratos inteligentes, é essencial seguir uma verificação formal e uma auditoria manual, garantindo assim uma avaliação abrangente e completa da postura de segurança do contrato inteligente.
Embora a verificação formal possa exigir muitos recursos, vale a pena o investimento para contratos com fatores de alto valor ou alto risco. Por fim, é essencial priorizar a segurança e garantir que os contratos inteligentes estejam livres de bugs, vulnerabilidades e comportamentos indesejados.
Leitura adicional
O que são contratos inteligentes?
O que é uma auditoria de segurança de contrato inteligente?
Aviso de isenção de responsabilidade e risco: este conteúdo é fornecido "como está" apenas para fins informativos e educacionais gerais, sem representação ou garantia de qualquer tipo. Não deve ser interpretado como aconselhamento financeiro, nem tem a intenção de recomendar a compra de qualquer produto ou serviço específico. Os preços dos ativos digitais são voláteis. O valor de um investimento pode aumentar ou diminuir, e você pode não recuperar o valor investido. Você é o único responsável por suas decisões de investimento. A Binance Academy não se responsabiliza por nenhuma perda que você possa sofrer. Este material não deve ser interpretado como aconselhamento financeiro.