Este artigo foi postado por um membro 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 protege-os contra erros, vulnerabilidades e outras condições adversas. Neste processo, especialistas humanos convertem a lógica do contrato inteligente em declarações matemáticas e, em seguida, utilizam um processo automatizado para verificar a lógica real em relação a um modelo do comportamento esperado do contrato. Combinando verificação formal e auditoria manual, podemos realizar uma avaliação abrangente da segurança dos contratos inteligentes.
Introdução
Contratos inteligentes são programas de computador implantados no blockchain que são executados automaticamente quando certas condições são atendidas. Os contratos inteligentes podem ser muito simples ou extremamente complexos e podem conter ativos no valor de milhões ou mesmo milhares de milhões de dólares.
Se existirem falhas de segurança no código do contrato inteligente, isso poderá ter consequências devastadoras, como o roubo de todos os bens detidos por criminosos. Em 2021, US$ 50 milhões foram roubados do formador de mercado automatizado (AMM) Uranium Finance devido a um erro de digitação em um contrato inteligente.
Também em 2021, a Compound Finance emitiu por engano US$ 80 milhões em recompensas devido a um único erro de codificação. Em 2022, US$ 320 milhões foram roubados da Wormhole Bridge devido a um erro no contrato inteligente.
Portanto, é importante definir seu programa de contrato inteligente desde o início. Os contratos inteligentes adotam um modelo de código aberto, o que significa que, uma vez implantado o contrato, o código se torna público. Se um hacker descobrir um bug, ele poderá explorá-lo imediatamente. Além disso, a prática normal de corrigir vulnerabilidades de segurança ao longo do tempo é ineficaz porque o código dos contratos inteligentes muitas vezes não pode ser modificado após a implantação.
Como funciona a verificação de contrato inteligente?
A verificação formal dos contratos inteligentes é obtida apresentando a lógica e o comportamento esperado do contrato inteligente como declarações matemáticas. Os auditores utilizam então ferramentas automatizadas para verificar se essas declarações estão corretas.
O processo envolve:
Definir as especificações e características esperadas do contrato em linguagem formal.
Converta o código de um contrato em uma declaração formal, como um modelo matemático ou lógico.
Verifique as especificações e propriedades do contrato usando prova automatizada de teoremas ou verificação de modelo.
Repita o processo de validação para encontrar e corrigir quaisquer erros ou desvios das características esperadas.
Por que a verificação inteligente de contratos é importante
Ao aplicar o raciocínio matemático, ajuda a garantir que os contratos inteligentes verificados formalmente estão livres de erros, vulnerabilidades e outras situações adversas. A verificação também ajuda a aumentar a confiança no contrato porque suas propriedades foram rigorosamente testadas e são corretas e confiáveis.
Os exemplos abaixo descrevem como a verificação inteligente de contratos pode ajudar a prevenir perdas financeiras significativas e outras consequências catastróficas.
Uniswap
Uniswap é um AMM bem conhecido. O contrato inteligente Uniswap V1 passou por verificação formal durante o processo de desenvolvimento. Antes do lançamento, esta verificação formal encontrou e corrigiu alguns erros de arredondamento, evitando que os fundos do Uniswap V1 fossem drenados.
Balanceador
Balancer V2 também é um AMM comprovado. A verificação formal descobriu e corrigiu um erro de cálculo de taxa no recurso de empréstimo instantâneo do contrato inteligente que deixou a plataforma de negociação vulnerável a roubo.
Lua Segura
Após a implantação do SafeMoon V1, um erro muito pequeno foi descoberto por meio de verificação formal. Se o erro não for descoberto, se o proprietário do contrato realizar certas operações antes de desistir da propriedade, o proprietário do contrato poderá recuperá-lo após desistir do contrato.
A maioria das auditorias manuais do fork SafeMoon V1 não percebe esse bug porque combinações específicas de valores de variáveis do programa precisam ser analisadas para encontrá-lo. Os humanos podem facilmente ignorar esse problema, mas as máquinas podem detectá-lo a tempo.
Como a verificação formal e a auditoria manual funcionam juntas
A verificação formal fornece uma forma sistemática e automatizada de verificar a lógica e o comportamento de um contrato em relação às suas características esperadas. Isso torna mais fácil identificar e corrigir possíveis bugs ou vulnerabilidades. Isto é particularmente útil para problemas complexos e sutis que seriam difíceis de detectar através da inspeção manual.
A auditoria manual envolve especialistas que revisam o código, o design e a implantação do contrato. Os auditores utilizam a sua experiência e conhecimentos 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 as ferramentas automatizadas possam não detectar.
Combinando verificação formal e auditoria manual, podemos realizar uma avaliação abrangente da segurança dos contratos inteligentes. Isso aumenta as chances de encontrar e corrigir quaisquer vulnerabilidades. Ao fazê-lo, estamos a adotar uma abordagem de segurança de defesa profunda que combina a experiência de humanos e máquinas.
Conclusão
Para garantir a segurança dos contratos inteligentes, a verificação formal e a auditoria manual devem ser combinadas para garantir uma avaliação abrangente e completa da postura de segurança dos contratos inteligentes.
Embora a verificação formal exija mais recursos, é um investimento que vale a pena para contratos com elevado valor ou factores de risco elevados. Afinal, no final das contas, a segurança é mais importante do que qualquer outra coisa. Certifique-se de priorizar a segurança e garantir que os contratos inteligentes estejam livres de bugs, vulnerabilidades e comportamentos inesperados indesejáveis.
Leitura adicional
O que é um contrato inteligente?
O que é auditoria de segurança de contrato inteligente?
Isenção de responsabilidade e aviso de risco: O conteúdo deste artigo são fatos e destinam-se apenas a informações gerais e fins educacionais e não constituem qualquer representação ou garantia. Este artigo não deve ser interpretado como um conselho financeiro e não recomenda que você compre qualquer produto ou serviço específico. Os preços dos ativos digitais podem flutuar. O valor do seu investimento pode cair ou subir e você pode não recuperar o principal investido. Você é o único responsável por suas próprias decisões de investimento e a Binance Academy não é responsável por quaisquer perdas que você possa sofrer. Este material não constitui aconselhamento financeiro.
