Este artigo é uma contribuição da comunidade. Autor: Dimitris Tsapis, vice-presidente de engenharia da CertiK, uma empresa de auditoria de contratos inteligentes web3.
DR
A verificação formal garante que os contratos inteligentes estejam livres de bugs, vulnerabilidades e outros comportamentos não intencionais. O processo envolve um especialista humano exibindo a lógica do contrato inteligente na forma de dados matemáticos e, em seguida, executando-o através de um processo de verificação automática da 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 dos contratos inteligentes.
a 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 variam de programas simples a complexos e podem conter ativos no valor de 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 detidos pelo contrato inteligente. Durante 2021, o criador de mercado automatizado Uranium Finance teve um roubo de US$ 50 milhões devido a um único erro de digitação em um contrato inteligente.
Também durante 2021, o protocolo Compound Finance entregou US$ 80 milhões em recompensas não ganhas como resultado de um erro de token único. Durante 2022, US$ 320 milhões foram roubados da Wormhole Bridge como resultado de um erro de programação em um de seus contratos inteligentes.
É importante acertar o software de contrato inteligente na primeira vez. Os contratos inteligentes são contratos de código aberto, o que significa que o código está disponível ao público assim que o contrato é publicado. Se um hacker encontrar um bug, ele poderá explorá-lo imediatamente. Além disso, lidar com vulnerabilidades de segurança ao longo do tempo não é uma opção, já que o código do contrato inteligente normalmente não pode ser modificado após ser implantado.
Como funciona a verificação de contrato inteligente?
A verificação formal de contratos inteligentes funciona expondo a lógica e o comportamento necessários dos contratos inteligentes na forma de dados computacionais. Os auditores podem usar ferramentas automatizadas para validar dados.
O processo inclui o seguinte:
Especificar as especificações e características desejadas do contrato no idioma oficial.
Traduzir o código do contrato em uma apresentação formal, como modelos ou estruturas lógicas matemáticas.
Uso de ferramentas de prova de teoremas ou verificação de modelos para auditar especificações e propriedades de contratos.
Repita o processo de verificação para encontrar e corrigir quaisquer erros ou desvios das características exigidas.
Por que a verificação inteligente de contratos é 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 cuidadosamente verificadas.
Aqui estão alguns exemplos de como a verificação inteligente de contratos pode ajudar a prevenir perdas financeiras significativas e outras consequências terríveis.
Uniswap
Uniswap é um conhecido criador de mercado automatizado. Quando o contrato inteligente Uniswap V1 foi desenvolvido, ele foi oficialmente verificado. Antes do seu lançamento, este processo de verificação oficial foi capaz de encontrar e corrigir erros de arredondamento que teriam levado ao roubo de fundos do Uniswap V1.
Balanceador
Balancer V2 também é um criador de mercado automatizado verificado oficialmente. O processo de verificação oficial foi capaz de encontrar e corrigir contas de taxas incorretas e incluiu uma função de empréstimo instantâneo no contrato inteligente, o que poderia colocar a plataforma de negociação em risco de roubo.
Lua Segura
SafeMoon V1 incluiu um bug despercebido que foi encontrado por meio de verificação oficial após sua publicação. Era possível ao proprietário renunciar à propriedade do contrato e readquiri-lo novamente, se certas operações fossem realizadas antes da renúncia da propriedade.
O erro passa despercebido durante a maioria das auditorias manuais dos garfos SafeMoon V1 porque encontrá-lo requer a análise de conjuntos específicos de valores de variáveis do programa. Isso é algo fácil de ser ignorado pelos humanos, mas fácil de ser encontrado pelas máquinas.
Como a verificação formal e a auditoria manual funcionam juntas
A verificação formal fornece uma maneira sistemática e automática 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 despercebidos que podem ser difíceis de detectar durante uma verificação manual.
O processo de auditoria manual envolve a revisão especializada do código e design do contrato, bem como a sua publicação. O auditor utiliza sua experiência para identificar riscos de segurança e avaliar o status de segurança do contrato em geral. Também confirma que o processo de verificação formal foi concluído corretamente e verifica quaisquer problemas que possam não ser detectados por ferramentas automatizadas.
A combinação de verificação formal e auditoria manual fornece uma avaliação abrangente da segurança dos contratos inteligentes. Isso aumenta a probabilidade de encontrar e corrigir quaisquer vulnerabilidades. O resultado é uma abordagem defensiva à segurança que aproveita as capacidades únicas de humanos e máquinas.
Pensamentos finais
Para garantir a segurança dos contratos inteligentes, é necessário utilizar tanto um processo de verificação formal como uma auditoria manual para garantir uma avaliação abrangente e precisa do estado de segurança do contrato inteligente.
Embora a verificação formal possa consumir muitos recursos, é um investimento que vale a pena para contratos inteligentes de alto valor ou de alto risco. Por fim, é importante priorizar a segurança e garantir que os contratos inteligentes estejam livres de bugs, vulnerabilidades e outros comportamentos não intencionais.
Artigos relacionados
O que é um contrato inteligente?
O que é uma auditoria de segurança para contratos inteligentes?
Isenção de responsabilidade e aviso de risco: este conteúdo é fornecido a você “como está” apenas para fins informativos e educacionais gerais, sem quaisquer representações ou garantias 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 podem ser voláteis. O valor do seu investimento pode aumentar ou diminuir e você pode não receber de volta o valor investido. Você é o único responsável por suas decisões de investimento e a Binance Academy não é responsável por quaisquer perdas que você possa incorrer. Este não é um conselho financeiro.