Come usare Echidna per testare gli smart contract

Installazione

Echidna è installabile tramite docker o usando il binario pre-compilato.

Echidna tramite docker

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

L'ultimo comando esegue eth-security-toolbox in un docker che ha accesso alla tua cartella corrente. Puoi modificare i file dal tuo host ed eseguire gli strumenti sui file dal docker

Nel docker, esegui:

solc-select 0.5.11
cd /home/training

Binario

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

Introduzione al fuzzing basato sulla proprietà

Echidna è un fuzzer basato sulla proprietà, che abbiamo descritto nei nostri post del blog precedenti (1opens in a new tab, 2opens in a new tab, 3opens in a new tab).

Fuzzing

Il fuzzingopens in a new tab è una ben nota tecnica nella community della sicurezza. Consiste nella generazione di input più o meno randomici, per trovare i bug nel programma. I fuzzer per il software tradizionale (come AFLopens in a new tab o LibFuzzeropens in a new tab) sono noti per essere strumenti efficienti per trovare i bug.

Oltre alla generazione di input puramente casuale, esistono molte tecniche e strategie per generare input validi, tra cui:

• Ottenere feedback da ogni esecuzione e generazione della guida durante l'utilizzo. Ad esempio, se un input appena generato conduce alla scoperta di un nuovo percorso, può avere senso generare nuovi input vicini a esso.
• Generare l'input rispettando un vincolo strutturale. Ad esempio, se il tuo input contiene un'intestazione con un checksum, avrà senso lasciare che il fuzzer generi input a convalida del checksum.
• Usare input noti per generarne di nuovi: se hai accesso a un grande dataset di input validi, il tuo fuzzer può generarne di nuovi, anziché iniziare da zero la generazione. In genere sono detti seed.

Fuzzing basato sulla proprietà

Echidna appartiene a una famiglia specifica di fuzzer: il fuzzing basato sulla proprietà, ampiamente ispirato da QuickCheckopens in a new tab. In contrasto al fuzzer classico che prova a trovare i crash, Echidna prova a rompere le invarianti definite dall'utente.

Negli smart contract, le invarianti sono funzioni di Solidity, che possono rappresentare ogni stato non corretto o non valido raggiungibile dal contratto, tra cui:

• Controllo d'accesso errato: il malintenzionato diventa il proprietario del contratto.
• Macchina di stato errata: i token sono trasferibili mentre il contratto è in pausa.
• Aritmetica errata: l'utente può sottovalutare il proprio saldo e ottenere token gratuiti illimitati.

Testare una proprietà con Echidna

Vedremo come testare un contratto intelligente con Echidna. L'obiettivo è il seguente smart contract token.solopens 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}
Mostra tutto
Copia

Presumeremo che questo token debba avere le seguenti proprietà:

• Chiunque può avere al massimo 1.000 token
• Il token non è trasferibile (non è un token ERC20)

Scrivi una proprietà

Le proprietà di Echidna sono funzioni di Solidity. Una proprietà deve:

• Non avere alcun argomento
• Restituire true se va a buon fine
• Avere un nome che inizia per echidna

Echidna:

• Genererà automaticamente transazioni arbitrarie per testare la proprietà.
• Segnalare ogni transazione che fa sì che una proprietà restituisca false o generi un errore.
• Scartare l'effetto collaterale quando si chiama una proprietà (ad es. se la proprietà cambia una variabile di stato, viene scartata dopo il test)

La seguente proprietà controlla che il chiamante non abbia più di 1.000 token:

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

Usa l'eredità per separare il contratto dalle proprietà:

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

token.solopens in a new tab implementa la proprietà ed eredita dal token.

Avviare un contratto

Echidna necessita di un costruttore senza argomento. Se il tuo contratto necessita di un'inizializzazione specifica, devi farlo nel costruttore.

Esistono degli indirizzi specifici in Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 per chiamare il costruttore.
• 0x10000, 0x20000, e 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 per chiamare casualmente le altre funzioni.

Non necessitiamo di alcuna inizializzazione particolare nel nostro esempio corrente, di conseguenza il nostro costruttore è vuoto.

Eseguire Echidna

Echidna è avviato con:

echidna-test contract.sol

Se contract.sol contiene più contratti, puoi specificare l'obiettivo:

echidna-test contract.sol --contract MyContract

Riepilogo: Testare una proprietà

Di seguito è riepilogata l'esecuzione di Echidna nel nostro esempio:

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  }
Copia

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

Echidna ha individuato che la proprietà è violata se backdoor viene chiamata.

Filtrare le funzioni da chiamare durante una campagna di fuzzing

Vedremo come filtrare le funzioni da sottoporre a fuzzing. L'obiettivo è il seguente smart contract:

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}
Mostra tutto
Copia

Questo piccolo esempio forza Echidna a trovare una certa sequenza di transazioni per modificare una variabile di stato. Ciò è difficile per un fuzzer (si consiglia di usare uno strumento di esecuzione simbolica come Manticoreopens in a new tab). Possiamo eseguire Echidna per verificarlo:

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

Funzioni di filtraggio

Echidna fa fatica a trovare la sequenza corretta per testare questo contratto perché le due funzioni di reset (reset1 e reset2) imposteranno tutte le variabili di stato su false. Tuttavia, possiamo usare una funzionalità speciale di Echidna per inserire nella blacklist la funzione di reset o nella whitelist solo le funzioni f, g, h e i.

Per inserire le funzioni nella blacklist, possiamo usare questo file di configurazione:

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

Un altro approccio per filtrare le funzioni è elencare quelle nella whitelist. Per farlo, possiamo usare questo file di configurazione:

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

• filterBlacklist è true di default.
• Il filtraggio sarà eseguito solo per nome (senza parametri). Se hai f() e f(uint256), il filtro "f" abbinerà entrambe le funzioni.

Eseguire Echidna

Per eseguire Echidna con un file di configurazione blacklist.yaml:

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

Echidna troverà la sequenza di transazioni per falsificare la proprietà quasi immediatamente.

Riepilogo: Filtrare le funzioni

Echidna può inserire le funzioni di blacklist o whitelist da chiamare durante una campagna di fuzzing usando:

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

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

Echidna avvia una campagna di fuzzing inserendo f1, f2 e f3 nella blacklist o solo chiamandole, in base al valore del booleano filterBlacklist.

Come testare l'affermazione di Solidity con Echidna

In questo breve tutorial, mostreremo come usare Echidna per testare il controllo dell'affermazione nei contratti. Supponiamo di avere un contratto come questo:

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}
Mostra tutto
Copia

Scrivere un'asserzione

Vogliamo assicurarci che tmp sia minore o uguale al counter dopo averne restituita la differenza. Potremmo scrivere una proprietà di Echidna, ma dovremmo memorizzare da qualche parte il valore tmp. Invece, potremmo usare un'asserzione come questa:

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}
Mostra tutto
Copia

Eseguire Echidna

Per abilitare il test di insuccesso dell'asserzione, crea un file di configurazione di Echidnaopens in a new tab config.yaml:

1checkAsserts: true

Quando eseguiamo questo contratto in Echidna, otteniamo i risultati previsti:

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
Mostra tutto

Come puoi vedere, Echidna segnala alcuni insuccessi dell'asserzione nella funzione inc. Aggiungere più di un'asserzione per funzione è possibile, ma Echidna non può dire quale sia fallita.

Quando e come usare le asserzioni

Le asserzioni sono utilizzabili come alternative a proprietà esplicite, specialmente se le condizioni per il controllo sono direttamente correlate all'uso corretto della stessa operazione f. Aggiungere le asserzioni dopo il codice farà sì che il controllo abbia luogo immediatamente dopo la sua esecuzione:

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

Al contrario, l'utilizzo di una proprietà esplicita di Echidna eseguirà casualmente le transazioni e non esiste alcun metodo semplice per imporre esattamente quando verrà controllata. È comunque possibile sfruttare questa scappatoia:

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

Tuttavia, esistono dei problemi:

• Fallisce se f è dichiarata come internal o external.
• Non è chiaro quali argomenti dovrebbero essere usati per chiamare f.
• Se f si ripristina, la proprietà fallirà.

In generale, consigliamo di seguire i consigli di John Regehropens in a new tab su come usare le affermazioni:

• Non forzare alcun effetto collaterale durante il controllo dell'affermazione. Ad esempio: assert(ChangeStateAndReturn() == 1)
• Non affermare dichiarazioni ovvie. Ad esempio assert(var >= 0) dove var è dichiarata come uint.

Infine, consigliamo di non usare require al posto di assert, poiché Echidna non potrà rilevarlo (ma il contratto si ripristinerà ugualmente).

Riepilogo: Controllo dell'asserzione

Quanto segue riepiloga l'esecuzione di Echidna nel nostro esempio:

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}
Mostra tutto
Copia

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
Mostra tutto

Echidna ha trovato che l'asserzione in inc può fallire se questa funzione è chiamata diverse volte con grandi argomenti.

Raccogliere e modificare un corpus di Echidna

Vedremo come raccogliere e usare un corpus di transazioni con Echidna. L'obiettivo è il seguente smart contract magic.solopens 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}
Mostra tutto
Copia

Questo piccolo esempio forza Echidna a trovare una certi valori per modificare una variabile di stato, il che è difficile per un fuzzer (si consiglia di usare uno strumento d'esecuzione simbolica come Manticoreopens in a new tab). Possiamo eseguire Echidna per verificarlo:

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

Tuttavia, possiamo comunque usare Echidna per raccogliere il corpus mentre si esegue questa campagna di fuzzing.

Raccogliere un corpus

Per abilitare la raccolta, crea la cartella di un corpus:

mkdir corpus-magic

E un file di configurazione di Echidnaopens in a new tab config.yaml:

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

Ora possiamo eseguire il nostro strumento e controllare il corpus raccolto:

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

Echidna non è ancora in grado di trovare i valori magici corretti, ma possiamo dare un'occhiata al corpus raccolto. Ad esempio, uno di questi file era:

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]
Mostra tutto
Copia

Chiaramente, questo input non innescherà il fallimento nella nostra proprietà. Tuttavia, nel prossimo passaggio, vedremo come modificarlo a tale scopo.

Seeding di un corpus

Echidna necessita di un po' di aiuto per poter affrontare la funzione magic. Copieremo e modificheremo l'input per usare parametri idonei a tale scopo:

cp corpus/2712688662897926208.txt corpus/new.txt

Modificheremo new.txt per chiamare magic(42,129,333,0). Ora possiamo ri-eseguire 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
Mostra tutto

Questa volta, ha scoperto che la proprietà è immediatamente violata.

Individuare le transazioni ad alto consumo di gas

Vedremo come individuare le transazioni con un alto consumo di gas con Echidna. L'obiettivo è il seguente smart contract:

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}
Mostra tutto
Copia

Qui expensive può avere un gran consumo di gas.

Attualmente, Echidna necessità sempre di una proprietà da testare: qui echidna_test restituisce sempre true. Possiamo eseguire Echidna per verificarlo:

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

Misurare il Consumo di Gas

Per abilitare il consumo di gas con Echidna, crea un file di configurazione config.yaml:

1estimateGas: true

In questo esempio, ridurremo anche le dimensioni della sequenza di transazione per facilitare la comprensione dei risultati:

1seqLen: 2
2estimateGas: true

Eseguire Echidna

Una volta creato il file di configurazione, possiamo eseguire Echidna come segue:

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
Mostra tutto

• Il gas mostrato è una stima fornita da HEVMopens in a new tab.

Filtrare le Chiamate di Riduzione del Gas

Il tutorial precedente sulle funzioni di filtraggio da chiamare durante una campagna di fuzzing, mostra come rimuovere alcune funzioni dal tuo test.
Questo può esser critico per ottenere una stima accurata del gas. Considera l'esempio seguente:

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}
Mostra tutto
Copia

Se Echidna può chiamare tutte le funzioni, non troverà facilmente le transazioni a costo elevato di 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
Mostra tutto

Questo perché il costo dipende dalla dimensione di addrs e le chiamate casuali tendono a lasciare l'array quasi vuoto. L'inserimento in blacklist di pop e clear, tuttavia, fornisce risultati molto più efficaci:

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

Sommario: Individuare le transazioni ad alto consumo di gas

Echidna può trovare le transazioni ad alto consumo di gas usando l'opzione di configurazione estimateGas:

1estimateGas: true

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

Echidna segnalerà una sequenza con il consumo massimo di gas per ogni funzione, una volta terminata la campagna di fuzzing.

Page last update: 4 dicembre 2023

popens in a new tab

nopens in a new tab

Mopens in a new tab

+7

Visualizza chi ha contribuito