Analisamos a verificação formal e a execução simbólica com dois membros da equipe de segurança Web3 da Trail of Bits. Além disso, revisamos o valor que essas técnicas trazem e as comparamos a outras ferramentas.
Verificação formal com a Trail of Bits
Um enorme agradecimento a Troy e Josselin da Trail of Bits por dedicarem seu tempo a esta entrevista. Além disso, um agradecimento especial a Hari, Runtime Verification, Leo Alt e Palina por sua ajuda na compreensão desses conceitos e por seu trabalho na área.
Você pode ver a entrevista completa com o Troy aqui.
Você pode ver a entrevista completa com o Josselin aqui.
Introdução
Assista ao vídeo aqui.
A verificação formal é o ato de provar ou refutar uma determinada propriedade de um sistema usando um modelo matemático.
A execução simbólica é uma técnica usada para a verificação formal. A execução simbólica explora os diferentes caminhos em um programa, criando uma representação matemática para cada caminho.
Dito de forma simples, a execução simbólica é a conversão do seu código em um conjunto de expressões matemáticas. Ou, ainda mais claramente, a transformação do seu código em matemática.
É esta a bala de prata para sua jornada de auditoria? Vamos descobrir.
A Equipe
Miniatura da entrevista com Josselin
Tive o imenso prazer de entrevistar o chefe de engenharia de blockchain da Trail of Bits, Josselin, e o engenheiro de segurança da Trail of Bits, Troy, sobre metodologias de teste e verificação formal. Tenho links para as entrevistas completas com ambos (Troy, Josselin) se você quiser assistir!
Para entender o que são verificação formal e execução simbólica, precisamos de uma rápida revisão sobre alguns dos testes na Web3. Se você não viu meu vídeo sobre o teste de invariante, certifique-se de assisti-lo antes de ler isso.
Ao testar, quais ferramentas usamos para ter alta confiança de que nosso programa funciona da maneira que desejamos?
Camada 0 | Revisão Manual
Todo auditor e engenheiro de contrato inteligente deve ser capaz de revisar manualmente seu próprio código. O ChatGPT não é bom o suficiente. A revisão manual é ótima, mas precisamos ter certeza de que não dependemos apenas de humanos para obter resultados; precisamos ter processos automatizados para termos mais garantias de que os bugs serão encontrados.
Camada 1 | Teste Unitário
Obviamente, você tem testes unitários, que testam algo muito específico. Ter um teste unitário para cada linha do seu código lhe dará uma boa cobertura de código. E é o mínimo absoluto para testes.
Função de Exemplo do Solidity
Se o exemplo acima for nosso código Solidity, nossa função setNumber deve definir number como newNumber. Um teste unitário seria capaz de detectar isso.
Resultado do teste unitário do Foundry
E se estivermos usando o Foundry, poderíamos obter uma saída que se parece com a acima.
Se um teste falhar, isso significa que nosso teste detectou um problema, e podemos voltar ao nosso código para corrigi-lo.
A maioria dos frameworks, como Foundry, Hardhat, Apeworx, Truffle e Brownie, têm a capacidade de realizar testes unitários.
Camada 2 | Teste de Fuzzing
O fuzzing é onde você pega entradas aleatórias e as executa em seu programa. Portanto, você deve definir coisas em seu código que deseja que sejam sempre verdadeiras.
O teste de fuzzing é o novo mínimo absoluto para a segurança Web3.
Porque eu digo que é.
Se você ainda não assistiu ao meu vídeo sobre fuzzing... Faça isso!
Para testes de fuzzing/invariante/propriedade, você precisa entender a propriedade ou invariante do seu sistema para fazer o fuzzing. Uma vez que você tenha sua propriedade definida, jogue dados aleatórios em seu sistema para quebrar essa propriedade. Se você encontrar algo que a quebre, você sabe que tem um caso extremo que precisa ser refatorado no seu código.
Foundry, Echidna e Consensys Diligence incorporam ferramentas de fuzzing (fuzzers).
Camada 3 | Análise Estática
Testes unitários e testes de fuzzing são conhecidos como testes dinâmicos. Dinâmico significa que você está realmente fazendo algo, como realmente executando nosso código.
Troy
Na análise estática, apenas olhamos nosso código ou temos alguma ferramenta que analise nosso código. Por exemplo, este código aqui tem uma vulnerabilidade clássica de reentrância em nossa função de saque.
Código Vulnerável
Se executarmos uma ferramenta de análise estática como o Slither, ela detectará automaticamente esse erro. Isso é ótimo para identificar rapidamente partes muito específicas do seu código que são conhecidas como práticas ruins.
Até mesmo o compilador Solidity pode ser considerado uma ferramenta de análise estática.
Camada 4 | Verificação Formal
A verificação formal é o ato de provar ou refutar uma determinada propriedade do sistema. Isso geralmente é feito por meio de um modelo matemático do sistema e da propriedade.
Aí está aquela palavra novamente, propriedade. Vê-se que quase independente do que você esteja fazendo em seus testes, você precisa entender as propriedades do seu sistema, e ali mesmo, Josselin nos deu algumas das características-chave entre o teste de fuzzing e a verificação formal.
- O teste de fuzzing tenta quebrar propriedades jogando dados aleatórios em seu sistema.
- A verificação formal tenta quebrar propriedades usando provas matemáticas.
Existem muitas maneiras diferentes de fazer a verificação formal, como:
- Execução simbólica
- Interpretação abstrata
- Verificação de Modelo
Para este blog, vamos nos concentrar na execução simbólica, pois atualmente é uma das maneiras mais populares usadas na Web3.
Execução Simbólica
Exemplo de exploração de caminho
Você pode aprender mais sobre execução simbólica em geral neste vídeo do MIT.
A execução simbólica é uma técnica onde você tenta explorar os diferentes caminhos do programa e representar esses caminhos como expressões matemáticas para tentar provar algo. Para cada caminho de execução, você vai criar uma representação matemática. Portanto, a primeira coisa que precisamos fazer é descobrir o que queremos provar ou refutar.
Exemplo de Código
Para nossa demonstração acima, vamos dizer que nosso invariante é que f nunca deve reverter, e é isso que vamos tentar provar ou refutar. Agora, isso pode parecer um exemplo bobo, mas você pode imaginar que essa era uma função chamada “sacar dinheiro”, e você quer que os usuários sempre consigam sacar seu dinheiro. O que pareceria um exemplo muito menos bobo.
Na execução simbólica, vamos converter essa função em uma representação matemática/lógica de cada caminho de execução de nosso código. Uma vez que temos um conjunto de funções matemáticas, podemos inseri-las em um solucionador (solver), que nos dirá se uma propriedade é verdadeira ou falsa, ou se nosso invariante é verdadeiro ou falso. Para usar a execução simbólica para verificação formal, seguimos estas etapas:
- Explore todos os caminhos possíveis
- Converta caminhos em expressões matemáticas
- Envie expressões matemáticas para um Solucionador SMT/SAT.
Explorando os caminhos
Visualização do processo de verificação formal com Execução Simbólica
Neste exemplo, temos 2 caminhos:
- Caminho 1: retornamos (a + 1)
- Caminho 2: a + 1 causa um overflow e nós reverteremos
Se passarmos o valor máximo de uint256 e tentarmos adicionar 1 a ele, o Solidity irá reverter (a partir de Solidity 0.8). Estes são os dois possíveis caminhos que nosso código pode tomar. Ferramentas de software podem encontrar esses caminhos automaticamente, mas mostraremos isso mais tarde.
Agora que temos nossos 2 caminhos, os convertemos em expressões matemáticas. Um dos conjuntos de expressões mais populares é convertê-los em um conjunto de booleanos, assim:
Caminho 1:
a < type(uint256).max
Caminho 2:
a == type(uint256).max
a + 1 < a
O Caminho 2 só pode ser alcançado se a > a + 1, uma vez que reverteremos quando 1 é adicionado a a. Este conjunto de booleanos será então colocado em um solucionador SAT, que tentará encontrar valores para a para fazer todos os booleanos serem verdadeiros. Se for capaz de encontrar um valor para a, considerará o grupo de booleanos "solucionável" ou sat.
Com nosso pequeno exemplo, você pode ver como é fácil fazer um grupo de booleanos, mas se obtivermos funções mais complexas, fica mais difícil. Queremos converter essa lista de booleanos para uma linguagem SMT-LIB para fornecer a um solucionador SAT, o exemplo acima poderia ser reescrito em SMT-LIB assim:
; Declare uma variável inteira simbólica 'a' como um inteiro de 256 bits
(declare-const a (_ BitVec 256))
; Crie um contexto para o Caminho 1
(push)
; Adicione asserções para o Caminho 1
; afirma que a não é igual a uint256.max
(assert (distinct a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
(check-sat)
; Remova o contexto para o Caminho 1
(pop)
; Crie um contexto para o Caminho 2
(push)
; Adicione asserções para o Caminho 2
; afirma que a é igual a uint256.max
(assert (= a #xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
; bvult é "bit vector unsigned less than", então estamos verificando que a + 1 é menor que a
(assert (bvult (bvadd a (_ bv1 256)) a))
; Verifique se o Caminho 2 é satisfatório
(check-sat)
Agora, se você pegar esse código e colá-lo em uma ferramenta como Z3 ou executá-lo localmente em sua máquina, o que lhe dará uma saída que se parece com algo assim:
Exemplo de Saída do Z3
As duas saídas sat indicam que foi possível encontrar uma entrada que torna o conjunto de booleanos de cada caminho verdadeiro. E uma vez que o caminho 2 reverte e nosso invariante é que ele nunca deve reverter, provamos que nosso invariante falha!
Hoje, eu criei este código do SMT-LIB manualmente com a ajuda do ChatGPT. No entanto, ferramentas de execução simbólica como Manticore, HEVM e até mesmo o verificador SMT do Solidity podem fornecer uma saída semelhante. Mas todas essas ferramentas vêm com um Z3 embutido. Então, elas até pulam a etapa de conversão em booleanos e simplesmente lhe dão a saída do solucionador SMT.
Se você deseja ver uma comparação detalhada de muitas das ferramentas disponíveis que fazem execução simbólica, confira este post da Palina.
Até mesmo o compilador Solidity em si pode realizar todo este processo nos bastidores:
- 1. Explorando os caminhos
- 2. Convertendo os caminhos em um conjunto de booleanos
- 3. Verificando se esses caminhos são alcançáveis ou não
Usando o compilador solc, podemos executar com o Model Checker Engine (Mecanismo de Verificação de Modelo) e procurar por um overflow.
Exemplo de execução do verificador SMT do solc
Ao executar isso, você verá que o compilador Solidity foi capaz de fazer uma execução simbólica. Agora, a reversão de operações é bem fácil de encontrar. No entanto, em vez disso, poderíamos procurar por asserts revertidos. Se a não é igual a um, execute novamente, mas em vez de overflow, procure por asserts.
Primeiro, adicionamos um assert em nosso código.
https://miro.medium.com/v2/resize:fit:1100/format:webp/1*OV3oMZ2yFvG5oRt1KksQgg.png
Adicionando um assert
Depois, execute o verificador solc procurando por asserts (invariantes) quebrados.
https://miro.medium.com/v2/resize:fit:1100/format:webp/1*2oOvna7dbWsH0cJ1QpZX5A.png
Verificador de assert do Solidity
E veríamos que, novamente, ele foi capaz de encontrar uma entrada para quebrar nosso assert matematicamente.
Recapitulação
Fizemos muita coisa aqui. Vamos recapitular.
- Criamos um código Solidity.
- Compreendemos nosso invariante.
- Usamos uma ferramenta de execução simbólica, como a incorporada no Solidity, para criar um conjunto de expressões booleanas que representam todos os caminhos de execução do nosso código (isso aconteceu de forma automática).
- Em seguida, os inserimos em um solucionador como o Z3 (nos bastidores) para ver se nossa propriedade poderia falhar apenas executando essa única função.
Nós passamos por um tutorial completo deste exemplo na entrevista com o Josselin, então certifique-se de conferir isso também se quiser aprender mais.
Não tenha medo se isso parecer um pouco complicado; não hesite em fazer perguntas e deixar comentários nas descrições.
Limitações
Miniatura da entrevista com Troy
Essa é uma bala de prata?
Não.
Às vezes, o servidor pode não conseguir resolver a questão também, como se a questão fosse muito complexa. Geralmente damos um tempo limite ao servidor devido à complexidade de algumas tarefas, como inverter uma função hash, o que desafia até mesmo os servidores mais robustos.
Josselin
Como qualquer tecnologia, essas não são abordagens que servem para todos os tamanhos. Usar a execução simbólica pode encontrar o chamado problema de explosão de caminhos; onde há muitos caminhos para um computador explorar em um tempo razoável e um solucionador nunca seria capaz de terminar.
Na prática
Quão prático é seguir todos esses passos? Quão difícil é realmente fazer isso bem?
Essas técnicas exigem um esforço significativo para serem usadas. Você precisa entender como elas funcionam e precisa compreender suas limitações e como auxiliá-las. Também exigem um grande esforço para serem mantidas no final do dia. Eu acredito que o que realmente importa são as propriedades. Se você quer saber se um erro pode ocorrer e se a propriedade pode ser quebrada, você não precisa necessariamente de um método formal para isso e pode usar um fuzzer, que é muito mais fácil de usar e oferece basicamente o mesmo tipo de valor.
Josselin
A equipe da Trail of Bits criou o secure-contracts.com para ajudar os desenvolvedores a entender as propriedades, permitindo que eles construam e testem código com base em testes orientados a propriedades.
Em alguns casos, um fuzzer suficientemente potente é tudo de que você precisa, e a execução simbólica e a verificação formal são exageradas.
Além disso, mesmo a verificação formal não prova que seu código está livre de erros. Tudo o que faz é provar matematicamente que seu código faz aquela única coisa específica corretamente.
Espero que, com o avanço da inteligência artificial, muito disso se torne bem mais fácil. Mas acho que só o tempo dirá.
Conclusão
Por enquanto, espero que você tenha aprendido pelo menos o básico sobre execução simbólica. Se quiser aprender mais, deixe um comentário.
😸😸 Siga o Patrick 😸😸
Agende uma auditoria de contrato inteligente na Cyfrin!
Twitch Stream Uploads & Shorts
Artigo original publicado por Patrick Collins. Traduzido por Paulinho Giovannini.
Oldest comments (0)