Come usare Echidna per testare i contratti intelligenti
Installazione
Echidna può essere installato tramite docker o utilizzando il binario precompilato.
Echidna tramite docker
docker pull trailofbits/eth-security-toolboxdocker run -it -v "$PWD":/home/training trailofbits/eth-security-toolboxL'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-testBinario
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 tuttoFaremo 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
truese 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
falseo 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:
0x00a329c0648769A73afAc7F9381E08FB43dBEA72che chiama il costruttore.0x10000,0x20000e0x00a329C0648769a73afAC7F9381e08fb43DBEA70che 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.solSe contract.sol contiene più contratti, puoi specificare l'obiettivo:
echidna-test contract.sol --contract MyContractRiepilogo: Testare una proprietà
Quanto segue riassume l'esecuzione di echidna sul nostro esempio:
echidna-test token.sol1...2echidna_balance_under_1000: failed!💥3 Call sequence, shrinking (2596/5000):4 airdrop()5 backdoor()67...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;67 function f(uint x) public {8 require(x == 12);9 state1 = true;10 }1112 function g(uint x) public {13 require(state1);14 require(x == 8);15 state2 = true;16 }1718 function h(uint x) public {19 require(state2);20 require(x == 42);21 state3 = true;22 }2324 function i() public {25 require(state3);26 state4 = true;27 }2829 function reset1() public {30 state1 = false;31 state2 = false;32 state3 = false;33 return;34 }3536 function reset2() public {37 state1 = false;38 state2 = false;39 state3 = false;40 return;41 }4243 function echidna_state4() public returns (bool) {44 return (!state4);45 }46}Mostra tuttoQuesto 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: true2filterFunctions: ["reset1", "reset2"]Un altro approccio per filtrare le funzioni è elencare le funzioni nella whitelist. Per farlo, possiamo utilizzare questo file di configurazione:
1filterBlacklist: false2filterFunctions: ["f", "g", "h", "i"]filterBlacklistètrueper impostazione predefinita.- Il filtraggio verrà eseguito solo per nome (senza parametri). Se hai
f()ef(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: true2filterFunctions: ["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;34 function inc(uint val) public returns (uint){5 uint tmp = counter;6 counter += val;7 // tmp <= counter8 return (counter - tmp);9 }10}Mostra tuttoScrivere 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;34 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 tuttoEseguire Echidna
Per abilitare il test di fallimento dell'asserzione, crea un file di configurazione di Echidna (opens in a new tab) config.yaml:
1checkAsserts: trueQuando eseguiamo questo contratto in Echidna, otteniamo i risultati attesi:
echidna-test assert.sol --config config.yamlAnalyzing contract: /tmp/assert.sol:Incrementorassertion 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 code3 ...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 comeinternaloexternal. - Non è chiaro quali argomenti debbano essere utilizzati per chiamare
f. - Se
fesegue 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)dovevarè dichiarata comeuint.
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;34 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 tuttoechidna-test assert.sol --config config.yamlAnalyzing contract: /tmp/assert.sol:Incrementorassertion 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 }1112 function echidna_magic_values() public returns (bool) {13 return !value_found;14 }1516}Mostra tuttoQuesto 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-magicE un file di configurazione di Echidna (opens in a new tab) config.yaml:
1coverage: true2corpusDir: "corpus-magic"Ora possiamo eseguire il nostro strumento e controllare il corpus raccolto:
echidna-test magic.sol --config config.yamlEchidna 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 tuttoChiaramente, 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.txtModificheremo 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;34 function expensive(uint8 times) public {5 for(uint8 i=0; i < times; i++)6 state = state + i;7 }89 function echidna_test() public returns (bool) {10 return true;11 }1213}Mostra tuttoQui 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: trueIn questo esempio, ridurremo anche la dimensione della sequenza di transazioni per rendere i risultati più facili da comprendere:
1seqLen: 22estimateGas: trueEseguire 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.70sC.expensive(uint8) with gas 5463708: expensive(255) expensive(255)Mostra tutto- Il gas mostrato è una stima fornita da HEVM (opens in a new tab).
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;34 function push(address a) public {5 addrs.push(a);6 }78 function pop() public {9 addrs.pop();10 }1112 function clear() public{13 addrs.length = 0;14 }1516 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 }2223 function echidna_test() public returns (bool) {24 return true;25 }26}Mostra tuttoSe 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 tuttoQuesto 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: true2filterFunctions: ["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 tuttoRiepilogo: 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: trueechidna-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