VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
Contratos inteligentesestão a tornar possível criar aplicações descentralizadas, sem confiança e robustas que introduzem novos casos de uso e desbloqueiam valor para os utilizadores. Como os contratos inteligentes lidam com grandes quantidades de valor, a segurança é uma consideração crítica para os programadores.
A verificação formal é uma das técnicas recomendadas para melhorar segurança de contratos inteligentesVerificação formal, que utilizamétodos formais
para a especificação, conceção e verificação de programas, tem sido utilizada há 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 cumpre 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á corretamente funcional.
O QUE É 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 permite-nos verificar se o comportamento de um sistema satisfaz alguns requisitos (ou seja, se 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á em conformidade com sua especificação e derivar uma prova matemática da correção do primeiro. Quando um contrato satisfaz sua especificação, é 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 a descrever como os resultados das funções são calculados dado 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, visualizando-os como sistemas que aceitam entradas e executam cálculos com base nessas entradas.
Os 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 blockchain. Esses 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 concentram-se 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. Os 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 aplicações de contratos inteligentes, como rastros de programas e gráficos de fluxo de controlo
, para raciocinar sobre propriedades relevantes para a execução de um contrato.
Os 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 na definição de propriedades críticas de segurança em contratos inteligentes e na deteção de vulnerabilidades potenciais.
O que é uma especificação formal?
Uma especificação é simplesmente um requisito técnico que um determinado sistema deve satisfazer. Na programação, as 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 numa especificação formal como uma coleção de declarações escritas numa linguagem formal que descrevem a execução pretendida de um smart contract. As especificações cobrem as propriedades de um contrato e definem como o contrato deve comportar-se em diferentes circunstâncias. O objetivo da verificação formal é determinar se um smart contract 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 propensos a vulnerabilidades que podem prejudicar a funcionalidade ou causar exploits maliciosos.
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
As especificações formais permitem o raciocínio matemático sobre a correção da execução do programa. Tal como acontece com modelos formais, as especificações formais podem captar propriedades de alto nível ou o comportamento de baixo nível de uma implementação de contrato.
As especificações formais são derivadas usando elementos de lógica do 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
As especificações formais para contratos inteligentes podem ser classificadas amplamente como especificações de nível alto ou baixo. Independentemente da categoria a que uma especificação pertença, ela 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 ao modelo”) descreve o comportamento de alto nível de um programa. As especificações de alto nível modelam um contrato inteligente como um máquina de estados finitos
(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 estarei com fome")." Quando aplicadas à verificação formal, lógicas temporais são usadas para afirmar sobre o comportamento correto de sistemas modelados como máquinas de estados. Especificamente, uma lógica temporal descreve os estados futuros em que um contrato inteligente pode estar e como 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 mau acontece” e geralmente expressam invariância. Uma propriedade de segurança pode definir requisitos gerais de software, como 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).
Por exemplo, considere este requisito de segurança que abrange as condições para usar o transfer() ou transferFrom() nos contratos de tokens ERC-20: "O saldo do remetente nunca é inferior à quantidade solicitada de tokens a ser enviada.". Esta descrição em linguagem natural de um invariante de contrato pode ser traduzida para uma especificação formal (matemática), que pode então ser verificada rigorosamente quanto à validade.
As propriedades de vivacidade afirmam que "algo de bom acontece eventualmente" e dizem respeito à capacidade de um contrato de progredir através de diferentes estados. Um exemplo de propriedade de vivacidade é "liquidez", que se refere à capacidade de um contrato de transferir seus saldos para os usuários mediante solicitação. Se esta propriedade for violada, os usuários não seriam capazes de retirar os ativos armazenados no contrato, como aconteceu com o Incidente da carteira de paridade
.
Especificações de baixo nível
Especificações de alto nível partem de um modelo de estado finito de um contrato e definem as propriedades desejadas desse modelo. Em contraste, especificações de baixo nível (também chamadas de "especificações orientadas à propriedade") frequentemente modelam programas (contratos inteligentes) como sistemas compostos por 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 os rastros do programa e tentam definir propriedades de um contrato inteligente ao longo desses rastros. Os rastros referem-se a sequências de execuções de funções que alteram o estado de um contrato inteligente; assim, as especificações de baixo nível ajudam a especificar os requisitos para a execução interna de um contrato.
Especificações formais de baixo nível podem ser fornecidas tanto como propriedades no estilo Hoare ou invariáveis nos caminhos de execução.
Propriedades no estilo de 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 utilizadores que chamam o contrato devem satisfazer este requisito. Uma pós-condição é um predicado que descreve a condição que uma função estabelece se for executada corretamente; os utilizadores podem esperar que esta 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, não muda).
As especificações no estilo Hoare podem garantir a correção parcial ou total. 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 for verdadeira. A prova da correção total é obtida se uma pré-condição for verdadeira antes da execução da função, a execução for garantida para terminar e, quando o fizer, a pós-condição for verdadeira.
Obter uma prova de correção total é difícil, uma vez que algumas execuções podem atrasar antes de terminar, ou nunca terminar. Dito isto, a questão de saber se a execução termina é, sem dúvida, um ponto discutível, uma vez que o mecanismo de gás do Ethereum impede loops de programa infinitos (a execução termina com sucesso ou termina devido a um erro de 'falta de gás').
As especificações do contrato inteligente criadas 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). Dessa maneira, 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 no Solidity.
as declarações de exigência expressam uma condição prévia ou invariante e são frequentemente utilizadas para validar as entradas do utilizador, enquanto o assert captura uma pós-condição necessária para a segurança. Por exemplo, o controlo de acesso adequado para funções (um exemplo de uma propriedade de segurança) pode ser alcançado utilizando require como uma verificação de pré-condição na identidade da conta chamadora. Da mesma forma, uma invariante sobre valores admissíveis de variáveis de estado num contrato (por exemplo, o número total de tokens em circulação) pode ser protegida contra violações utilizando 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 transitam 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 num 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, um grafo de fluxo de controlo
(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 traço representado como um caminho no grafo de fluxo de controle.
Principalmente, as especificações de nível de rastreio são usadas para raciocinar sobre padrões de execução interna em contratos inteligentes. Ao criar especificações de nível de rastreio, afirmamos os caminhos de execução admissíveis (ou seja, transições de estado) para um contrato inteligente. Usando técnicas, como 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 publicamente acessíveis para descrever propriedades de nível de rastreamento. Aqui, assumimos que o contrato DAO permite que os usuários realizem as seguintes operações:
- Depositar fundos
- Votar numa proposta após depositar fundos
- Reivindique um reembolso se não votarem numa proposta
Os exemplos de propriedades de nível de rastreamento podem ser "os usuários que não depositam fundos não podem votar em uma proposta" ou "os usuários que não votam em uma proposta devem sempre ser capazes de solicitar um reembolso". Ambas as propriedades afirmam sequências de execução preferidas (a votação não pode ocorrer antes do depósito de fundos e a reivindicação de reembolso não pode ocorrer depois de votar em uma proposta).
TÉCNICAS DE VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
Verificação de modelos
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 estado, enquanto as propriedades dos estados de contrato permitidos são definidos usando lógica temporal.
A verificação de modelos 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 fundamentadas emlógica proposicional
. Isto simplifica a tarefa do algoritmo de verificação de modelos, ou seja, provar que um modelo matemático satisfaz uma determinada fórmula lógica.
A verificação de modelos na verificação formal é principalmente usada 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, que explicamos anteriormente.
Por exemplo, uma propriedade de segurança relacionada ao controle de acesso (por exemplo, Apenas o proprietário do contrato pode chamar selfdestruct) pode ser escrita em lógica formal. Posteriormente, o algoritmo de verificação de modelo pode verificar se o contrato satisfaz esta especificação formal.
A verificação de modelos utiliza 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 teorema é verificar a equivalência lógica entre essas afirmações. "Equivalência lógica" (também chamada de "biimplicação lógica") é um tipo de relação entre duas afirmações, de tal forma 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 afirmações sobre o modelo de um contrato e sua propriedade é formulada como uma afirmação prová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 se contrai como sistemas de transição com estados finitos, a prova de teorema pode lidar com a análise de sistemas de estados infinitos. No entanto, isso significa que um provador de teorema automatizado 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-o mais caro de usar do que a verificação de modelos, que é totalmente automatizada.
Execução simbólica
A execução simbólica é um método de análise de 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 de nível de rastreamento no código de um contrato.
A execução simbólica representa uma traçado de execução como uma fórmula matemática sobre valores de entrada simbólicos, também chamada de predicado de caminho. 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 aciona a execução em direção a esse caminho.
Suponha que a função de um contrato inteligente recebe como entrada um valor uint (x) e reverte quando x é maior que 5 e também menor que 10. Encontrar um valor para x que desencadeia o erro usando um procedimento de teste normal exigiria percorrer dezenas de casos de teste (ou mais) sem a garantia de realmente encontrar uma entrada que desencadeie o erro.
Pelo contrário, 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 do caminho associado x = X > 5 ∧ X < 10 seria então dado a um solucionador SMT para resolver. Se um valor específico satisfizer a fórmula x = X > 5 ∧ X < 10, o solucionador SMT o calculará - por exemplo, o solucionador poderia produzir 7 como um valor para x.
Porque 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 os testes regulares para encontrar 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 aciona o erro e reproduzir 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 transbordamento:
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, logo, ela serve como 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 a perdas irreparáveis para os utilizadores
. Verificar formalmente um contrato antes da implantação, no entanto, pode aumentar as garantias de que ele funcionará como esperado uma vez em execução na blockchain.
A fiabilidade é uma qualidade muito 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 fiabilidade dos contratos torna a verificação formal necessária. A verificação formal é capaz de detetar problemas complicados, como subfluxos e sobrefluxos de inteiros, reentrância e otimizações de gás pobres, que podem escapar aos auditores e testadores.
Provar a correção funcional
A realização de testes de programa é o método mais comum para provar que um contrato inteligente satisfaz alguns requisitos. Isso envolve a execução de um contrato com uma amostra dos dados que se espera que ele manipule e analisar o seu comportamento. Se o contrato devolver os resultados esperados para os dados de amostra, então os desenvolvedores têm prova objetiva da sua correção.
No entanto, esta 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 detetar bugs (ou seja, se alguns caminhos de código falharem ao devolver os resultados desejados durante a execução), mas não pode provar conclusivamente a ausência de bugs.
Pelo contrário, a verificação formal pode provar formalmente que um contrato inteligente satisfaz os requisitos para uma gama infinita de execuções sem executar o contrato de todo. 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. Então 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 satisfaz os 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 perspetivas de provar que um contrato é funcionalmente correto em relação a uma especificação.
Alvos ideais de verificação
Um alvo de verificação descreve o sistema a ser formalmente verificado. A verificação formal é melhor utilizada em “sistemas embarcados” (pequenas e simples partes de software que fazem parte de um sistema maior). Também são ideais para domínios especializados que têm poucas regras, pois isso facilita a modificação de ferramentas para verificar propriedades específicas do domínio.
Os contratos inteligentes - pelo menos, em certa medida - cumprem ambos os requisitos. Por exemplo, o tamanho pequeno dos contratos Ethereum torna-os adequados para verificação formal. Da mesma forma, o EVM segue regras simples, o que torna mais fácil especificar e verificar propriedades semânticas para programas em execução no EVM.
Ciclo de desenvolvimento mais rápido
Técnicas de verificação formal, como verificação de modelos e execução simbólica, são geralmente mais eficientes do que a análise regular do código de contrato inteligente (realizada durante testes ou auditorias). Isto porque a verificação formal depende de valores simbólicos para testar asserções ("e se um utilizador tentar levantar n éter?") ao contrário dos testes que utilizam valores concretos ("e se um utilizador tentar levantar 5 éter?").
As variáveis de entrada simbólicas podem abranger múltiplas classes de valores concretos, portanto, as abordagens de verificação formal prometem uma cobertura de código maior num período de tempo mais curto. Quando utilizado de forma eficaz, a verificação formal pode acelerar o ciclo de desenvolvimento para os programadores.
A verificação formal também melhora o processo de construção de aplicações descentralizadas (dapps) ao reduzir erros de design dispendiosos. A atualização de 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 detetar muitos erros na implementação de contratos que podem escapar aos testadores e auditores e fornece ampla oportunidade para corrigir esses problemas antes de implementar um contrato.
DESVANTAGENS DA VERIFICAÇÃO FORMAL
Custo da mão de obra manual
A verificação formal, especialmente a verificação semi-automatizada em que um humano guia 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.
Estes fatores (esforço e habilidade) tornam a verificação formal mais exigente e dispendiosa em comparação com os métodos usuais de avaliação da correção em contratos, como testes e auditorias. No entanto, pagar o custo por uma auditoria de verificação completa é prático, dadas as consequências 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 estiverem mal escritas, as violações das propriedades — que apontam para execuções vulneráveis — não podem ser detetadas pela auditoria de verificação formal. Neste caso, um programador pode assumir erroneamente 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 do modelo e a verificação simbólica, respetivamente, podem afetar os procedimentos de verificação. Além disso, as ferramentas de verificação formal muitas vezes 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 programa determinar se uma propriedade (descrita como uma fórmula lógica) pode ser satisfeita ou não (o “problema da decidibilidade
“) because a program might never terminate. As such, it may be impossible to prove some properties for a contract even if it’s well-specified.
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES ETHEREUM
Línguas 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. A sua suite 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 (Certora Verification Language), com violações de propriedade detetadas 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 incorporado baseado em SMT (Satisfiability Modulo Theories) e resolução de Horn. 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 no 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 na estrutura K. KEVM é executável e pode provar certas afirmações relacionadas com propriedades usando lógica de alcançabilidade.
Estruturas lógicas para provas 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, 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 detetar padrões vulneráveis em contratos inteligentes
Manticore - Uma ferramenta para analisar a análise de bytecode EVM com base em execução simbólica.
hevm - hevm é um motor de execução simbólica e verificador de equivalência para bytecode EVM.
Mythril - Uma ferramenta de execução simbólica para detetar vulnerabilidades em contratos inteligentes Ethereum
Aviso Legal：
- Este artigo é republicado a partir de []. Todos os direitos autorais pertencem ao autor original [**]. Se houver objeções a esta reimpressão, entre em contato com o Gate Learnequipa e eles tratarão disso prontamente.
- Aviso de responsabilidade: As opiniões expressas neste artigo são exclusivamente as do autor e não constituem qualquer conselho de investimento.
- As traduções do artigo para outros idiomas são feitas pela equipe Gate Learn. A menos que mencionado, copiar, distribuir ou plagiar os artigos traduzidos é proibido.
Artigos relacionados
O que é o Ethereum 2.0? Entender a Mesclagem
O que é o EtherVista, o "Novo Padrão para DEX" auto-proclamado?
O que é a Rocket Pool?
VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
O QUE É A VERIFICAÇÃO FORMAL?
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
TÉCNICAS DE VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
DESADVANTAGENS DA VERIFICAÇÃO FORMAL
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES ETHEREUM
Contratos inteligentesestão a tornar possível criar aplicações descentralizadas, sem confiança e robustas que introduzem novos casos de uso e desbloqueiam valor para os utilizadores. Como os contratos inteligentes lidam com grandes quantidades de valor, a segurança é uma consideração crítica para os programadores.
A verificação formal é uma das técnicas recomendadas para melhorar segurança de contratos inteligentesVerificação formal, que utilizamétodos formais
para a especificação, conceção e verificação de programas, tem sido utilizada há 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 cumpre 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á corretamente funcional.
O QUE É 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 permite-nos verificar se o comportamento de um sistema satisfaz alguns requisitos (ou seja, se 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á em conformidade com sua especificação e derivar uma prova matemática da correção do primeiro. Quando um contrato satisfaz sua especificação, é 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 a descrever como os resultados das funções são calculados dado 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, visualizando-os como sistemas que aceitam entradas e executam cálculos com base nessas entradas.
Os 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 blockchain. Esses 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 concentram-se 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. Os 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 aplicações de contratos inteligentes, como rastros de programas e gráficos de fluxo de controlo
, para raciocinar sobre propriedades relevantes para a execução de um contrato.
Os 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 na definição de propriedades críticas de segurança em contratos inteligentes e na deteção de vulnerabilidades potenciais.
O que é uma especificação formal?
Uma especificação é simplesmente um requisito técnico que um determinado sistema deve satisfazer. Na programação, as 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 numa especificação formal como uma coleção de declarações escritas numa linguagem formal que descrevem a execução pretendida de um smart contract. As especificações cobrem as propriedades de um contrato e definem como o contrato deve comportar-se em diferentes circunstâncias. O objetivo da verificação formal é determinar se um smart contract 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 propensos a vulnerabilidades que podem prejudicar a funcionalidade ou causar exploits maliciosos.
TIPOS DE ESPECIFICAÇÕES FORMAIS PARA CONTRATOS INTELIGENTES
As especificações formais permitem o raciocínio matemático sobre a correção da execução do programa. Tal como acontece com modelos formais, as especificações formais podem captar propriedades de alto nível ou o comportamento de baixo nível de uma implementação de contrato.
As especificações formais são derivadas usando elementos de lógica do 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
As especificações formais para contratos inteligentes podem ser classificadas amplamente como especificações de nível alto ou baixo. Independentemente da categoria a que uma especificação pertença, ela 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 ao modelo”) descreve o comportamento de alto nível de um programa. As especificações de alto nível modelam um contrato inteligente como um máquina de estados finitos
(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 estarei com fome")." Quando aplicadas à verificação formal, lógicas temporais são usadas para afirmar sobre o comportamento correto de sistemas modelados como máquinas de estados. Especificamente, uma lógica temporal descreve os estados futuros em que um contrato inteligente pode estar e como 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 mau acontece” e geralmente expressam invariância. Uma propriedade de segurança pode definir requisitos gerais de software, como 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).
Por exemplo, considere este requisito de segurança que abrange as condições para usar o transfer() ou transferFrom() nos contratos de tokens ERC-20: "O saldo do remetente nunca é inferior à quantidade solicitada de tokens a ser enviada.". Esta descrição em linguagem natural de um invariante de contrato pode ser traduzida para uma especificação formal (matemática), que pode então ser verificada rigorosamente quanto à validade.
As propriedades de vivacidade afirmam que "algo de bom acontece eventualmente" e dizem respeito à capacidade de um contrato de progredir através de diferentes estados. Um exemplo de propriedade de vivacidade é "liquidez", que se refere à capacidade de um contrato de transferir seus saldos para os usuários mediante solicitação. Se esta propriedade for violada, os usuários não seriam capazes de retirar os ativos armazenados no contrato, como aconteceu com o Incidente da carteira de paridade
.
Especificações de baixo nível
Especificações de alto nível partem de um modelo de estado finito de um contrato e definem as propriedades desejadas desse modelo. Em contraste, especificações de baixo nível (também chamadas de "especificações orientadas à propriedade") frequentemente modelam programas (contratos inteligentes) como sistemas compostos por 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 os rastros do programa e tentam definir propriedades de um contrato inteligente ao longo desses rastros. Os rastros referem-se a sequências de execuções de funções que alteram o estado de um contrato inteligente; assim, as especificações de baixo nível ajudam a especificar os requisitos para a execução interna de um contrato.
Especificações formais de baixo nível podem ser fornecidas tanto como propriedades no estilo Hoare ou invariáveis nos caminhos de execução.
Propriedades no estilo de 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 utilizadores que chamam o contrato devem satisfazer este requisito. Uma pós-condição é um predicado que descreve a condição que uma função estabelece se for executada corretamente; os utilizadores podem esperar que esta 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, não muda).
As especificações no estilo Hoare podem garantir a correção parcial ou total. 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 for verdadeira. A prova da correção total é obtida se uma pré-condição for verdadeira antes da execução da função, a execução for garantida para terminar e, quando o fizer, a pós-condição for verdadeira.
Obter uma prova de correção total é difícil, uma vez que algumas execuções podem atrasar antes de terminar, ou nunca terminar. Dito isto, a questão de saber se a execução termina é, sem dúvida, um ponto discutível, uma vez que o mecanismo de gás do Ethereum impede loops de programa infinitos (a execução termina com sucesso ou termina devido a um erro de 'falta de gás').
As especificações do contrato inteligente criadas 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). Dessa maneira, 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 no Solidity.
as declarações de exigência expressam uma condição prévia ou invariante e são frequentemente utilizadas para validar as entradas do utilizador, enquanto o assert captura uma pós-condição necessária para a segurança. Por exemplo, o controlo de acesso adequado para funções (um exemplo de uma propriedade de segurança) pode ser alcançado utilizando require como uma verificação de pré-condição na identidade da conta chamadora. Da mesma forma, uma invariante sobre valores admissíveis de variáveis de estado num contrato (por exemplo, o número total de tokens em circulação) pode ser protegida contra violações utilizando 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 transitam 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 num 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, um grafo de fluxo de controlo
(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 traço representado como um caminho no grafo de fluxo de controle.
Principalmente, as especificações de nível de rastreio são usadas para raciocinar sobre padrões de execução interna em contratos inteligentes. Ao criar especificações de nível de rastreio, afirmamos os caminhos de execução admissíveis (ou seja, transições de estado) para um contrato inteligente. Usando técnicas, como 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 publicamente acessíveis para descrever propriedades de nível de rastreamento. Aqui, assumimos que o contrato DAO permite que os usuários realizem as seguintes operações:
- Depositar fundos
- Votar numa proposta após depositar fundos
- Reivindique um reembolso se não votarem numa proposta
Os exemplos de propriedades de nível de rastreamento podem ser "os usuários que não depositam fundos não podem votar em uma proposta" ou "os usuários que não votam em uma proposta devem sempre ser capazes de solicitar um reembolso". Ambas as propriedades afirmam sequências de execução preferidas (a votação não pode ocorrer antes do depósito de fundos e a reivindicação de reembolso não pode ocorrer depois de votar em uma proposta).
TÉCNICAS DE VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
Verificação de modelos
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 estado, enquanto as propriedades dos estados de contrato permitidos são definidos usando lógica temporal.
A verificação de modelos 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 fundamentadas emlógica proposicional
. Isto simplifica a tarefa do algoritmo de verificação de modelos, ou seja, provar que um modelo matemático satisfaz uma determinada fórmula lógica.
A verificação de modelos na verificação formal é principalmente usada 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, que explicamos anteriormente.
Por exemplo, uma propriedade de segurança relacionada ao controle de acesso (por exemplo, Apenas o proprietário do contrato pode chamar selfdestruct) pode ser escrita em lógica formal. Posteriormente, o algoritmo de verificação de modelo pode verificar se o contrato satisfaz esta especificação formal.
A verificação de modelos utiliza 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 teorema é verificar a equivalência lógica entre essas afirmações. "Equivalência lógica" (também chamada de "biimplicação lógica") é um tipo de relação entre duas afirmações, de tal forma 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 afirmações sobre o modelo de um contrato e sua propriedade é formulada como uma afirmação prová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 se contrai como sistemas de transição com estados finitos, a prova de teorema pode lidar com a análise de sistemas de estados infinitos. No entanto, isso significa que um provador de teorema automatizado 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-o mais caro de usar do que a verificação de modelos, que é totalmente automatizada.
Execução simbólica
A execução simbólica é um método de análise de 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 de nível de rastreamento no código de um contrato.
A execução simbólica representa uma traçado de execução como uma fórmula matemática sobre valores de entrada simbólicos, também chamada de predicado de caminho. 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 aciona a execução em direção a esse caminho.
Suponha que a função de um contrato inteligente recebe como entrada um valor uint (x) e reverte quando x é maior que 5 e também menor que 10. Encontrar um valor para x que desencadeia o erro usando um procedimento de teste normal exigiria percorrer dezenas de casos de teste (ou mais) sem a garantia de realmente encontrar uma entrada que desencadeie o erro.
Pelo contrário, 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 do caminho associado x = X > 5 ∧ X < 10 seria então dado a um solucionador SMT para resolver. Se um valor específico satisfizer a fórmula x = X > 5 ∧ X < 10, o solucionador SMT o calculará - por exemplo, o solucionador poderia produzir 7 como um valor para x.
Porque 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 os testes regulares para encontrar 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 aciona o erro e reproduzir 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 transbordamento:
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, logo, ela serve como 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 a perdas irreparáveis para os utilizadores
. Verificar formalmente um contrato antes da implantação, no entanto, pode aumentar as garantias de que ele funcionará como esperado uma vez em execução na blockchain.
A fiabilidade é uma qualidade muito 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 fiabilidade dos contratos torna a verificação formal necessária. A verificação formal é capaz de detetar problemas complicados, como subfluxos e sobrefluxos de inteiros, reentrância e otimizações de gás pobres, que podem escapar aos auditores e testadores.
Provar a correção funcional
A realização de testes de programa é o método mais comum para provar que um contrato inteligente satisfaz alguns requisitos. Isso envolve a execução de um contrato com uma amostra dos dados que se espera que ele manipule e analisar o seu comportamento. Se o contrato devolver os resultados esperados para os dados de amostra, então os desenvolvedores têm prova objetiva da sua correção.
No entanto, esta 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 detetar bugs (ou seja, se alguns caminhos de código falharem ao devolver os resultados desejados durante a execução), mas não pode provar conclusivamente a ausência de bugs.
Pelo contrário, a verificação formal pode provar formalmente que um contrato inteligente satisfaz os requisitos para uma gama infinita de execuções sem executar o contrato de todo. 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. Então 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 satisfaz os 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 perspetivas de provar que um contrato é funcionalmente correto em relação a uma especificação.
Alvos ideais de verificação
Um alvo de verificação descreve o sistema a ser formalmente verificado. A verificação formal é melhor utilizada em “sistemas embarcados” (pequenas e simples partes de software que fazem parte de um sistema maior). Também são ideais para domínios especializados que têm poucas regras, pois isso facilita a modificação de ferramentas para verificar propriedades específicas do domínio.
Os contratos inteligentes - pelo menos, em certa medida - cumprem ambos os requisitos. Por exemplo, o tamanho pequeno dos contratos Ethereum torna-os adequados para verificação formal. Da mesma forma, o EVM segue regras simples, o que torna mais fácil especificar e verificar propriedades semânticas para programas em execução no EVM.
Ciclo de desenvolvimento mais rápido
Técnicas de verificação formal, como verificação de modelos e execução simbólica, são geralmente mais eficientes do que a análise regular do código de contrato inteligente (realizada durante testes ou auditorias). Isto porque a verificação formal depende de valores simbólicos para testar asserções ("e se um utilizador tentar levantar n éter?") ao contrário dos testes que utilizam valores concretos ("e se um utilizador tentar levantar 5 éter?").
As variáveis de entrada simbólicas podem abranger múltiplas classes de valores concretos, portanto, as abordagens de verificação formal prometem uma cobertura de código maior num período de tempo mais curto. Quando utilizado de forma eficaz, a verificação formal pode acelerar o ciclo de desenvolvimento para os programadores.
A verificação formal também melhora o processo de construção de aplicações descentralizadas (dapps) ao reduzir erros de design dispendiosos. A atualização de 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 detetar muitos erros na implementação de contratos que podem escapar aos testadores e auditores e fornece ampla oportunidade para corrigir esses problemas antes de implementar um contrato.
DESVANTAGENS DA VERIFICAÇÃO FORMAL
Custo da mão de obra manual
A verificação formal, especialmente a verificação semi-automatizada em que um humano guia 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.
Estes fatores (esforço e habilidade) tornam a verificação formal mais exigente e dispendiosa em comparação com os métodos usuais de avaliação da correção em contratos, como testes e auditorias. No entanto, pagar o custo por uma auditoria de verificação completa é prático, dadas as consequências 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 estiverem mal escritas, as violações das propriedades — que apontam para execuções vulneráveis — não podem ser detetadas pela auditoria de verificação formal. Neste caso, um programador pode assumir erroneamente 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 do modelo e a verificação simbólica, respetivamente, podem afetar os procedimentos de verificação. Além disso, as ferramentas de verificação formal muitas vezes 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 programa determinar se uma propriedade (descrita como uma fórmula lógica) pode ser satisfeita ou não (o “problema da decidibilidade
“) because a program might never terminate. As such, it may be impossible to prove some properties for a contract even if it’s well-specified.
FERRAMENTAS DE VERIFICAÇÃO FORMAL PARA CONTRATOS INTELIGENTES ETHEREUM
Línguas 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. A sua suite 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 (Certora Verification Language), com violações de propriedade detetadas 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 incorporado baseado em SMT (Satisfiability Modulo Theories) e resolução de Horn. 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 no 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 na estrutura K. KEVM é executável e pode provar certas afirmações relacionadas com propriedades usando lógica de alcançabilidade.
Estruturas lógicas para provas 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, 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 detetar padrões vulneráveis em contratos inteligentes
Manticore - Uma ferramenta para analisar a análise de bytecode EVM com base em execução simbólica.
hevm - hevm é um motor de execução simbólica e verificador de equivalência para bytecode EVM.
Mythril - Uma ferramenta de execução simbólica para detetar vulnerabilidades em contratos inteligentes Ethereum
Aviso Legal：
- Este artigo é republicado a partir de []. Todos os direitos autorais pertencem ao autor original [**]. Se houver objeções a esta reimpressão, entre em contato com o Gate Learnequipa e eles tratarão disso prontamente.
- Aviso de responsabilidade: As opiniões expressas neste artigo são exclusivamente as do autor e não constituem qualquer conselho de investimento.
- As traduções do artigo para outros idiomas são feitas pela equipe Gate Learn. A menos que mencionado, copiar, distribuir ou plagiar os artigos traduzidos é proibido.
Artigos relacionados
O que é o Ethereum 2.0? Entender a Mesclagem
O que é o EtherVista, o "Novo Padrão para DEX" auto-proclamado?