Vai al contenuto principale

Come usare Echidna per testare i contratti intelligenti

Solidity
contratti intelligenti
sicurezza
testing
fuzzing
Avanzato
Trailofbits
10 aprile 2020
13 minuti di lettura

Installazione

Echidna può essere installato tramite docker o utilizzando il binario precompilato.

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 directory corrente. Puoi modificare i file dal tuo host ed eseguire gli strumenti sui file dal docker

All'interno di docker, esegui:

echidna-test

Binario

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

Introduzione al fuzzing basato sulle proprietà

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

Fuzzing

Il Fuzzing (opens in a new tab) è una tecnica ben nota nella community della sicurezza. Consiste nel generare input più o meno casuali per trovare bug nel programma. I fuzzer per i software tradizionali (come AFL (opens in a new tab) o LibFuzzer (opens in a new tab)) sono noti per essere strumenti efficienti per trovare bug.

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

  • Ottenere feedback da ogni esecuzione e guidare la generazione utilizzandolo. Ad esempio, se un input appena generato porta alla scoperta di un nuovo percorso, può avere senso generare nuovi input vicini ad 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 che convalidano il checksum.
  • Utilizzare input noti per generare nuovi input: se hai accesso a un ampio set di dati di input validi, il tuo fuzzer può generare nuovi input da essi, piuttosto che iniziare la sua generazione da zero. Questi sono solitamente chiamati seed (semi).

Fuzzing basato sulle proprietà

Echidna appartiene a una famiglia specifica di fuzzer: il fuzzing basato sulle proprietà, fortemente ispirato a QuickCheck (opens in a new tab). A differenza dei fuzzer classici che cercheranno di trovare crash, Echidna cercherà di infrangere gli invarianti definiti dall'utente.

Nei contratti intelligenti, gli invarianti sono funzioni Solidity, che possono rappresentare qualsiasi stato errato o non valido che il contratto può raggiungere, tra cui:

  • Controllo degli accessi errato: l'attaccante è diventato il proprietario del contratto.
  • Macchina a stati errata: i token possono essere trasferiti mentre il contratto è in pausa.
  • Aritmetica errata: l'utente può mandare in underflow 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 contratto intelligente token.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}
Mostra tutto

Faremo l'ipotesi che questo token debba avere le seguenti proprietà:

  • Chiunque può avere al massimo 1000 token
  • Il token non può essere trasferito (non è un token ERC20)

Scrivere una proprietà

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

  • Non avere argomenti
  • Restituire true se ha successo
  • Avere il suo nome che inizia con echidna

Echidna farà quanto segue:

  • Genererà automaticamente transazioni arbitrarie per testare la proprietà.
  • Segnalerà qualsiasi transazione che porta una proprietà a restituire false o a generare un errore.
  • Scarterà gli effetti collaterali quando si chiama una proprietà (ad es., se la proprietà modifica una variabile di stato, viene scartata dopo il test)

La seguente proprietà verifica che il chiamante non abbia più di 1000 token:

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

Usa l'ereditarietà per separare il tuo contratto dalle tue proprietà:

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

token.sol (opens in a new tab) implementa la proprietà ed eredita dal token.

Inizializzare un contratto

Echidna ha bisogno di un costruttore senza argomenti. Se il tuo contratto necessita di un'inizializzazione specifica, devi farla nel costruttore.

Ci sono alcuni indirizzi specifici in Echidna:

  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 che chiama il costruttore.
  • 0x10000, 0x20000 e 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 che chiamano casualmente le altre funzioni.

Non abbiamo bisogno di alcuna inizializzazione particolare nel nostro esempio attuale, di conseguenza il nostro costruttore è vuoto.

Eseguire Echidna

Echidna viene 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à

Quanto segue riassume l'esecuzione di echidna sul nostro esempio:

echidna-test token.sol
1...
2echidna_balance_under_1000: failed!💥
3 Call sequence, shrinking (2596/5000):
4 airdrop()
5 backdoor()
6
7...

Echidna ha scoperto che la proprietà viene violata se viene chiamato backdoor.

Filtrare le funzioni da chiamare durante una campagna di fuzzing

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

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

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

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

Filtrare le funzioni

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

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

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

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

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]
  • filterBlacklist è true per impostazione predefinita.
  • Il filtraggio verrà eseguito solo per nome (senza parametri). Se hai f() e f(uint256), il filtro "f" corrisponderà a 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 nella blacklist o nella whitelist le funzioni da chiamare durante una campagna di fuzzing utilizzando:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]
echidna-test contract.sol --config config.yaml
...

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

Come testare l'assert di Solidity con Echidna

In questo breve tutorial, mostreremo come utilizzare Echidna per testare il controllo delle asserzioni 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

Scrivere un'asserzione

Vogliamo assicurarci che tmp sia minore o uguale a counter dopo aver restituito la sua differenza. Potremmo scrivere una proprietà Echidna, ma avremmo bisogno di memorizzare il valore tmp da qualche parte. 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

Eseguire Echidna

Per abilitare il test di fallimento dell'asserzione, crea un file di configurazione di Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

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

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

Come puoi vedere, Echidna segnala alcuni fallimenti di asserzione nella funzione inc. È possibile aggiungere più di un'asserzione per funzione, ma Echidna non può dire quale asserzione è fallita.

Quando e come usare le asserzioni

Le asserzioni possono essere utilizzate come alternative alle proprietà esplicite, specialmente se le condizioni da verificare sono direttamente correlate all'uso corretto di qualche operazione f. L'aggiunta di asserzioni dopo del codice imporrà che il controllo avvenga immediatamente dopo la sua esecuzione:

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

Al contrario, l'utilizzo di una proprietà echidna esplicita eseguirà casualmente le transazioni e non c'è un modo semplice per imporre esattamente quando verrà verificata. È comunque possibile utilizzare questa soluzione alternativa:

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

Tuttavia, ci sono alcuni problemi:

  • Fallisce se f è dichiarata come internal o external.
  • Non è chiaro quali argomenti debbano essere utilizzati per chiamare f.
  • Se f esegue un revert, la proprietà fallirà.

In generale, consigliamo di seguire la raccomandazione di John Regehr (opens in a new tab) su come utilizzare le asserzioni:

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

Infine, per favore non usare require invece di assert, poiché Echidna non sarà in grado di rilevarlo (ma il contratto verrà comunque annullato).

Riepilogo: Controllo delle asserzioni

Quanto segue riassume l'esecuzione di echidna sul 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
echidna-test assert.sol --config config.yaml
Analyzing contract: /tmp/assert.sol:Incrementor
assertion in inc: failed!💥
Call sequence, shrinking (2596/5000):
inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)

Echidna ha scoperto che l'asserzione in inc può fallire se questa funzione viene chiamata più volte con argomenti di grandi dimensioni.

Raccogliere e modificare un corpus di Echidna

Vedremo come raccogliere e utilizzare un corpus di transazioni con Echidna. L'obiettivo è il seguente contratto intelligente magic.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 == 333);
7 require(magic_4 == 0);
8 value_found = true;
9 return;
10 }
11
12 function echidna_magic_values() public returns (bool) {
13 return !value_found;
14 }
15
16}
Mostra tutto

Questo piccolo esempio forza Echidna a trovare determinati valori per modificare una variabile di stato. Questo è difficile per un fuzzer (si consiglia di utilizzare uno strumento di esecuzione simbolica come Manticore (opens in a new tab)). Possiamo eseguire Echidna per verificarlo:

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

Tuttavia, possiamo ancora utilizzare Echidna per raccogliere il corpus durante l'esecuzione di questa campagna di fuzzing.

Raccogliere un corpus

Per abilitare la raccolta del corpus, crea una directory per il corpus:

mkdir corpus-magic

E un file di configurazione di Echidna (opens 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 riesce ancora a trovare i valori magici corretti, ma possiamo dare un'occhiata al corpus che ha raccolto. Ad esempio, uno di questi file era:

1[
2 {
3 "_m": "magic(uint256,uint256,uint256,uint256)",
4 "_args": [
5 "0x4fa567653f26f941",
6 "0x227c946b75c6b9",
7 "0x1176a2410b466f71",
8 "0xbf6b4ea0ceebdce8"
9 ],
10 "_gas": "0x50911",
11 "_value": "0x0",
12 "_delay": ["0x1364", "0xccfa"]
13 }
14]
Mostra tutto

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

Seminare un corpus

Echidna ha bisogno di un po' di aiuto per gestire la funzione magic. Copieremo e modificheremo l'input per utilizzare parametri adatti ad essa:

cp corpus/covered.1560453495.html new.txt

Modificheremo new.txt per chiamare magic(42,129,333,0). Ora possiamo eseguire nuovamente Echidna:

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

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

Trovare transazioni con un elevato consumo di gas

Vedremo come trovare le transazioni con un elevato consumo di gas con Echidna. L'obiettivo è il seguente contratto intelligente:

1contract C {
2 uint state;
3
4 function expensive(uint8 times) public {
5 for(uint8 i=0; i < times; i++)
6 state = state + i;
7 }
8
9 function echidna_test() public returns (bool) {
10 return true;
11 }
12
13}
Mostra tutto

Qui expensive può avere un grande consumo di gas.

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

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

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 la dimensione della sequenza di transazioni per rendere i risultati più facili da comprendere:

1seqLen: 2
2estimateGas: true

Eseguire Echidna

Una volta creato il file di configurazione, possiamo eseguire Echidna in questo modo:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
fuzzing time: 2.70s
C.expensive(uint8) with gas 5463708:
expensive(255)
expensive(255)
Mostra tutto

Filtrare le chiamate che riducono il gas

Il tutorial su filtrare le funzioni da chiamare durante una campagna di fuzzing qui sopra mostra come rimuovere alcune funzioni dai tuoi test.
Questo può essere fondamentale per ottenere una stima accurata del gas. Considera il seguente esempio:

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

Se Echidna può chiamare tutte le funzioni, non troverà facilmente transazioni con un costo del gas elevato:

echidna-test gas.sol --config config.yaml
...
C.check() with gas 733189:
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
check()
Mostra tutto

Questo perché il costo dipende dalla dimensione di addrs e le chiamate casuali tendono a lasciare l'array quasi vuoto. Inserire nella blacklist pop e clear, tuttavia, ci dà risultati molto migliori:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]
echidna-test gas.sol --config config.yaml
...
C.check() with gas 5082692:
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
push(0x0000000000000000000000000000000000000000)
check()
Mostra tutto

Riepilogo: Trovare transazioni con un elevato consumo di gas

Echidna può trovare transazioni con un elevato consumo di gas utilizzando l'opzione di configurazione estimateGas:

1estimateGas: true
echidna-test contract.sol --config config.yaml
...

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

Ultimo aggiornamento della pagina: 21 ottobre 2025

Questo tutorial è stato utile?