VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
Contratos inteligentesestão tornando possível a criação de aplicativos descentralizados, sem confiança e robustos que introduzem novos casos de uso e desbloqueiam valor para os usuários. Como os contratos inteligentes lidam com grandes quantidades de valor, a segurança é uma consideração crítica para os desenvolvedores.
A verificação formal é uma das técnicas recomendadas para melhorarsegurança de contrato inteligente. Verificação formal, que usa métodos formais
para especificar, projetar e verificar programas, tem sido usado por anos para garantir a correção de sistemas críticos de hardware e software.
Quando implementada em contratos inteligentes, a verificação formal pode provar que a lógica de negócios de um contrato atende a uma especificação predefinida. Comparado a outros métodos para avaliar a correção do código do contrato, como testes, a verificação formal oferece garantias mais fortes de que um contrato inteligente está funcionalmente correto.
O QUE É A VERIFICAÇÃO FORMAL?
A verificação formal refere-se ao processo de avaliação da correção de um sistema em relação a uma especificação formal. Em termos mais simples, a verificação formal nos permite verificar se o comportamento de um sistema satisfaz alguns requisitos (ou seja, faz o que queremos).
Os comportamentos esperados do sistema (um contrato inteligente, neste caso) são descritos usando modelagem formal, enquanto as linguagens de especificação permitem a criação de propriedades formais. As técnicas de verificação formal podem então verificar que a implementação de um contrato está de acordo com sua especificação e derivar uma prova matemática da correção do primeiro. Quando um contrato satisfaz sua especificação, ele é descrito como "funcionalmente correto", "correto por design" ou "correto por construção".
O que é um modelo formal?
Em ciência da computação, um modelo formal
é uma descrição matemática de um processo computacional. Os programas são abstraídos em funções matemáticas (equações), com o modelo descrevendo como as saídas para funções são computadas dada uma entrada.
Os modelos formais fornecem um nível de abstração sobre o qual a análise do comportamento de um programa pode ser avaliada. A existência de modelos formais permite a criação de uma especificação formal, que descreve as propriedades desejadas do modelo em questão.
Diferentes técnicas são usadas para modelar contratos inteligentes para verificação formal. Por exemplo, alguns modelos são usados para raciocinar sobre o comportamento de alto nível de um contrato inteligente. Essas técnicas de modelagem aplicam uma visão de caixa-preta aos contratos inteligentes, vendo-os como sistemas que aceitam entradas e executam computação com base nessas entradas.
Modelos de alto nível focam na relação entre contratos inteligentes e agentes externos, como contas de propriedade externa (EOAs), contas de contrato e o ambiente de blockchain. Tais modelos são úteis para definir propriedades que especificam como um contrato deve se comportar em resposta a certas interações do usuário.
Por outro lado, outros modelos formais se concentram no comportamento de baixo nível de um contrato inteligente. Enquanto os modelos de alto nível podem ajudar a raciocinar sobre a funcionalidade de um contrato, eles podem falhar em capturar detalhes sobre o funcionamento interno da implementação. Modelos de baixo nível aplicam uma visão de caixa branca à análise de programas e dependem de representações de baixo nível de aplicativos de contratos inteligentes, como rastreamentos de programas e gráficos de fluxo de controle
, para raciocinar sobre propriedades relevantes para a execução de um contrato.
Modelos de baixo nível são considerados ideais, uma vez que representam a execução real de um contrato inteligente no ambiente de execução do Ethereum (ou seja, o EVM). As técnicas de modelagem de baixo nível são especialmente úteis para estabelecer propriedades críticas de segurança em contratos inteligentes e detectar vulnerabilidades potenciais.
O que é uma especificação formal?
Uma especificação é simplesmente um requisito técnico que um sistema específico deve satisfazer. Na programação, especificações representam ideias gerais sobre a execução de um programa (ou seja, o que o programa deve fazer).
No contexto dos contratos inteligentes, as especificações formais referem-se a propriedades—descrições formais dos requisitos que um contrato deve satisfazer. Tais propriedades são descritas como “invariantes” e representam afirmações lógicas sobre a execução de um contrato que devem permanecer verdadeiras em todas as circunstâncias possíveis, sem exceções.
Assim, podemos pensar em uma especificação formal como uma coleção de declarações escritas em uma linguagem formal que descrevem a execução pretendida de um contrato inteligente. As especificações abrangem as propriedades de um contrato e definem como o contrato deve se comportar em diferentes circunstâncias. O objetivo da verificação formal é determinar se um contrato inteligente possui essas propriedades (invariantes) e se essas propriedades não são violadas durante a execução.
Especificações formais são críticas no desenvolvimento de implementações seguras de contratos inteligentes. Contratos que falham em implementar invariantes ou têm suas propriedades violadas durante a execução estão sujeitos a vulnerabilidades que podem prejudicar a funcionalidade ou causar explorações maliciosas.
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
Especificações formais permitem raciocínio matemático sobre a correção da execução do programa. Assim como modelos formais, especificações formais podem capturar propriedades de alto nível ou o comportamento de baixo nível de uma implementação de contrato.
Especificações formais são derivadas usando elementos de lógica de programa
, que permitem raciocínio formal sobre as propriedades de um programa. Uma lógica de programa tem regras formais que expressam (em linguagem matemática) o comportamento esperado de um programa. Várias lógicas de programa são usadas na criação de especificações formais, incluindo lógica de alcançabilidade
Especificações formais para contratos inteligentes podem ser classificadas de forma ampla como especificações de alto nível ou de baixo nível. Independentemente da categoria a que pertence uma especificação, esta deve descrever adequadamente e de forma não ambígua a propriedade do sistema em análise.
Especificações de alto nível
Como o nome sugere, uma especificação de alto nível (também chamada de "especificação orientada a modelos") descreve o comportamento de alto nível de um programa. As especificações de alto nível modelam um smart contract como um máquina de estado finito
(FSM), que pode fazer a transição entre estados realizando operações, com lógica temporal usada para definir propriedades formais para o modelo FSM.
são "regras para raciocinar sobre proposições qualificadas em termos de tempo (por exemplo, "Estou sempre com fome" ou "Eventualmente ficarei com fome")." Quando aplicadas à verificação formal, lógicas temporais são usadas para declarar assertivas sobre o comportamento correto de sistemas modelados como máquinas de estado. Especificamente, uma lógica temporal descreve os estados futuros em que um contrato inteligente pode estar e como ele transita entre os estados.
As especificações de alto nível geralmente capturam duas propriedades temporais críticas para contratos inteligentes: segurança e vivacidade. As propriedades de segurança representam a ideia de que "nada de ruim acontece" e geralmente expressam invariância. Uma propriedade de segurança pode definir requisitos gerais de software, como a liberdade de impasse
, ou expressar propriedades específicas de domínio para contratos (por exemplo, invariantes no controle de acesso para funções, valores admissíveis de variáveis de estado ou condições para transferências de tokens).
Considere, por exemplo, este requisito de segurança que abrange as condições para usar o transfer() ou transferFrom() nos contratos de token ERC-20: 'O saldo do remetente nunca é inferior à quantidade solicitada de tokens a serem enviados.' Essa descrição em linguagem natural de um invariante de contrato pode ser traduzida em uma especificação formal (matemática), que pode então ser verificada rigorosamente quanto à validade.
As propriedades de vivacidade afirmam que "algo eventualmente bom acontece" e dizem respeito à capacidade de um contrato progredir por diferentes estados. Um exemplo de propriedade de vivacidade é "liquidez", que se refere à capacidade de um contrato transferir seus saldos para os usuários quando solicitado. Se essa propriedade for violada, os usuários não poderão sacar os ativos armazenados no contrato, como aconteceu com o Incidente da carteira Parity
.
Especificações de baixo nível
As especificações de alto nível partem de um modelo de contrato de estado finito e definem as propriedades desejadas desse modelo. Em contraste, as especificações de baixo nível (também chamadas de especificações orientadas a propriedades) frequentemente modelam programas (contratos inteligentes) como sistemas que compreendem uma coleção de funções matemáticas e descrevem o comportamento correto de tais sistemas.
Em termos mais simples, as especificações de baixo nível analisam rastros de programa e tentam definir propriedades de um contrato inteligente ao longo desses rastros. Os rastros se referem a sequências de execuções de funções que alteram o estado de um contrato inteligente; portanto, as especificações de baixo nível ajudam a especificar os requisitos para a execução interna de um contrato.
As especificações formais de baixo nível podem ser fornecidas como propriedades estilo Hoare ou invariáveis nos caminhos de execução.
Propriedades de estilo Hoare
fornece um conjunto de regras formais para raciocinar sobre a correção de programas, incluindo contratos inteligentes. Uma propriedade no estilo de Hoare é representada por um triplo de Hoare {P}c{Q}, onde c é um programa e P e Q são predicados sobre o estado do c (ou seja, o programa), formalmente descritos como precondições e pós-condições, respectivamente.
Uma pré-condição é um predicado que descreve as condições necessárias para a execução correta de uma função; os usuários que chamam o contrato devem satisfazer esse requisito. Uma pós-condição é um predicado que descreve a condição que uma função estabelece se executada corretamente; os usuários podem esperar que essa condição seja verdadeira após chamar a função. Um invariante na lógica de Hoare é um predicado que é preservado pela execução de uma função (ou seja, ele não muda).
As especificações no estilo Hoare podem garantir ou parcial ou total correção. A implementação de uma função de contrato é considerada "parcialmente correta" se a pré-condição for verdadeira antes da execução da função e, se a execução terminar, a pós-condição também é verdadeira. A prova da total correção é obtida se uma pré-condição for verdadeira antes da execução da função, a execução é garantida para terminar e, quando isso acontece, a pós-condição é verdadeira.
Obter prova de total correção é difícil, uma vez que algumas execuções podem atrasar antes de terminar, ou nunca terminar. Isso dito, a questão de se a execução termina é, indiscutivelmente, um ponto discutível, uma vez que o mecanismo de gasolina do Ethereum impede loops de programa infinitos (a execução termina com sucesso ou termina devido a erro de 'falta de gasolina').
As especificações de contratos inteligentes criados usando lógica de Hoare terão precondições, pós-condições e invariantes definidos para a execução de funções e loops em um contrato. As precondições frequentemente incluem a possibilidade de entradas errôneas para uma função, com as pós-condições descrevendo a resposta esperada a tais entradas (por exemplo, lançando uma exceção específica). Desta forma, as propriedades no estilo Hoare são eficazes para garantir a correção das implementações de contrato.
Muitos frameworks de verificação formal usam especificações no estilo de Hoare para provar a correção semântica das funções. Também é possível adicionar propriedades no estilo de Hoare (como assertivas) diretamente ao código do contrato usando as declarações require e assert em Solidity.
declarações de exigência expressam uma pré-condição ou invariante e são frequentemente usadas para validar entradas de usuário, enquanto assert captura uma pós-condição necessária para a segurança. Por exemplo, o controle de acesso adequado para funções (um exemplo de uma propriedade de segurança) pode ser alcançado usando require como uma verificação de pré-condição na identidade da conta chamadora. Da mesma forma, uma invariante sobre valores permissíveis de variáveis de estado em um contrato (por exemplo, número total de tokens em circulação) pode ser protegida de violação usando assert para confirmar o estado do contrato após a execução da função.
Propriedades de nível de rastreamento
Especificações baseadas em traços descrevem operações que fazem a transição de um contrato entre diferentes estados e as relações entre essas operações. Como explicado anteriormente, os traços são sequências de operações que alteram o estado de um contrato de uma maneira particular.
Esta abordagem baseia-se no modelo de contratos inteligentes como sistemas de transição de estado com alguns estados predefinidos (descritos por variáveis de estado) juntamente com um conjunto de transições predefinidas (descritas por funções de contrato). Além disso, gráfico de fluxo de controle
(CFG), que é uma representação gráfica do fluxo de execução de um programa, é frequentemente usado para descrever a semântica operacional de um contrato. Aqui, cada trajeto é representado como um caminho no grafo de fluxo de controle.
Primeiramente, as especificações de nível de rastreamento são usadas para raciocinar sobre padrões de execução interna em contratos inteligentes. Ao criar especificações em nível de rastreamento, afirmamos os caminhos de execução admissíveis (ou seja, transições de estado) para um contrato inteligente. Utilizando técnicas, como a execução simbólica, podemos verificar formalmente que a execução nunca segue um caminho não definido no modelo formal.
Vamos usar um exemplo de um DAOcontrato que possui algumas funções de acesso público para descrever propriedades de nível de rastreamento. Aqui, assumimos que o contrato DAO permite que os usuários realizem as seguintes operações:
- Depósito de fundos
- Vote em uma proposta após depositar fundos
- Reivindique um reembolso se eles não votarem em uma proposta
Exemplo de propriedades de nível de rastreamento poderiam ser “usuários que não depositam fundos não podem votar em uma proposta” ou “usuários que não votam em uma proposta sempre devem poder solicitar um reembolso”. Ambas as propriedades afirmam sequências de execução preferidas (a votação não pode acontecer antes do depósito de fundos e reivindicar um reembolso não pode acontecer depois de votar em uma proposta).
TÉCNICAS PARA VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES VERI
Verificação de modelo
A verificação de modelos é uma técnica de verificação formal na qual um algoritmo verifica um modelo formal de um contrato inteligente em relação à sua especificação. Na verificação de modelos, os contratos inteligentes são frequentemente representados como sistemas de transição de estados, enquanto as propriedades sobre estados de contrato permitidos são definidas usando lógica temporal.
A verificação de modelo requer a criação de uma representação matemática abstrata de um sistema (ou seja, um contrato) e a expressão de propriedades deste sistema usando fórmulas enraizadas emlógica proposicional
. Isso simplifica a tarefa do algoritmo de verificação de modelo, ou seja, provar que um modelo matemático satisfaz uma fórmula lógica dada.
A verificação de modelo na verificação formal é usada principalmente para avaliar propriedades temporais que descrevem o comportamento de um contrato ao longo do tempo. As propriedades temporais para contratos inteligentes incluem segurança e vivacidade, como explicamos anteriormente.
Por exemplo, uma propriedade de segurança relacionada ao controle de acesso (por exemplo, apenas o proprietário do contrato pode chamar a autodestruição) pode ser escrita em lógica formal. Em seguida, o algoritmo de verificação de modelo pode verificar se o contrato satisfaz esta especificação formal.
A verificação de modelos usa a exploração do espaço de estados, que envolve a construção de todos os estados possíveis de um contrato inteligente e a tentativa de encontrar estados alcançáveis que resultem em violações de propriedades. No entanto, isso pode levar a um número infinito de estados (conhecido como o 'problema da explosão de estados'), portanto, os verificadores de modelos dependem de técnicas de abstração para tornar possível a análise eficiente de contratos inteligentes.
Prova de teorema
A prova de teoremas é um método de raciocínio matemático sobre a correção de programas, incluindo contratos inteligentes. Envolve a transformação do modelo do sistema de um contrato e suas especificações em fórmulas matemáticas (declarações lógicas).
O objetivo da prova de teorema é verificar a equivalência lógica entre essas afirmações. "Equivalência lógica" (também chamada de "bicondicional lógico") é um tipo de relação entre duas afirmações, de modo que a primeira afirmação é verdadeira se e somente se a segunda afirmação for verdadeira.
A relação necessária (equivalência lógica) entre declarações sobre o modelo de um contrato e sua propriedade é formulada como uma declaração comprovável (chamada de teorema). Usando um sistema formal de inferência, o provador automático de teoremas pode verificar a validade do teorema. Em outras palavras, um provador de teoremas pode provar de forma conclusiva que o modelo de um contrato inteligente corresponde precisamente às suas especificações.
Enquanto a verificação de modelos contratos como sistemas de transição com estados finitos, a prova de teoremas pode lidar com a análise de sistemas de estado infinito. No entanto, isso significa que um provador automático de teoremas nem sempre pode saber se um problema lógico é “decidível” ou não.
Como resultado, muitas vezes é necessária assistência humana para orientar o provador de teoremas na derivação de provas de correção. O uso do esforço humano na prova de teoremas torna mais caro de se usar do que a verificação de modelos, que é totalmente automatizada.
Execução simbólica
A execução simbólica é um método de analisar um contrato inteligente executando funções usando valores simbólicos (por exemplo, x > 5) em vez de valores concretos (por exemplo, x == 5). Como técnica de verificação formal, a execução simbólica é usada para raciocinar formalmente sobre propriedades em nível de rastreamento no código de um contrato.
A execução simbólica representa um rastro de execução como uma fórmula matemática sobre valores de entrada simbólicos, também chamada de predicado de caminho. Um Resolvedor SMT
é usado para verificar se um predicado de caminho é "satisfatório" (ou seja, existe um valor que pode satisfazer a fórmula). Se um caminho vulnerável for satisfatório, o solucionador SMT gerará um valor concreto que direciona a execução para esse caminho.
Suponha que a função de um contrato inteligente receba como entrada um valor uint (x) e reverta quando x for maior que 5 e também menor que 10. Encontrar um valor para x que acione o erro usando um procedimento de teste normal exigiria executar dezenas de casos de teste (ou mais) sem a garantia de realmente encontrar uma entrada que acione o erro.
Por outro lado, uma ferramenta de execução simbólica executaria a função com o valor simbólico: X > 5 ∧ X < 10 (ou seja, x é maior que 5 E x é menor que 10). O predicado de caminho associado x = X > 5 ∧ X < 10 seria então dado a um solucionador SMT para resolver. Se um determinado valor satisfizer a fórmula x = X > 5 ∧ X < 10, o solucionador SMT o calculará — por exemplo, o solucionador pode produzir 7 como um valor para x.
Como a execução simbólica depende de entradas para um programa, e o conjunto de entradas para explorar todos os estados alcançáveis é potencialmente infinito, ainda é uma forma de teste. No entanto, como mostrado no exemplo, a execução simbólica é mais eficiente do que o teste regular para localizar entradas que acionam violações de propriedade.
Além disso, a execução simbólica produz menos falsos positivos do que outras técnicas baseadas em propriedades (por exemplo, fuzzing) que geram aleatoriamente entradas para uma função. Se um estado de erro for acionado durante a execução simbólica, é possível gerar um valor concreto que acione o erro e reproduza o problema.
A execução simbólica também pode fornecer algum grau de prova matemática de correção. Considere o seguinte exemplo de uma função de contrato com proteção contra overflow:
Um rastreamento de execução que resulta em um estouro de inteiro precisaria satisfazer a fórmula: z = x + y E (z >= x) E (z=>y) E (z < x OU z < y) Tal fórmula é improvável de ser resolvida, portanto, serve como uma prova matemática de que a função safe_add nunca causa estouro.
Por que usar verificação formal para contratos inteligentes?
Necessidade de confiabilidade
A verificação formal é usada para avaliar a correção de sistemas críticos de segurança cuja falha pode ter consequências devastadoras, como morte, ferimentos ou ruína financeira. Os contratos inteligentes são aplicações de alto valor que controlam enormes quantidades de valor, e erros simples no design podem levar aperdas irreparáveis para os usuários
Verificar formalmente um contrato antes da implantação, no entanto, pode aumentar as garantias de que ele funcionará como esperado quando estiver em execução na blockchain.
A confiabilidade é uma qualidade altamente desejada em qualquer contrato inteligente, especialmente porque o código implantado na Máquina Virtual Ethereum (EVM) é tipicamente imutável. Com atualizações pós-lançamento não facilmente acessíveis, a necessidade de garantir a confiabilidade dos contratos torna a verificação formal necessária. A verificação formal é capaz de detectar questões complicadas, como subfluxos e superfluxos de inteiros, reentrância e otimizações de gás ruins, que podem passar despercebidas por auditores e testadores.
Provar a correção funcional
Testar um programa é o método mais comum para provar que um contrato inteligente atende a alguns requisitos. Isso envolve a execução de um contrato com uma amostra dos dados que se espera que ele manipule e a análise de seu comportamento. Se o contrato retornar os resultados esperados para os dados de amostra, então os desenvolvedores têm uma prova objetiva de sua correção.
No entanto, essa abordagem não pode provar a execução correta para valores de entrada que não fazem parte da amostra. Portanto, testar um contrato pode ajudar a detectar bugs (ou seja, se alguns caminhos de código falharem em retornar os resultados desejados durante a execução), mas não pode provar conclusivamente a ausência de bugs.
Por outro lado, a verificação formal pode provar formalmente que um contrato inteligente atende aos requisitos para uma gama infinita de execuções sem executar o contrato. Isso requer a criação de uma especificação formal que descreva precisamente os comportamentos corretos do contrato e o desenvolvimento de um modelo formal (matemático) do sistema do contrato. Em seguida, podemos seguir um procedimento de prova formal para verificar a consistência entre o modelo do contrato e sua especificação.
Com a verificação formal, a questão de verificar se a lógica de negócios de um contrato atende aos requisitos é uma proposição matemática que pode ser provada ou refutada. Ao provar formalmente uma proposição, podemos verificar um número infinito de casos de teste com um número finito de etapas. Desta forma, a verificação formal tem melhores perspectivas de provar que um contrato está funcionalmente correto em relação a uma especificação.
Alvos de verificação ideais
Um alvo de verificação descreve o sistema a ser verificado formalmente. A verificação formal é melhor usada em “sistemas embarcados” (pequenas e simples peças de software que fazem parte de um sistema maior). Eles também são ideais para domínios especializados que têm poucas regras, pois isso torna mais fácil modificar ferramentas para verificar propriedades específicas do domínio.
Os contratos inteligentes - pelo menos, em certa medida - atendem a ambos os requisitos. Por exemplo, o pequeno tamanho dos contratos do Ethereum os torna propensos à verificação formal. Da mesma forma, o EVM segue regras simples, o que torna a especificação e verificação de propriedades semânticas para programas em execução no EVM mais fácil.
Ciclo de desenvolvimento mais rápido
Técnicas de verificação formal, como verificação de modelo e execução simbólica, geralmente são mais eficientes do que a análise regular do código de contrato inteligente (realizada durante testes ou auditorias). Isso ocorre porque a verificação formal depende de valores simbólicos para testar asserções ("e se um usuário tentar sacar n éter?") ao contrário dos testes que usam valores concretos ("e se um usuário tentar sacar 5 éter?").
Variáveis de entrada simbólicas podem abranger várias classes de valores concretos, de modo que abordagens de verificação formal prometem cobertura de código maior em um período de tempo mais curto. Quando usada de forma eficaz, a verificação formal pode acelerar o ciclo de desenvolvimento para os desenvolvedores.
A verificação formal também melhora o processo de construção de aplicativos descentralizados (dapps) ao reduzir erros de design custosos. Atualizar contratos (quando possível) para corrigir vulnerabilidades requer uma extensa reescrita de bases de código e mais esforço gasto no desenvolvimento. A verificação formal pode detectar muitos erros na implementação de contratos que podem passar despercebidos por testadores e auditores, e fornece ampla oportunidade para corrigir esses problemas antes de implantar um contrato.
DESVANTAGENS DA VERIFICAÇÃO FORMAL
Custo da mão de obra manual
A verificação formal, especialmente a verificação semi-automatizada na qual um humano orienta o provador para derivar provas de correção, requer um trabalho manual considerável. Além disso, criar uma especificação formal é uma atividade complexa que exige um alto nível de habilidade.
Esses fatores (esforço e habilidade) tornam a verificação formal mais exigente e cara em comparação com os métodos usuais de avaliação de correção em contratos, como testes e auditorias. No entanto, pagar o custo por uma auditoria de verificação completa é prático, dada o custo dos erros nas implementações de contratos inteligentes.
Falsos negativos
A verificação formal só pode verificar se a execução do contrato inteligente corresponde à especificação formal. Como tal, é importante garantir que a especificação descreva adequadamente os comportamentos esperados de um contrato inteligente.
Se as especificações forem mal escritas, violações de propriedades - que apontam para execuções vulneráveis - não podem ser detectadas pela auditoria de verificação formal. Nesse caso, um desenvolvedor pode erroneamente assumir que o contrato está livre de bugs.
Problemas de desempenho
A verificação formal encontra uma série de problemas de desempenho. Por exemplo, problemas de explosão de estado e caminho encontrados durante a verificação de modelos e verificação simbólica, respectivamente, podem afetar os procedimentos de verificação. Além disso, as ferramentas de verificação formal frequentemente utilizam solucionadores SMT e outros solucionadores de restrições em sua camada subjacente, e esses solucionadores dependem de procedimentos computacionalmente intensivos.
Além disso, nem sempre é possível para os verificadores de programas determinar se uma propriedade (descrita como uma fórmula lógica) pode ser satisfeita ou não (oproblema de decidibilidade
") porque um programa pode nunca terminar. Como tal, pode ser impossível provar algumas propriedades para um contrato mesmo que esteja bem especificado.
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES DO ETHEREUM
Linguagens de especificação para criar especificações formais
Act: O Act permite a especificação de atualizações de armazenamento, condições pré/pós e invariantes de contrato. Sua suíte de ferramentas também possui backends de prova capazes de provar muitas propriedades via Coq, solucionadores SMT ou hevm.
Scribble - O Scribble transforma anotações de código na linguagem de especificação Scribble em assertivas concretas que verificam a especificação.
Dafny - Dafny é uma linguagem de programação pronta para verificação que depende de anotações de alto nível para raciocinar e provar a correção do código.
Verificadores de programas para verificar a correção
Certora Prover - Certora Prover é uma ferramenta automática de verificação formal para verificar a correção do código em contratos inteligentes. As especificações são escritas em CVL (Linguagem de Verificação Certora), com violações de propriedade detectadas usando uma combinação de análise estática e resolução de restrições.
Solidity SMTChecker - O SMTChecker do Solidity é um verificador de modelo integrado baseado em SMT (Satisfabilidade Modulo Theories) e resolução de Horn. Ele confirma se o código fonte de um contrato corresponde às especificações durante a compilação e verifica estaticamente as violações das propriedades de segurança.
solc-verify - solc-verify é uma versão estendida do compilador Solidity que pode realizar verificação formal automatizada de código Solidity usando anotações e verificação de programa modular.
KEVM - KEVM é uma semântica formal da Máquina Virtual Ethereum (EVM) escrita no framework K. KEVM é executável e pode provar certas afirmações relacionadas a propriedades usando lógica de alcançabilidade.
Estruturas lógicas para prova de teoremas
Isabelle - Isabelle/HOL é um assistente de prova que permite que fórmulas matemáticas sejam expressas em uma linguagem formal e fornece ferramentas para provar essas fórmulas. A principal aplicação é a formalização de provas matemáticas e, em particular, a verificação formal, que inclui provar a correção do hardware ou software de computador e provar propriedades de linguagens de computador e protocolos.
Coq - Coq é um provador de teoremas interativo que permite que você defina programas usando teoremas e gere interativamente provas verificadas por máquina de correção.
Ferramentas baseadas em execução simbólica para detectar padrões vulneráveis em contratos inteligentes
Manticore - Uma ferramenta para análise de bytecode EVM baseada em execução simbólica.
hevm - hevm é um mecanismo de execução simbólica e verificador de equivalência para bytecode EVM.
Mythril - Uma ferramenta de execução simbólica para detectar vulnerabilidades em contratos inteligentes Ethereum
Aviso Legal：
- Este artigo foi reproduzido de []. Todos os direitos autorais pertencem ao autor original [**]. Se houver objeções a esta reimpressão, entre em contato com o Gate Learnequipe e eles lidarão com isso prontamente.
- Isenção de Responsabilidade: As opiniões expressas neste artigo são exclusivamente do autor e não constituem aconselhamento de investimento.
- As traduções do artigo para outros idiomas são feitas pela equipe Gate Learn. Salvo indicação em contrário, copiar, distribuir ou plagiar os artigos traduzidos é proibido.
บทความที่เกี่ยวข้อง
O que é EtherVista, o autoproclamado "Novo Padrão para DEX"?
O que é Neiro? Tudo o que você precisa saber sobre NEIROETH
O que é Polígono 2.0 (POL)? Do MATIC ao POL
VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
O QUE É VERIFICAÇÃO FORMAL?
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
TÉCNICAS DE VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
DESVENTAGENS DA VERIFICAÇÃO FORMAL
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES DO ETHEREUM
Contratos inteligentesestão tornando possível a criação de aplicativos descentralizados, sem confiança e robustos que introduzem novos casos de uso e desbloqueiam valor para os usuários. Como os contratos inteligentes lidam com grandes quantidades de valor, a segurança é uma consideração crítica para os desenvolvedores.
A verificação formal é uma das técnicas recomendadas para melhorarsegurança de contrato inteligente. Verificação formal, que usa métodos formais
para especificar, projetar e verificar programas, tem sido usado por anos para garantir a correção de sistemas críticos de hardware e software.
Quando implementada em contratos inteligentes, a verificação formal pode provar que a lógica de negócios de um contrato atende a uma especificação predefinida. Comparado a outros métodos para avaliar a correção do código do contrato, como testes, a verificação formal oferece garantias mais fortes de que um contrato inteligente está funcionalmente correto.
O QUE É A VERIFICAÇÃO FORMAL?
A verificação formal refere-se ao processo de avaliação da correção de um sistema em relação a uma especificação formal. Em termos mais simples, a verificação formal nos permite verificar se o comportamento de um sistema satisfaz alguns requisitos (ou seja, faz o que queremos).
Os comportamentos esperados do sistema (um contrato inteligente, neste caso) são descritos usando modelagem formal, enquanto as linguagens de especificação permitem a criação de propriedades formais. As técnicas de verificação formal podem então verificar que a implementação de um contrato está de acordo com sua especificação e derivar uma prova matemática da correção do primeiro. Quando um contrato satisfaz sua especificação, ele é descrito como "funcionalmente correto", "correto por design" ou "correto por construção".
O que é um modelo formal?
Em ciência da computação, um modelo formal
é uma descrição matemática de um processo computacional. Os programas são abstraídos em funções matemáticas (equações), com o modelo descrevendo como as saídas para funções são computadas dada uma entrada.
Os modelos formais fornecem um nível de abstração sobre o qual a análise do comportamento de um programa pode ser avaliada. A existência de modelos formais permite a criação de uma especificação formal, que descreve as propriedades desejadas do modelo em questão.
Diferentes técnicas são usadas para modelar contratos inteligentes para verificação formal. Por exemplo, alguns modelos são usados para raciocinar sobre o comportamento de alto nível de um contrato inteligente. Essas técnicas de modelagem aplicam uma visão de caixa-preta aos contratos inteligentes, vendo-os como sistemas que aceitam entradas e executam computação com base nessas entradas.
Modelos de alto nível focam na relação entre contratos inteligentes e agentes externos, como contas de propriedade externa (EOAs), contas de contrato e o ambiente de blockchain. Tais modelos são úteis para definir propriedades que especificam como um contrato deve se comportar em resposta a certas interações do usuário.
Por outro lado, outros modelos formais se concentram no comportamento de baixo nível de um contrato inteligente. Enquanto os modelos de alto nível podem ajudar a raciocinar sobre a funcionalidade de um contrato, eles podem falhar em capturar detalhes sobre o funcionamento interno da implementação. Modelos de baixo nível aplicam uma visão de caixa branca à análise de programas e dependem de representações de baixo nível de aplicativos de contratos inteligentes, como rastreamentos de programas e gráficos de fluxo de controle
, para raciocinar sobre propriedades relevantes para a execução de um contrato.
Modelos de baixo nível são considerados ideais, uma vez que representam a execução real de um contrato inteligente no ambiente de execução do Ethereum (ou seja, o EVM). As técnicas de modelagem de baixo nível são especialmente úteis para estabelecer propriedades críticas de segurança em contratos inteligentes e detectar vulnerabilidades potenciais.
O que é uma especificação formal?
Uma especificação é simplesmente um requisito técnico que um sistema específico deve satisfazer. Na programação, especificações representam ideias gerais sobre a execução de um programa (ou seja, o que o programa deve fazer).
No contexto dos contratos inteligentes, as especificações formais referem-se a propriedades—descrições formais dos requisitos que um contrato deve satisfazer. Tais propriedades são descritas como “invariantes” e representam afirmações lógicas sobre a execução de um contrato que devem permanecer verdadeiras em todas as circunstâncias possíveis, sem exceções.
Assim, podemos pensar em uma especificação formal como uma coleção de declarações escritas em uma linguagem formal que descrevem a execução pretendida de um contrato inteligente. As especificações abrangem as propriedades de um contrato e definem como o contrato deve se comportar em diferentes circunstâncias. O objetivo da verificação formal é determinar se um contrato inteligente possui essas propriedades (invariantes) e se essas propriedades não são violadas durante a execução.
Especificações formais são críticas no desenvolvimento de implementações seguras de contratos inteligentes. Contratos que falham em implementar invariantes ou têm suas propriedades violadas durante a execução estão sujeitos a vulnerabilidades que podem prejudicar a funcionalidade ou causar explorações maliciosas.
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
Especificações formais permitem raciocínio matemático sobre a correção da execução do programa. Assim como modelos formais, especificações formais podem capturar propriedades de alto nível ou o comportamento de baixo nível de uma implementação de contrato.
Especificações formais são derivadas usando elementos de lógica de programa
, que permitem raciocínio formal sobre as propriedades de um programa. Uma lógica de programa tem regras formais que expressam (em linguagem matemática) o comportamento esperado de um programa. Várias lógicas de programa são usadas na criação de especificações formais, incluindo lógica de alcançabilidade
Especificações formais para contratos inteligentes podem ser classificadas de forma ampla como especificações de alto nível ou de baixo nível. Independentemente da categoria a que pertence uma especificação, esta deve descrever adequadamente e de forma não ambígua a propriedade do sistema em análise.
Especificações de alto nível
Como o nome sugere, uma especificação de alto nível (também chamada de "especificação orientada a modelos") descreve o comportamento de alto nível de um programa. As especificações de alto nível modelam um smart contract como um máquina de estado finito
(FSM), que pode fazer a transição entre estados realizando operações, com lógica temporal usada para definir propriedades formais para o modelo FSM.
são "regras para raciocinar sobre proposições qualificadas em termos de tempo (por exemplo, "Estou sempre com fome" ou "Eventualmente ficarei com fome")." Quando aplicadas à verificação formal, lógicas temporais são usadas para declarar assertivas sobre o comportamento correto de sistemas modelados como máquinas de estado. Especificamente, uma lógica temporal descreve os estados futuros em que um contrato inteligente pode estar e como ele transita entre os estados.
As especificações de alto nível geralmente capturam duas propriedades temporais críticas para contratos inteligentes: segurança e vivacidade. As propriedades de segurança representam a ideia de que "nada de ruim acontece" e geralmente expressam invariância. Uma propriedade de segurança pode definir requisitos gerais de software, como a liberdade de impasse
, ou expressar propriedades específicas de domínio para contratos (por exemplo, invariantes no controle de acesso para funções, valores admissíveis de variáveis de estado ou condições para transferências de tokens).
Considere, por exemplo, este requisito de segurança que abrange as condições para usar o transfer() ou transferFrom() nos contratos de token ERC-20: 'O saldo do remetente nunca é inferior à quantidade solicitada de tokens a serem enviados.' Essa descrição em linguagem natural de um invariante de contrato pode ser traduzida em uma especificação formal (matemática), que pode então ser verificada rigorosamente quanto à validade.
As propriedades de vivacidade afirmam que "algo eventualmente bom acontece" e dizem respeito à capacidade de um contrato progredir por diferentes estados. Um exemplo de propriedade de vivacidade é "liquidez", que se refere à capacidade de um contrato transferir seus saldos para os usuários quando solicitado. Se essa propriedade for violada, os usuários não poderão sacar os ativos armazenados no contrato, como aconteceu com o Incidente da carteira Parity
.
Especificações de baixo nível
As especificações de alto nível partem de um modelo de contrato de estado finito e definem as propriedades desejadas desse modelo. Em contraste, as especificações de baixo nível (também chamadas de especificações orientadas a propriedades) frequentemente modelam programas (contratos inteligentes) como sistemas que compreendem uma coleção de funções matemáticas e descrevem o comportamento correto de tais sistemas.
Em termos mais simples, as especificações de baixo nível analisam rastros de programa e tentam definir propriedades de um contrato inteligente ao longo desses rastros. Os rastros se referem a sequências de execuções de funções que alteram o estado de um contrato inteligente; portanto, as especificações de baixo nível ajudam a especificar os requisitos para a execução interna de um contrato.
As especificações formais de baixo nível podem ser fornecidas como propriedades estilo Hoare ou invariáveis nos caminhos de execução.
Propriedades de estilo Hoare
fornece um conjunto de regras formais para raciocinar sobre a correção de programas, incluindo contratos inteligentes. Uma propriedade no estilo de Hoare é representada por um triplo de Hoare {P}c{Q}, onde c é um programa e P e Q são predicados sobre o estado do c (ou seja, o programa), formalmente descritos como precondições e pós-condições, respectivamente.
Uma pré-condição é um predicado que descreve as condições necessárias para a execução correta de uma função; os usuários que chamam o contrato devem satisfazer esse requisito. Uma pós-condição é um predicado que descreve a condição que uma função estabelece se executada corretamente; os usuários podem esperar que essa condição seja verdadeira após chamar a função. Um invariante na lógica de Hoare é um predicado que é preservado pela execução de uma função (ou seja, ele não muda).
As especificações no estilo Hoare podem garantir ou parcial ou total correção. A implementação de uma função de contrato é considerada "parcialmente correta" se a pré-condição for verdadeira antes da execução da função e, se a execução terminar, a pós-condição também é verdadeira. A prova da total correção é obtida se uma pré-condição for verdadeira antes da execução da função, a execução é garantida para terminar e, quando isso acontece, a pós-condição é verdadeira.
Obter prova de total correção é difícil, uma vez que algumas execuções podem atrasar antes de terminar, ou nunca terminar. Isso dito, a questão de se a execução termina é, indiscutivelmente, um ponto discutível, uma vez que o mecanismo de gasolina do Ethereum impede loops de programa infinitos (a execução termina com sucesso ou termina devido a erro de 'falta de gasolina').
As especificações de contratos inteligentes criados usando lógica de Hoare terão precondições, pós-condições e invariantes definidos para a execução de funções e loops em um contrato. As precondições frequentemente incluem a possibilidade de entradas errôneas para uma função, com as pós-condições descrevendo a resposta esperada a tais entradas (por exemplo, lançando uma exceção específica). Desta forma, as propriedades no estilo Hoare são eficazes para garantir a correção das implementações de contrato.
Muitos frameworks de verificação formal usam especificações no estilo de Hoare para provar a correção semântica das funções. Também é possível adicionar propriedades no estilo de Hoare (como assertivas) diretamente ao código do contrato usando as declarações require e assert em Solidity.
declarações de exigência expressam uma pré-condição ou invariante e são frequentemente usadas para validar entradas de usuário, enquanto assert captura uma pós-condição necessária para a segurança. Por exemplo, o controle de acesso adequado para funções (um exemplo de uma propriedade de segurança) pode ser alcançado usando require como uma verificação de pré-condição na identidade da conta chamadora. Da mesma forma, uma invariante sobre valores permissíveis de variáveis de estado em um contrato (por exemplo, número total de tokens em circulação) pode ser protegida de violação usando assert para confirmar o estado do contrato após a execução da função.
Propriedades de nível de rastreamento
Especificações baseadas em traços descrevem operações que fazem a transição de um contrato entre diferentes estados e as relações entre essas operações. Como explicado anteriormente, os traços são sequências de operações que alteram o estado de um contrato de uma maneira particular.
Esta abordagem baseia-se no modelo de contratos inteligentes como sistemas de transição de estado com alguns estados predefinidos (descritos por variáveis de estado) juntamente com um conjunto de transições predefinidas (descritas por funções de contrato). Além disso, gráfico de fluxo de controle
(CFG), que é uma representação gráfica do fluxo de execução de um programa, é frequentemente usado para descrever a semântica operacional de um contrato. Aqui, cada trajeto é representado como um caminho no grafo de fluxo de controle.
Primeiramente, as especificações de nível de rastreamento são usadas para raciocinar sobre padrões de execução interna em contratos inteligentes. Ao criar especificações em nível de rastreamento, afirmamos os caminhos de execução admissíveis (ou seja, transições de estado) para um contrato inteligente. Utilizando técnicas, como a execução simbólica, podemos verificar formalmente que a execução nunca segue um caminho não definido no modelo formal.
Vamos usar um exemplo de um DAOcontrato que possui algumas funções de acesso público para descrever propriedades de nível de rastreamento. Aqui, assumimos que o contrato DAO permite que os usuários realizem as seguintes operações:
- Depósito de fundos
- Vote em uma proposta após depositar fundos
- Reivindique um reembolso se eles não votarem em uma proposta
Exemplo de propriedades de nível de rastreamento poderiam ser “usuários que não depositam fundos não podem votar em uma proposta” ou “usuários que não votam em uma proposta sempre devem poder solicitar um reembolso”. Ambas as propriedades afirmam sequências de execução preferidas (a votação não pode acontecer antes do depósito de fundos e reivindicar um reembolso não pode acontecer depois de votar em uma proposta).
TÉCNICAS PARA VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES VERI
Verificação de modelo
A verificação de modelos é uma técnica de verificação formal na qual um algoritmo verifica um modelo formal de um contrato inteligente em relação à sua especificação. Na verificação de modelos, os contratos inteligentes são frequentemente representados como sistemas de transição de estados, enquanto as propriedades sobre estados de contrato permitidos são definidas usando lógica temporal.
A verificação de modelo requer a criação de uma representação matemática abstrata de um sistema (ou seja, um contrato) e a expressão de propriedades deste sistema usando fórmulas enraizadas emlógica proposicional
. Isso simplifica a tarefa do algoritmo de verificação de modelo, ou seja, provar que um modelo matemático satisfaz uma fórmula lógica dada.
A verificação de modelo na verificação formal é usada principalmente para avaliar propriedades temporais que descrevem o comportamento de um contrato ao longo do tempo. As propriedades temporais para contratos inteligentes incluem segurança e vivacidade, como explicamos anteriormente.
Por exemplo, uma propriedade de segurança relacionada ao controle de acesso (por exemplo, apenas o proprietário do contrato pode chamar a autodestruição) pode ser escrita em lógica formal. Em seguida, o algoritmo de verificação de modelo pode verificar se o contrato satisfaz esta especificação formal.
A verificação de modelos usa a exploração do espaço de estados, que envolve a construção de todos os estados possíveis de um contrato inteligente e a tentativa de encontrar estados alcançáveis que resultem em violações de propriedades. No entanto, isso pode levar a um número infinito de estados (conhecido como o 'problema da explosão de estados'), portanto, os verificadores de modelos dependem de técnicas de abstração para tornar possível a análise eficiente de contratos inteligentes.
Prova de teorema
A prova de teoremas é um método de raciocínio matemático sobre a correção de programas, incluindo contratos inteligentes. Envolve a transformação do modelo do sistema de um contrato e suas especificações em fórmulas matemáticas (declarações lógicas).
O objetivo da prova de teorema é verificar a equivalência lógica entre essas afirmações. "Equivalência lógica" (também chamada de "bicondicional lógico") é um tipo de relação entre duas afirmações, de modo que a primeira afirmação é verdadeira se e somente se a segunda afirmação for verdadeira.
A relação necessária (equivalência lógica) entre declarações sobre o modelo de um contrato e sua propriedade é formulada como uma declaração comprovável (chamada de teorema). Usando um sistema formal de inferência, o provador automático de teoremas pode verificar a validade do teorema. Em outras palavras, um provador de teoremas pode provar de forma conclusiva que o modelo de um contrato inteligente corresponde precisamente às suas especificações.
Enquanto a verificação de modelos contratos como sistemas de transição com estados finitos, a prova de teoremas pode lidar com a análise de sistemas de estado infinito. No entanto, isso significa que um provador automático de teoremas nem sempre pode saber se um problema lógico é “decidível” ou não.
Como resultado, muitas vezes é necessária assistência humana para orientar o provador de teoremas na derivação de provas de correção. O uso do esforço humano na prova de teoremas torna mais caro de se usar do que a verificação de modelos, que é totalmente automatizada.
Execução simbólica
A execução simbólica é um método de analisar um contrato inteligente executando funções usando valores simbólicos (por exemplo, x > 5) em vez de valores concretos (por exemplo, x == 5). Como técnica de verificação formal, a execução simbólica é usada para raciocinar formalmente sobre propriedades em nível de rastreamento no código de um contrato.
A execução simbólica representa um rastro de execução como uma fórmula matemática sobre valores de entrada simbólicos, também chamada de predicado de caminho. Um Resolvedor SMT
é usado para verificar se um predicado de caminho é "satisfatório" (ou seja, existe um valor que pode satisfazer a fórmula). Se um caminho vulnerável for satisfatório, o solucionador SMT gerará um valor concreto que direciona a execução para esse caminho.
Suponha que a função de um contrato inteligente receba como entrada um valor uint (x) e reverta quando x for maior que 5 e também menor que 10. Encontrar um valor para x que acione o erro usando um procedimento de teste normal exigiria executar dezenas de casos de teste (ou mais) sem a garantia de realmente encontrar uma entrada que acione o erro.
Por outro lado, uma ferramenta de execução simbólica executaria a função com o valor simbólico: X > 5 ∧ X < 10 (ou seja, x é maior que 5 E x é menor que 10). O predicado de caminho associado x = X > 5 ∧ X < 10 seria então dado a um solucionador SMT para resolver. Se um determinado valor satisfizer a fórmula x = X > 5 ∧ X < 10, o solucionador SMT o calculará — por exemplo, o solucionador pode produzir 7 como um valor para x.
Como a execução simbólica depende de entradas para um programa, e o conjunto de entradas para explorar todos os estados alcançáveis é potencialmente infinito, ainda é uma forma de teste. No entanto, como mostrado no exemplo, a execução simbólica é mais eficiente do que o teste regular para localizar entradas que acionam violações de propriedade.
Além disso, a execução simbólica produz menos falsos positivos do que outras técnicas baseadas em propriedades (por exemplo, fuzzing) que geram aleatoriamente entradas para uma função. Se um estado de erro for acionado durante a execução simbólica, é possível gerar um valor concreto que acione o erro e reproduza o problema.
A execução simbólica também pode fornecer algum grau de prova matemática de correção. Considere o seguinte exemplo de uma função de contrato com proteção contra overflow:
Um rastreamento de execução que resulta em um estouro de inteiro precisaria satisfazer a fórmula: z = x + y E (z >= x) E (z=>y) E (z < x OU z < y) Tal fórmula é improvável de ser resolvida, portanto, serve como uma prova matemática de que a função safe_add nunca causa estouro.
Por que usar verificação formal para contratos inteligentes?
Necessidade de confiabilidade
A verificação formal é usada para avaliar a correção de sistemas críticos de segurança cuja falha pode ter consequências devastadoras, como morte, ferimentos ou ruína financeira. Os contratos inteligentes são aplicações de alto valor que controlam enormes quantidades de valor, e erros simples no design podem levar aperdas irreparáveis para os usuários
Verificar formalmente um contrato antes da implantação, no entanto, pode aumentar as garantias de que ele funcionará como esperado quando estiver em execução na blockchain.
A confiabilidade é uma qualidade altamente desejada em qualquer contrato inteligente, especialmente porque o código implantado na Máquina Virtual Ethereum (EVM) é tipicamente imutável. Com atualizações pós-lançamento não facilmente acessíveis, a necessidade de garantir a confiabilidade dos contratos torna a verificação formal necessária. A verificação formal é capaz de detectar questões complicadas, como subfluxos e superfluxos de inteiros, reentrância e otimizações de gás ruins, que podem passar despercebidas por auditores e testadores.
Provar a correção funcional
Testar um programa é o método mais comum para provar que um contrato inteligente atende a alguns requisitos. Isso envolve a execução de um contrato com uma amostra dos dados que se espera que ele manipule e a análise de seu comportamento. Se o contrato retornar os resultados esperados para os dados de amostra, então os desenvolvedores têm uma prova objetiva de sua correção.
No entanto, essa abordagem não pode provar a execução correta para valores de entrada que não fazem parte da amostra. Portanto, testar um contrato pode ajudar a detectar bugs (ou seja, se alguns caminhos de código falharem em retornar os resultados desejados durante a execução), mas não pode provar conclusivamente a ausência de bugs.
Por outro lado, a verificação formal pode provar formalmente que um contrato inteligente atende aos requisitos para uma gama infinita de execuções sem executar o contrato. Isso requer a criação de uma especificação formal que descreva precisamente os comportamentos corretos do contrato e o desenvolvimento de um modelo formal (matemático) do sistema do contrato. Em seguida, podemos seguir um procedimento de prova formal para verificar a consistência entre o modelo do contrato e sua especificação.
Com a verificação formal, a questão de verificar se a lógica de negócios de um contrato atende aos requisitos é uma proposição matemática que pode ser provada ou refutada. Ao provar formalmente uma proposição, podemos verificar um número infinito de casos de teste com um número finito de etapas. Desta forma, a verificação formal tem melhores perspectivas de provar que um contrato está funcionalmente correto em relação a uma especificação.
Alvos de verificação ideais
Um alvo de verificação descreve o sistema a ser verificado formalmente. A verificação formal é melhor usada em “sistemas embarcados” (pequenas e simples peças de software que fazem parte de um sistema maior). Eles também são ideais para domínios especializados que têm poucas regras, pois isso torna mais fácil modificar ferramentas para verificar propriedades específicas do domínio.
Os contratos inteligentes - pelo menos, em certa medida - atendem a ambos os requisitos. Por exemplo, o pequeno tamanho dos contratos do Ethereum os torna propensos à verificação formal. Da mesma forma, o EVM segue regras simples, o que torna a especificação e verificação de propriedades semânticas para programas em execução no EVM mais fácil.
Ciclo de desenvolvimento mais rápido
Técnicas de verificação formal, como verificação de modelo e execução simbólica, geralmente são mais eficientes do que a análise regular do código de contrato inteligente (realizada durante testes ou auditorias). Isso ocorre porque a verificação formal depende de valores simbólicos para testar asserções ("e se um usuário tentar sacar n éter?") ao contrário dos testes que usam valores concretos ("e se um usuário tentar sacar 5 éter?").
Variáveis de entrada simbólicas podem abranger várias classes de valores concretos, de modo que abordagens de verificação formal prometem cobertura de código maior em um período de tempo mais curto. Quando usada de forma eficaz, a verificação formal pode acelerar o ciclo de desenvolvimento para os desenvolvedores.
A verificação formal também melhora o processo de construção de aplicativos descentralizados (dapps) ao reduzir erros de design custosos. Atualizar contratos (quando possível) para corrigir vulnerabilidades requer uma extensa reescrita de bases de código e mais esforço gasto no desenvolvimento. A verificação formal pode detectar muitos erros na implementação de contratos que podem passar despercebidos por testadores e auditores, e fornece ampla oportunidade para corrigir esses problemas antes de implantar um contrato.
DESVANTAGENS DA VERIFICAÇÃO FORMAL
Custo da mão de obra manual
A verificação formal, especialmente a verificação semi-automatizada na qual um humano orienta o provador para derivar provas de correção, requer um trabalho manual considerável. Além disso, criar uma especificação formal é uma atividade complexa que exige um alto nível de habilidade.
Esses fatores (esforço e habilidade) tornam a verificação formal mais exigente e cara em comparação com os métodos usuais de avaliação de correção em contratos, como testes e auditorias. No entanto, pagar o custo por uma auditoria de verificação completa é prático, dada o custo dos erros nas implementações de contratos inteligentes.
Falsos negativos
A verificação formal só pode verificar se a execução do contrato inteligente corresponde à especificação formal. Como tal, é importante garantir que a especificação descreva adequadamente os comportamentos esperados de um contrato inteligente.
Se as especificações forem mal escritas, violações de propriedades - que apontam para execuções vulneráveis - não podem ser detectadas pela auditoria de verificação formal. Nesse caso, um desenvolvedor pode erroneamente assumir que o contrato está livre de bugs.
Problemas de desempenho
A verificação formal encontra uma série de problemas de desempenho. Por exemplo, problemas de explosão de estado e caminho encontrados durante a verificação de modelos e verificação simbólica, respectivamente, podem afetar os procedimentos de verificação. Além disso, as ferramentas de verificação formal frequentemente utilizam solucionadores SMT e outros solucionadores de restrições em sua camada subjacente, e esses solucionadores dependem de procedimentos computacionalmente intensivos.
Além disso, nem sempre é possível para os verificadores de programas determinar se uma propriedade (descrita como uma fórmula lógica) pode ser satisfeita ou não (oproblema de decidibilidade
") porque um programa pode nunca terminar. Como tal, pode ser impossível provar algumas propriedades para um contrato mesmo que esteja bem especificado.
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES DO ETHEREUM
Linguagens de especificação para criar especificações formais
Act: O Act permite a especificação de atualizações de armazenamento, condições pré/pós e invariantes de contrato. Sua suíte de ferramentas também possui backends de prova capazes de provar muitas propriedades via Coq, solucionadores SMT ou hevm.
Scribble - O Scribble transforma anotações de código na linguagem de especificação Scribble em assertivas concretas que verificam a especificação.
Dafny - Dafny é uma linguagem de programação pronta para verificação que depende de anotações de alto nível para raciocinar e provar a correção do código.
Verificadores de programas para verificar a correção
Certora Prover - Certora Prover é uma ferramenta automática de verificação formal para verificar a correção do código em contratos inteligentes. As especificações são escritas em CVL (Linguagem de Verificação Certora), com violações de propriedade detectadas usando uma combinação de análise estática e resolução de restrições.
Solidity SMTChecker - O SMTChecker do Solidity é um verificador de modelo integrado baseado em SMT (Satisfabilidade Modulo Theories) e resolução de Horn. Ele confirma se o código fonte de um contrato corresponde às especificações durante a compilação e verifica estaticamente as violações das propriedades de segurança.
solc-verify - solc-verify é uma versão estendida do compilador Solidity que pode realizar verificação formal automatizada de código Solidity usando anotações e verificação de programa modular.
KEVM - KEVM é uma semântica formal da Máquina Virtual Ethereum (EVM) escrita no framework K. KEVM é executável e pode provar certas afirmações relacionadas a propriedades usando lógica de alcançabilidade.
Estruturas lógicas para prova de teoremas
Isabelle - Isabelle/HOL é um assistente de prova que permite que fórmulas matemáticas sejam expressas em uma linguagem formal e fornece ferramentas para provar essas fórmulas. A principal aplicação é a formalização de provas matemáticas e, em particular, a verificação formal, que inclui provar a correção do hardware ou software de computador e provar propriedades de linguagens de computador e protocolos.
Coq - Coq é um provador de teoremas interativo que permite que você defina programas usando teoremas e gere interativamente provas verificadas por máquina de correção.
Ferramentas baseadas em execução simbólica para detectar padrões vulneráveis em contratos inteligentes
Manticore - Uma ferramenta para análise de bytecode EVM baseada em execução simbólica.
hevm - hevm é um mecanismo de execução simbólica e verificador de equivalência para bytecode EVM.
Mythril - Uma ferramenta de execução simbólica para detectar vulnerabilidades em contratos inteligentes Ethereum
Aviso Legal：
- Este artigo foi reproduzido de []. Todos os direitos autorais pertencem ao autor original [**]. Se houver objeções a esta reimpressão, entre em contato com o Gate Learnequipe e eles lidarão com isso prontamente.
- Isenção de Responsabilidade: As opiniões expressas neste artigo são exclusivamente do autor e não constituem aconselhamento de investimento.
- As traduções do artigo para outros idiomas são feitas pela equipe Gate Learn. Salvo indicação em contrário, copiar, distribuir ou plagiar os artigos traduzidos é proibido.
บทความที่เกี่ยวข้อง
O que é EtherVista, o autoproclamado "Novo Padrão para DEX"?
O que é Neiro? Tudo o que você precisa saber sobre NEIROETH