Como usar o Echidna para testar contratos inteligentes

Instalação

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

Echidna com docker

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

O último comando roda a 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 através 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 a fuzzing baseado em propriedade

Echidna é um fuzzer baseado em propriedades, descrevemos em nossos posts anteriores (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. It consists of generating inputs that are more or less random to find bugs in the program. Fuzzers por 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 aleatória de entradas, há muitas técnicas e estratégias para gerar bons inputs, incluindo:

• Obtenha feedback de cada execução e geração de guias usando-o. Por exemplo, se uma entrada recém-gerada leva à descoberta de um novo caminho, ele pode fazer sentido para gerar novas entradas fechadas a ele.
• Geração da entrada respeitando uma restrição estrutural. Por exemplo, se a sua entrada contiver um cabeçalho com uma soma de verificação, fará sentido deixar o difusor gerar uma entrada validando a soma de verificação.
• Usando entradas conhecidas para gerar novas entradas: se você tem acesso a um grande conjunto de dados de entrada válida, seu difusor pode gerar novas entradas a partir deles, ao invés de começar sua geração do zero. Eles geralmente são chamados de seeds.

Fuzzing baseado em propriedade

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

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

• Controle de acesso incorreto: quem ataca tornou-se o proprietário do contrato.
• Máquina de estado incorreta: os tokens podem ser transferidos enquanto o contrato é pausado.
• Aritmética incorreta: o usuário pode passar abaixo do saldo e obter tokens gratuitos ilimitados.

Testando uma propriedade com Echidna

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

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Exibir tudo
 Copiar

Assumiremos que esse token deve ter as seguintes propriedades:

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

Escrever uma propriedade

Propriedades do Echidna são funções de Solidity. Uma propriedade deve:

• Ter nenhum argumento
• Retornar verdadeiro se for bem sucedido
• Tenha seu nome começando com echidna

Echidna irá:

• Gera automaticamente transações arbitrárias para testar a propriedade.
• Relata quaisquer transações que levem uma propriedade para retornar `` falso ou lançar um erro.
• Descartar efeito lateral ao chamar uma propriedade (ou seja, se a propriedade altera uma variável de estado, ela é descartada após o teste)

A propriedade a seguir verifica que o "caller" não possui mais do que 1000 tokens:

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

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

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

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

Iniciar um contrato

Echidna precisa de um constructor sem argumento. Se seu contrato precisa de uma inicialização específica, você precisa fazê-lo no construtor.

Há alguns endereços específicos no Echidna:

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

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

Executando Echidna

Echidna foi lançado com:

echidna-test contract.sol

Se o contract.sol contém múltiplos contratos, você pode especificar o alvo:

echidna-test contract.sol --contract MyContract

Resumo: Testando uma propriedade

O seguinte resumo é a execução de Echidna no nosso exemplo:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
 Copiar

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Exibir tudo

Echidna descobriu que a propriedade é violada se backdoor é chamada.

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

Veremos como filtrar as funções a serem "fuzzed". O alvo é o seguinte contrato inteligente:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Exibir tudo
 Copiar

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

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

Filtrando funções

Echidna tem problemas para encontrar a sequência correta para testar esse 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 Echidna para ou para a lista negra redefinir a função ou apenas para a lista branca f, g, h e i funções.

Para funções da lista negra, podemos usar esse arquivo de configuração:

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

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

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

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

Executar Echidna

Para executar 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()

Echidna vai encontrar a sequência de transações para falsificar a propriedade quase de forma mesquinha.

Resumo: Filtrando funções

Echidna pode ser chamada na lista negra ou na lista branca durante uma campanha de fuzzing:

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

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

Echidna inicia uma campanha de fuzzing em qualquer blacklist f1, f2 e f3 ou apenas chamando a eles, de acordo com o valor do booleano filterBlacklist.

Como testar a asserção de Solidity com Echidna

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

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Exibir tudo
 Copiar

Escreva uma asserção

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

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Exibir tudo
 Copiar

Executando Echidna

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

1checkAsserts: true

Quando executamos este contrato em 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
Exibir tudo

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

Quando e como usar asserções

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

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
7
 Copiar

Pelo contrário, usando uma propriedade Echidna explícita irá executar transações aleatoriamente e não há maneira fácil de aplicar exatamente quando elas serão verificadas. Ainda é possível fazer esta solução alternativa:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
 Copiar

Entretanto, existem alguns problemas: %{issues}:

• Ele falha se f é declarado como interno ou externo.
• Não está claro quais argumentos devem ser usados para chamar f.
• Se f reverter, a propriedade irá falhar.

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

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

Finalmente, não use require em vez de assert, já que Echidna não será capaz de detectá-lo (mas o contrato será revertido mesmo assim).

Resumo: checando a asserção

O seguinte resumo é a execução de Echidna no nosso exemplo:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Exibir tudo
 Copiar

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
Exibir tudo

Echidna percebeu que a asserção em inc pode falhar se essa função é chamada várias vezes com argumentos grandes.

Coletando e modificando um corpus Echidna

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

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Exibir tudo
 Copiar

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

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

No entanto, ainda podemos usar o Echidna para coletar corpus na condução desta campanha de fuzzing.

Coletando um corpus

Para habilitar a coleção de corpus, crie um diretório corpus:

mkdir corpus-magic

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

1coverage: true
2corpusDir: "corpus-magic"

Agora podemos rodar nossa ferramenta e checar o corpus coletado:

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

Echidna ainda não conseguiu encontrar os valores mágicos corretos, mas podemos olhar para o corpus que ele coletou. Por exemplo, um desses arquivos foi:

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Exibir tudo
 Copiar

Claramente, esse input não causará falha em nossa propriedade. No entanto, no próximo passo, veremos como modificá-lo nesse sentido.

Semeando um corpus

Echidna precisa de ajuda para lidar com a função mágica. Vamos copiar e modificar a entrada para usar os parâmetros adequados para ele:

cp corpus/2712688662897926208.txt corpus/new.txt

Nós iremos modificar new.txt para chamar mágica(42,129,333,0). Agora, podemos reexecutar o Echidna:

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
Exibir tudo

Desta vez, constatou que a propriedade é violada imediatamente.

Localizando transações com alto consumo de gas

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

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Exibir tudo
 Copiar

Aqui caro pode ter um grande consumo de gas.

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

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

Medição do consumo de gas

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

1estimateGas: true

Neste exemplo, também reduziremos o tamanho da sequência de transações para facilitar a compreensão dos resultados:

1seqLen: 2
2estimateGas: true

Executando Echidna

Assim que tivermos o arquivo de configuração criado, poderemos 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
Exibir tudo

• O gas mostrado é um cálculo fornecido por HEVM(opens in a new tab).

Filtrando Chamadas com Redução de Gas

O tutorial sobre funções de filtragem para chamar durante uma campanha de difusão acima mostra como remover algumas funções de seu teste.
Isso pode ser fundamental para obter uma estimativa de gas precisa. Considere o seguinte exemplo:

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
Exibir tudo
 Copiar

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

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Exibir tudo

Isso porque o custo depende do tamanho dos addrs e chamadas aleatórias tendem a deixar o array quase vazio. Lista negra pop e limpa, no entanto, nos dá resultados muito melhores:

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

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

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

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

1estimateGas: true

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

Echidna irá relatar uma sequência com o consumo máximo de gas para cada função, uma vez terminada a campanha de fuzzing.