Introdução

À medida que o valor dos ativos na blockchain cresce rapidamente com vários projetos lançando diferentes casos de uso na economia cripto, ficar à frente de possíveis brechas e ameaças é mais imperativo do que nunca.

O Bitcoin foi inventado para substituir bancos, mas a tecnologia subjacente, blockchain, provou que poderia substituir quase qualquer intermediário. Seguindo em frente, isso não parou por aí, vendo o enorme potencial que a moeda digital possuía, o que o dinheiro em papel nunca poderia ter, e isso envolve a habilidade de programar dinheiro. De repente, advogados e contratos poderiam ser substituídos em transações financeiras. Esta forma de moeda digital avançou a descentralização, permitindo a execução automática de contratos com total transparência e sem intervenção humana. No entanto, como exatamente funcionam os contratos inteligentes? É realmente confiável confiar nesses sistemas que não possuem confiança?

Neste artigo, vamos explorar as extensas questões sobre a verificação formal de contratos inteligentes, discutindo seus prós, contras, impacto no ecossistema cripto e muito mais, com ênfase no Ethereum.

Breve História dos Contratos Inteligentes

Origem: CryptoSlate

Nick Szabo, um cientista da computação e criptógrafo americano frequentemente especulado como Satoshi Nakamoto, foi o pioneiro dos contratos inteligentes, apresentando o conceito pela primeira vez em 1994. Szabo descreveu os contratos inteligentes como protocolos de transação digital projetados para aplicar automaticamente os termos de um acordo. Seu objetivo era aprimorar os métodos de transação eletrônica, como sistemas de ponto de venda, e expandir suas capacidades para o mundo digital.

Szabo vislumbrou um futuro onde os acordos poderiam funcionar como máquinas de venda automática - automatizados, confiáveis e à prova de adulteração. Embora a tecnologia de sua época não fosse avançada o suficiente para realizar plenamente sua visão, as ideias de Szabo lançaram as bases para o que mais tarde revolucionaria a indústria blockchain. Quando Ethereum lançouem 2015, trouxe os contratos inteligentes para uso prático, transformando os conceitos teóricos de Szabo em componentes essenciais das aplicações descentralizadas.

A sua visão era a de contratos que pudessem gerir relações com termos precisos e automatizados, reduzindo a necessidade de intervenção humana e supervisão. Esta abordagem visava criar uma forma mais segura e eficiente de lidar com acordos, abrindo caminho para a evolução dos contratos inteligentes em poderosas ferramentas no ecossistema de blockchain. As perspicácias iniciais de Szabo continuam a moldar o panorama das transações digitais e do desenvolvimento de contratos inteligentes hoje em dia.

O que é Verificação formal?

Origem: Médio

A verificação formal é o processo de avaliar rigorosamente se um sistema, como um contrato inteligente, opera de acordo com um conjunto definido de regras ou especificações. Em essência, verifica se o sistema se comporta como esperado, garantindo que atenda às condições exigidas e execute as funções pretendidas sem erros.

Para alcançar isso, os comportamentos esperados do sistema são delineados usando modelos formais, enquanto linguagens de especificação são usadas para definir as propriedades exatas que o contrato deve satisfazer e veremos mais cenários práticos à medida que o artigo avança. As técnicas de verificação formal então correspondem à implementação do contrato às suas especificações, fornecendo prova matemática de sua correção. Quando um contrato atende a essas especificações, ele é considerado 'funcionalmente correto' ou 'correto por design', confirmando sua confiabilidade e segurança no ambiente blockchain.

Tipos de Especificações Formais para Contratos Inteligentes

Origem: Ever Scale

Especificações formais fornecem uma maneira estruturada de usar raciocínio matemático para verificar a precisão da execução de um programa. Essas especificações podem descrever propriedades de alto nível, que se concentram no comportamento geral, ou detalhes de baixo nível de como um contrato opera internamente. Ao definir esses comportamentos matematicamente, as especificações formais garantem que o contrato funcione conforme o pretendido.

Especificações de alto nível

As especificações de alto nível, também conhecidas como especificações orientadas a modelos, descrevem o comportamento geral de um contrato inteligente, tratando-o como uma máquina de estados finitos (FSM) que transita entre diferentes estados por meio de operações específicas. A lógica temporal é frequentemente usada para definir as regras formais que governam essas transições, detalhando como o contrato se move entre os estados ao longo do tempo e as condições que deve cumprir para fazê-lo corretamente.

Essas especificações capturam duas propriedades essenciais: segurança e vitalidade. A segurança garante que eventos indesejáveis não ocorram, como evitar que o saldo do remetente caia abaixo do valor necessário para uma transação. A vitalidade, por outro lado, garante que o contrato continue a funcionar e progredir, como manter a liquidez para que os usuários possam retirar fundos quando solicitado. Ambas as propriedades garantem que os contratos inteligentes operem de forma segura e confiável, protegendo as interações e ativos dos usuários.

Especificações de baixo nível

As especificações de baixo nível, também conhecidas como especificações orientadas a propriedades, concentram-se em definir o comportamento correto dos contratos inteligentes analisando seus processos de execução internos. Ao contrário das especificações de alto nível que modelam os contratos como máquinas de estados finitos, as especificações de baixo nível visualizam os contratos inteligentes como sistemas de funções matemáticas e examinam as sequências de execução de funções, conhecidas como traces, que alteram o estado do contrato.

Técnicas para Verificação Formal de Contratos Inteligentes

Origem: Ever Scale

Verificação de modelos

A verificação de modelo é um método de verificação formal que usa algoritmos para avaliar se o modelo de um contrato inteligente está alinhado com suas especificações. Contratos inteligentes são tipicamente representados como sistemas de transição de estado, e suas propriedades são definidas usando temporal.lógica. Este processo envolve a criação de um modelo matemático do contrato e expressando suas propriedades através de fórmulas lógicas, permitindo que o algoritmo verifique se o modelo atende a essas especificações.

Demonstração de Teorema

Ao contrário da verificação de modelos, a prova de teoremas é uma abordagem matemática usada para estabelecer a correção de programas, incluindo contratos inteligentes. Este método envolve a conversão do modelo e das especificações de um contrato em fórmulas lógicas para verificar sua equivalência lógica, ou seja, uma declaração é verdadeira se a outra for verdadeira. Formulando essa relação como um teorema, um provador automático de teoremas pode validar a correção do modelo de contrato em relação às suas especificações.

Em contraste com a verificação de modelos, que é limitada a sistemas de estados finitos, a prova de teoremas pode analisar sistemas de estados infinitos, mas muitas vezes requer orientação humana para lidar com problemas lógicos complexos. Consequentemente, a prova de teoremas tende a ser mais intensiva em recursos do que o processo de verificação de modelos totalmente automatizado.

Execução Simbólica

A execução simbólica é um método de análise poderoso para contratos inteligentes que envolve a execução de funções com valores simbólicos em vez de entradas específicas. Esta técnica de verificação formal permite a análise de propriedades ao nível do traço no código de um contrato, representando os caminhos de execução como fórmulas matemáticas, conhecidas como predicados de caminho. Um solucionador SMT é então utilizado para determinar se estes predicados são satisfatórios, ou seja, se existe uma entrada que satisfaça as condições.

Por exemplo, se uma função de contrato reverter quando um valor estiver entre 5 e 10, a execução simbólica pode identificar eficientemente tais valores desencadeantes avaliando a condição como X > 5 ∧ X < 10. Este método é frequentemente mais eficaz do que os testes tradicionais, produzindo menos falsos positivos e gerando diretamente valores concretos que reproduzem qualquer solver SMT empregado para determinar erros encontrados, tornando-a assim uma ferramenta valiosa para garantir a confiabilidade dos contratos inteligentes.

O que são contratos inteligentes?

Fonte: Ternamente

Os contratos inteligentes são programas de computador automatizados que operam em uma blockchain, executando ações quando condições específicas são cumpridas. Eles podem variar de acordos simples a processos altamente complexos e podem gerenciar ativos avaliados em milhões ou até bilhões de dólares.

Embora os contratos inteligentes tenham o potencial de revolucionar vários setores, como votação política, gestão da cadeia de abastecimento, cuidados de saúde e imobiliário, este artigo mantém o foco no impacto deles no campo das criptomoedas. O design deles permite que várias partes colaborem sem o risco de manipulação, oferecendo um quadro transparente e seguro que melhora a eficiência e a inovação. No entanto, é importante reconhecer que os contratos inteligentes também têm vulnerabilidades e desafios.

Vulnerabilidades com Contratos Inteligentes

Vulnerabilidades de segurançaem código de contrato inteligente pode levar a resultados catastróficos, como a perda total de ativos armazenados dentro do contrato, como demonstrado por incidentes recentes.

• Em 2021, o criador de mercado automatizado Uranium Finance sofreu um roubo de $50 milhõesdevido a um simples erro de digitação em seu contrato inteligente.
• Também em 2021, Compound Finance distribuiu inadvertidamente $ 80 milhõesem recompensas não ganhas, novamente por causa de um erro de um único caractere.
• Ocorreu uma violação mais significativa em 2022quando $320 milhões foram roubados da Ponte Wormholedevido a um bug em um de seus contratos inteligentes.

Dado estes exemplos, é crucial garantir que os contratos inteligentes sejam codificados com precisão desde o início. Uma vez implantados, os contratos inteligentes são de código aberto, o que significa que o seu código é publicamente acessível, tornando fácil para os hackers explorar quaisquer vulnerabilidades descobertas. Além disso, a natureza imutável dos contratos inteligentes significa que, uma vez lançados, o seu código normalmente não pode ser alterado para corrigir falhas de segurança, deixando-os perpetuamente em risco se não forem desenvolvidos com a máxima precisão.

Como Funciona a Verificação de Contratos Inteligentes?

Fonte: Certik

O processo inclui:

• Definindo as especificações e propriedades desejadas do contrato usando linguagem formal.
• Traduzir o código do contrato para uma representação formal, como modelos matemáticos ou expressões lógicas.
• Provadores de teoremas automatizados ou verificadores de modelos são empregados para confirmar a validade das especificações e propriedades do contrato.
• Repetir iterativamente o processo de verificação para identificar e corrigir erros ou desvios das propriedades pretendidas.

Principais características dos contratos inteligentes

Origem: Certik

Pense nos contratos inteligentes como acordos gravados em pedra - uma vez criados, não podem ser alterados. Operando no livro-razão imutável de uma blockchain, esses contratos aplicam automaticamente os termos sem a necessidade de intermediários, o que acelera as transações e diminui os custos. Essa natureza fixa aumenta a segurança e descentraliza o controle, reduzindo significativamente as chances de fraude e corrupção.

Porque a Verificação de Contratos Inteligentes é Importante

O raciocínio matemático desempenha um papel crucial em garantir que os contratos inteligentes verificados formalmente estejam livres de bugs, vulnerabilidades e comportamentos inesperados. Este processo rigoroso aumenta a confiança no contrato, uma vez que as suas propriedades foram minuciosamente validadas.

Exemplos bem-sucedidos de verificação de contratos inteligentes destacam a sua importância na prevenção de perdas financeiras significativas.

Uniswap

Por exemplo, Uniswap, um conhecido criador de mercado automatizado (AMM), passou por verificação formal durante o desenvolvimento do seu contrato inteligente V1, que identificou e corrigiu erros de arredondamentoque poderia ter drenado fundos.

Balancer

Da mesma forma, o Balancer V2, outro AMM, beneficiou-se da verificação formal que descobriuum cálculo incorreto de taxarelacionado com empréstimos flash, prevenindo potenciais roubos.

SafeMoon

SafeMoon V1 teve um pequeno bugidentificado através de verificação formal após a implantação. Esse bug permitia que o proprietário renunciasse à propriedade e a recuperasse em certas condições, um detalhe que a maioria das auditorias manuais não percebeu devido à sua complexidade. A capacidade de verificação formal de analisar combinações específicas de valores de variáveis a torna uma ferramenta eficaz para detectar problemas que os auditores humanos podem negligenciar.

Como a Verificação Formal e a Auditoria Manual Funcionam Juntas

A verificação formal oferece um método sistemático e automatizado para verificar a lógica e o comportamento de um contrato inteligente em relação às suas propriedades pretendidas. Esta abordagem simplifica a identificação e correção de erros ou bugs potenciais, especialmente questões complexas que inspeções manuais podem ignorar.

Por outro lado, a auditoria manual envolve uma revisão minuciosa do código, design e implementação do contrato por um especialista. O auditor utiliza a sua experiência para identificar os riscos de segurança e avaliar a postura geral de segurança do contrato. Eles também podem validar a correção do processo de verificação formal e identificar problemas que as ferramentas automatizadas possam perder. A combinação da verificação formal com a auditoria manual cria uma avaliação abrangente da segurança, aumentando a probabilidade de descobrir e resolver vulnerabilidades, e estabelecendo uma estratégia de defesa robusta que aproveita as vantagens tanto da expertise humana quanto da análise automatizada.

Prós e contras dos contratos inteligentes

Origem: Blockonomi

Os contratos inteligentes não são perfeitos, mas as suas vantagens superam significativamente as desvantagens. Simplificam transações complexas, poupando tempo e dinheiro, promovendo transparência e reduzindo disputas. Uma vez que operam com código, minimizam erros humanos. A sua segurança é robusta, graças a proteções criptográficas. No entanto, os contratos inteligentes podem ser inflexíveis e ter dificuldade em adaptar-se a situações inesperadas. Além disso, a configuração requer competências de codificação especializadas, o que pode ser uma barreira para alguns. Apesar destes desafios, os contratos inteligentes estão a transformar indústrias.

Vantagens dos Contratos Inteligentes

• Melhorar a eficiência automatizando tarefas, poupando tempo e dinheiro.
• Aumentar a transparência ao fornecer a todas as partes acesso às mesmas informações, reduzindo disputas.
• Reduza erros confiando no código, o que elimina erros humanos.
• Reforce a segurança com proteções criptográficas, tornando difícil a adulteração.

Desvantagens dos Contratos Inteligentes

• Falta de flexibilidade para se ajustar a situações imprevistas devido à sua natureza rígida.
• Exigem conhecimentos especializados de codificação, limitando a adoção generalizada.

Ferramentas de Verificação Formal para Contratos Inteligentes Ethereum

Origem: Calibraint

Linguagens de especificação para criar especificações formais

• Act: Act permite aos usuários definir atualizações de armazenamento, pré e pós-condições e invariantes de contrato. Sua suíte de ferramentas inclui provedores de prova que podem validar várias propriedades usando Coq, solucionadores SMT ou hevm.

GitHub

Documentação

• Scribble: Scribble converte anotações de código escritas na sua linguagem de especificação em assertivas específicas que verificam as especificações.

Documentação

• Dafny: Dafny é uma linguagem de programação projetada para verificação, usando anotações de alto nível para ajudar a raciocinar e confirmar a correção do código.

GitHub

Verificadores de programas para verificar a exatidão

• Certora Prover: Certora Prover é uma ferramenta automatizada de verificação formal que verifica a correção dos códigos de contratos inteligentes. As especificações são criadas usando a Linguagem de Verificação Certora (CVL), e detecta violações de propriedade através de uma combinação de análise estática e técnicas de resolução de restrições.

Site

Documentação

• Solidity SMTChecker: O SMTChecker do Solidity é um verificador de modelo integrado que utiliza Satisfiability Modulo Theories (SMT) e resolução de Horn. Ele verifica se o código-fonte de um contrato está alinhado com as especificações durante a compilação e verifica violações de propriedades de segurança.

GitHub

• Solc-verify: Solc-verify é uma versão aprimorada do compilador Solidity que permite a verificação formal automatizada de código Solidity por meio de anotações e verificação modular do programa.

GitHub

• KEVM: KEVM representa formalmente a Máquina Virtual Ethereum(EVM)criado usando o framework K. É executável e pode verificar reivindicações específicas relacionadas a propriedades através da lógica de alcançabilidade.

GitHub

Documentação

Estruturas lógicas para prova de teoremas

• Isabelle: Isabelle/HOL é um assistente de prova que ajuda os usuários a expressar fórmulas matemáticas em uma linguagem formal e fornece ferramentas para prová-las. Seu uso principal é formalizar provas matemáticas, especialmente para verificar a correção de hardware e software de computador e as propriedades de linguagens de programação e protocolos.

GitHub

Documentação

• Coq - Coq é um provador de teorema interativo que permite definir programas com teoremas e criar provas verificadas por máquina de sua correção através de um processo interativo.

GitHub

Documentação

Ferramentas baseadas em execução simbólica para detetar padrões vulneráveis em contratos inteligentes

• Manticore - Uma ferramenta que analisa o bytecode EVM usando execução simbólica.

GitHub

Documentação

• Hevm - hevm é um motor de execução simbólica que verifica a equivalência do bytecode do EVM.

GitHub

• Mythril - Uma ferramenta de execução simbólica usada para encontrar vulnerabilidades em contratos inteligentes Ethereum.

GitHub

Documentação

Conclusão

Para proteger os contratos inteligentes, combinar verificação formal com auditoria manual é crucial para uma avaliação abrangente da sua segurança. Embora a verificação formal possa ser pesada em recursos, é um investimento valioso para contratos que envolvem altas apostas ou riscos significativos. Os contratos inteligentes são mais do que um conceito moderno; eles estão transformando as operações comerciais globais e, embora apresentem desafios, sua capacidade incomparável de aumentar a eficiência, minimizar erros e reforçar a segurança não pode ser ignorada. Os contratos inteligentes têm um potencial tremendo para simplificar processos e fomentar a confiança em transações digitais. Nesse sentido, as organizações que adotam essa tecnologia hoje estarão preparadas para prosperar em um futuro que prioriza a transparência e a confiabilidade.