Como usar o Echidna para testar contratos inteligentes

Instalação

O Echidna pode ser instalado através do Docker ou usando o binário pré-compilado.

Echidna através do Docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

O último comando executa o eth-security-toolbox em um Docker que tem acesso ao seu diretório atual. Você pode alterar os arquivos do seu host e executar as ferramentas nos arquivos a partir do Docker

Dentro do Docker, execute:

solc-select 0.5.11
cd /home/training

Binário

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

Introdução ao fuzzing baseado em propriedades

O Echidna é um fuzzer baseado em propriedades, que descrevemos em nossas postagens anteriores do blog (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Fuzzing

Fuzzing (opens in a new tab) é uma técnica bem conhecida na comunidade de segurança. Consiste em gerar entradas que são mais ou menos aleatórias para encontrar bugs no programa. Fuzzers para software tradicional (como AFL (opens in a new tab) ou LibFuzzer (opens in a new tab)) são conhecidos por serem ferramentas eficientes para encontrar bugs.

Além da geração puramente aleatória de entradas, existem muitas técnicas e estratégias para gerar boas entradas, incluindo:

• Obter feedback de cada execução e guiar a geração usando-o. Por exemplo, se uma entrada recém-gerada leva à descoberta de um novo caminho, pode fazer sentido gerar novas entradas próximas a ela.
• Gerar a entrada respeitando uma restrição estrutural. Por exemplo, se sua entrada contém um cabeçalho com um checksum, fará sentido deixar o fuzzer gerar entradas que validem o checksum.
• Usar entradas conhecidas para gerar novas entradas: se você tem acesso a um grande conjunto de dados de entradas válidas, seu fuzzer pode gerar novas entradas a partir delas, em vez de começar sua geração do zero. Estas são geralmente chamadas de sementes (seeds).

Fuzzing baseado em propriedades

O Echidna pertence a uma família específica de fuzzer: fuzzing baseado em propriedades fortemente inspirado no QuickCheck (opens in a new tab). Em contraste com o fuzzer clássico que tentará encontrar falhas (crashes), o Echidna tentará quebrar invariantes definidos pelo usuário.

Em contratos inteligentes, invariantes são funções em Solidity que podem representar qualquer estado incorreto ou inválido que o contrato possa alcançar, incluindo:

• Controle de acesso incorreto: o invasor se tornou o proprietário do contrato.
• Máquina de estado incorreta: os tokens podem ser transferidos enquanto o contrato está pausado.
• Aritmética incorreta: o usuário pode causar um underflow em seu saldo e obter tokens gratuitos ilimitados.

Testando uma propriedade com o Echidna

Veremos como testar um contrato inteligente com o Echidna. O alvo é o seguinte contrato inteligente token.sol (opens in a new tab):

contract Token{
  mapping(address => uint) public balances;
  function airdrop() public{
      balances[msg.sender] = 1000;
  }
  function consume() public{
      require(balances[msg.sender]>0);
      balances[msg.sender] -= 1;
  }
  function backdoor() public{
      balances[msg.sender] += 1;
  }
}

Faremos a suposição de que este token deve ter as seguintes propriedades:

• Qualquer pessoa pode ter no máximo 1000 tokens
• O token não pode ser transferido (não é um token ERC-20)

Escrever uma propriedade

As propriedades do Echidna são funções em Solidity. Uma propriedade deve:

• Não ter argumentos
• Retornar true se for bem-sucedida
• Ter seu nome começando com echidna

O Echidna irá:

• Gerar automaticamente transações arbitrárias para testar a propriedade.
• Relatar quaisquer transações que levem uma propriedade a retornar false ou lançar um erro.
• Descartar efeitos colaterais ao chamar uma propriedade (ou seja, se a propriedade alterar uma variável de estado, ela será descartada após o teste)

A propriedade a seguir verifica se o chamador não tem mais de 1000 tokens:

function echidna_balance_under_1000() public view returns(bool){
      return balances[msg.sender] <= 1000;
}

Use herança para separar seu contrato de suas propriedades:

contract TestToken is Token{
      function echidna_balance_under_1000() public view returns(bool){
            return balances[msg.sender] <= 1000;
      }
  }

token.sol (opens in a new tab) implementa a propriedade e herda do token.

Iniciar um contrato

O Echidna precisa de um construtor sem argumentos. Se o seu contrato precisar de uma inicialização específica, você precisará fazê-la no construtor.

Existem alguns endereços específicos no Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 que chama o construtor.
• 0x10000, 0x20000 e 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 que chamam aleatoriamente as outras funções.

Não precisamos de nenhuma inicialização específica em nosso exemplo atual, como resultado, nosso construtor está vazio.

Executar o Echidna

O Echidna é iniciado com:

echidna-test contract.sol

Se contract.sol contiver vários contratos, você pode especificar o alvo:

echidna-test contract.sol --contract MyContract

Resumo: Testando uma propriedade

O seguinte resume a execução do Echidna em nosso exemplo:

contract TestToken is Token{
    constructor() public {}
        function echidna_balance_under_1000() public view returns(bool){
          return balances[msg.sender] <= 1000;
        }
  }

echidna-test testtoken.sol --contract TestToken
...

echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()

...

O Echidna descobriu que a propriedade é violada se backdoor for chamado.

Filtrando funções para chamar durante uma campanha de fuzzing

Veremos como filtrar as funções a serem submetidas ao fuzzing. O alvo é o seguinte contrato inteligente:

contract C {
  bool state1 = false;
  bool state2 = false;
  bool state3 = false;
  bool state4 = false;

  function f(uint x) public {
    require(x == 12);
    state1 = true;
  }

  function g(uint x) public {
    require(state1);
    require(x == 8);
    state2 = true;
  }

  function h(uint x) public {
    require(state2);
    require(x == 42);
    state3 = true;
  }

 function i() public {
    require(state3);
    state4 = true;
  }

  function reset1() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function reset2() public {
    state1 = false;
    state2 = false;
    state3 = false;
    return;
  }

  function echidna_state4() public returns (bool) {
    return (!state4);
  }
}

Este pequeno exemplo força o Echidna a encontrar uma certa sequência de transações para alterar uma variável de estado. Isso é difícil para um fuzzer (recomenda-se usar uma ferramenta de execução simbólica como o Manticore (opens in a new tab)). Podemos executar o Echidna para verificar isso:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

Filtrando funções

O Echidna tem problemas para encontrar a sequência correta para testar este contrato porque as duas funções de redefinição (reset1 e reset2) definirão todas as variáveis de estado como false. No entanto, podemos usar um recurso especial do Echidna para colocar a função de redefinição em uma lista de bloqueio ou colocar em uma lista de permissões apenas as funções f, g, h e i.

Para colocar funções na lista de bloqueio, podemos usar este arquivo de configuração:

filterBlacklist: true
filterFunctions: ["reset1", "reset2"]

Outra abordagem para filtrar funções é listar as funções permitidas. Para fazer isso, podemos usar este arquivo de configuração:

filterBlacklist: false
filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist é true por padrão.
• A filtragem será realizada apenas pelo nome (sem parâmetros). Se você tiver f() e f(uint256), o filtro "f" corresponderá a ambas as funções.

Executar o Echidna

Para executar o Echidna com um arquivo de configuração blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

O Echidna encontrará a sequência de transações para falsificar a propriedade quase imediatamente.

Resumo: Filtrando funções

O Echidna pode colocar funções em uma lista de bloqueio ou de permissões para chamar durante uma campanha de fuzzing usando:

filterBlacklist: true
filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

O Echidna inicia uma campanha de fuzzing bloqueando f1, f2 e f3 ou apenas chamando-as, de acordo com o valor do booleano filterBlacklist.

Como testar a asserção do Solidity com o Echidna

Neste breve tutorial, mostraremos como usar o Echidna para testar a verificação de asserção em contratos. Vamos supor que temos um contrato como este:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    // tmp <= counter
    return (counter - tmp);
  }
}

Escrever uma asserção

Queremos ter certeza de que tmp é menor ou igual a counter após retornar sua diferença. Poderíamos escrever uma propriedade do Echidna, mas precisaremos armazenar o valor de tmp em algum lugar. Em vez disso, poderíamos usar uma asserção como esta:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

Executar o Echidna

Para habilitar o teste de falha de asserção, crie um arquivo de configuração do Echidna (opens in a new tab) config.yaml:

checkAsserts: true

Quando executamos este contrato no Echidna, obtemos os resultados esperados:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)

Seed: 1806480648350826486

Como você pode ver, o Echidna relata alguma falha de asserção na função inc. Adicionar mais de uma asserção por função é possível, mas o Echidna não pode dizer qual asserção falhou.

Quando e como usar asserções

As asserções podem ser usadas como alternativas a propriedades explícitas, especialmente se as condições a serem verificadas estiverem diretamente relacionadas ao uso correto de alguma operação f. Adicionar asserções após algum código forçará que a verificação aconteça imediatamente após sua execução:

function f(..) public {
    // algum código complexo
    ...
    assert (condition);
    ...
}

Pelo contrário, usar uma propriedade explícita do Echidna executará transações aleatoriamente e não há uma maneira fácil de forçar exatamente quando ela será verificada. Ainda é possível fazer esta solução alternativa:

function echidna_assert_after_f() public returns (bool) {
    f(..);
    return(condition);
}

No entanto, existem alguns problemas:

• Falha se f for declarado como internal ou external.
• Não está claro quais argumentos devem ser usados para chamar f.
• Se f reverter, a propriedade falhará.

Em geral, recomendamos seguir a recomendação de John Regehr (opens in a new tab) sobre como usar asserções:

• Não force nenhum efeito colateral durante a verificação da asserção. Por exemplo: assert(ChangeStateAndReturn() == 1)
• Não faça asserções de declarações óbvias. Por exemplo assert(var >= 0) onde var é declarado como uint.

Finalmente, por favor não use require em vez de assert, pois o Echidna não será capaz de detectá-lo (mas o contrato será revertido de qualquer maneira).

Resumo: Verificação de asserção

O seguinte resume a execução do Echidna em nosso exemplo:

contract Incrementor {
  uint private counter = 2**200;

  function inc(uint val) public returns (uint){
    uint tmp = counter;
    counter += val;
    assert (tmp <= counter);
    return (counter - tmp);
  }
}

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)

Seed: 1806480648350826486

O Echidna descobriu que a asserção em inc pode falhar se esta função for chamada várias vezes com argumentos grandes.

Coletando e modificando um corpus do Echidna

Veremos como coletar e usar um corpus de transações com o Echidna. O alvo é o seguinte contrato inteligente magic.sol (opens in a new tab):

contract C {
  bool value_found = false;
  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
    require(magic_1 == 42);
    require(magic_2 == 129);
    require(magic_3 == magic_4+333);
    value_found = true;
    return;
  }

  function echidna_magic_values() public returns (bool) {
    return !value_found;
  }

}

Este pequeno exemplo força o Echidna a encontrar certos valores para alterar uma variável de estado. Isso é difícil para um fuzzer (recomenda-se usar uma ferramenta de execução simbólica como o Manticore (opens in a new tab)). Podemos executar o Echidna para verificar isso:

echidna-test magic.sol
...

echidna_magic_values: passed! 🎉

Seed: 2221503356319272685

No entanto, ainda podemos usar o Echidna para coletar corpus ao executar esta campanha de fuzzing.

Coletando um corpus

Para habilitar a coleta de corpus, crie um diretório de corpus:

mkdir corpus-magic

E um arquivo de configuração do Echidna (opens in a new tab) config.yaml:

coverage: true
corpusDir: "corpus-magic"

Agora podemos executar nossa ferramenta e verificar o corpus coletado:

echidna-test magic.sol --config config.yaml

O Echidna ainda não consegue encontrar os valores mágicos corretos, mas podemos dar uma olhada no corpus que ele coletou. Por exemplo, um desses arquivos era:

[
  {
    "_gas'": "0xffffffff",
    "_delay": ["0x13647", "0xccf6"],
    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
    "_value": "0x0",
    "_call": {
      "tag": "SolCall",
      "contents": [
        "magic",
        [
          {
            "contents": [
              256,
              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
            ],
            "tag": "AbiUInt"
          },
          {
            "contents": [256, "334"],
            "tag": "AbiUInt"
          },
          {
            "contents": [
              256,
              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
            ],
            "tag": "AbiUInt"
          },
          {
            "tag": "AbiUInt",
            "contents": [256, "332"]
          }
        ]
      ]
    },
    "_gasprice'": "0xa904461f1"
  }
]

Claramente, esta entrada não acionará a falha em nossa propriedade. No entanto, na próxima etapa, veremos como modificá-la para isso.

Semeando um corpus

O Echidna precisa de alguma ajuda para lidar com a função magic. Vamos copiar e modificar a entrada para usar parâmetros adequados para ela:

cp corpus/2712688662897926208.txt corpus/new.txt

Modificaremos new.txt para chamar magic(42,129,333,0). Agora, podemos executar o Echidna novamente:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)


Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537

Desta vez, ele descobriu que a propriedade é violada imediatamente.

Encontrando transações com alto consumo de gás

Veremos como encontrar as transações com alto consumo de gás com o Echidna. O alvo é o seguinte contrato inteligente:

contract C {
  uint state;

  function expensive(uint8 times) internal {
    for(uint8 i=0; i < times; i++)
      state = state + i;
  }

  function f(uint x, uint y, uint8 times) public {
    if (x == 42 && y == 123)
      expensive(times);
    else
      state = 0;
  }

  function echidna_test() public returns (bool) {
    return true;
  }

}

Aqui expensive pode ter um grande consumo de gás.

Atualmente, o Echidna sempre precisa de uma propriedade para testar: aqui echidna_test sempre retorna true. Podemos executar o Echidna para verificar isso:

echidna-test gas.sol
...
echidna_test: passou! 🎉

Semente: 2320549945714142710

Medindo o consumo de gás

Para habilitar o consumo de gás com o Echidna, crie um arquivo de configuração config.yaml:

estimateGas: true

Neste exemplo, também reduziremos o tamanho da sequência de transações para tornar os resultados mais fáceis de entender:

seqLen: 2
estimateGas: true

Executar o Echidna

Depois de criar o arquivo de configuração, podemos executar o Echidna assim:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉

f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2

Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325

• O gás mostrado é uma estimativa fornecida pela HEVM (opens in a new tab).

Filtrando chamadas que reduzem o gás

O tutorial sobre filtrando funções para chamar durante uma campanha de fuzzing acima mostra como remover algumas funções de seus testes. Isso pode ser crítico para obter uma estimativa precisa de gás. Considere o seguinte exemplo:

contract C {
  address [] addrs;
  function push(address a) public {
    addrs.push(a);
  }
  function pop() public {
    addrs.pop();
  }
  function clear() public{
    addrs.length = 0;
  }
  function check() public{
    for(uint256 i = 0; i < addrs.length; i++)
      for(uint256 j = i+1; j < addrs.length; j++)
        if (addrs[i] == addrs[j])
          addrs[j] = address(0x0);
  }
  function echidna_test() public returns (bool) {
      return true;
  }
}

Se o Echidna puder chamar todas as funções, ele não encontrará facilmente transações com alto custo de gás:

echidna-test pushpop.sol --config config.yaml
...
pop usou um máximo de 10746 de gás
...
check usou um máximo de 23730 de gás
...
clear usou um máximo de 35916 de gás
...
push usou um máximo de 40839 de gás

Isso ocorre porque o custo depende do tamanho de addrs e chamadas aleatórias tendem a deixar o array quase vazio. Colocar pop e clear na lista de bloqueio, no entanto, nos dá resultados muito melhores:

filterBlacklist: true
filterFunctions: ["pop", "clear"]

echidna-test pushpop.sol --config config.yaml
...
push usou um máximo de 40839 de gás
...
check usou um máximo de 1484472 de gás

Resumo: Encontrando transações com alto consumo de gás

O Echidna pode encontrar transações com alto consumo de gás usando a opção de configuração estimateGas:

estimateGas: true

echidna-test contract.sol --config config.yaml
...

O Echidna relatará uma sequência com o consumo máximo de gás para cada função, assim que a campanha de fuzzing terminar.

Última atualização da página: 3 de março de 2026

p (opens in a new tab)

n (opens in a new tab)

M (opens in a new tab)

+9

Ver contribuidores