crytic/echidnaFuzzer per smart contract Ethereum
Echidna è una strana creatura che mangia bug ed è altamente elettrosensibile (con le scuse a Jacob Stanley)
Più seriamente, Echidna è un programma Haskell progettato per il fuzzing/testing basato su proprietà di smart contract Ethereum. Utilizza sofisticate campagne di fuzzing basate su grammatica su un contract ABI per falsificare predicati definiti dall'utente o asserzioni Solidity. Abbiamo progettato Echidna con la modularità in mente, così può essere facilmente esteso per includere nuove mutazioni o testare contratti specifici in casi specifici.
.. e un bellissimo logo artigianale ad alta risoluzione.
La funzionalità principale di Echidna è un eseguibile chiamato echidna, che prende un contratto e una lista
di invarianti (proprietà che dovrebbero rimanere sempre vere) come input. Per ogni invariante, genera
sequenze casuali di chiamate al contratto e verifica se l'invariante è valida. Se riesce a trovare un modo
per falsificare l'invariante, stampa la sequenza di chiamate che lo fa. Se non ci riesce, hai una certa
garanzia che il contratto sia sicuro.
Le invarianti sono espresse come funzioni Solidity con nomi che iniziano con echidna_, non hanno argomenti e restituiscono un booleano. Ad esempio, se hai una variabile balance che non dovrebbe mai scendere sotto 20, puoi scrivere una funzione extra nel tuo contratto come questa:```solidity
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
Per verificare queste invarianti, eseguire:```sh
$ echidna myContract.sol
Un esempio di contratto con test può essere trovato in tests/solidity/basic/flags.sol. Per eseguirlo, dovresti eseguire:```sh $ echidna tests/solidity/basic/flags.sol
Echidna dovrebbe trovare una sequenza di chiamate che falsifica `echidna_sometimesfalse` e non dovrebbe essere in grado di trovare un input falsificante per `echidna_alwaystrue`.
### Modalità di test
L'esempio sopra utilizza la modalità predefinita **property**, ma Echidna supporta diverse modalità di test, configurate tramite `testMode` nel file di configurazione o `--test-mode` sulla CLI:
* **`property`** (predefinita): Testa le funzioni con prefisso `echidna_` che restituiscono `bool`.
* **`assertion`**: Rileva i fallimenti delle asserzioni da `assert()` e dagli helper `assertX` di Foundry (`assertTrue`, `assertEq`, ecc.).
* **`foundry`**: Esegue test in stile Foundry, seguendo le sue convenzioni di denominazione: test unitari e fuzz con prefisso `test` (quelli con prefisso `testFail` devono revertire) e invarianti stateful con prefisso `invariant` o `statefulFuzz`. Le funzioni con prefisso `check` e `prove` sono punti di ingresso simbolici, ma poiché questa modalità è una campagna di fuzzing, vengono sottoposte a fuzzing come qualsiasi altra funzione di test.
* **`verification`**: Verifica simbolicamente ogni funzione del contratto utilizzando una singola transazione. Le funzioni con prefisso `check` e `prove` vengono sempre utilizzate come punti di ingresso.
* **`overflow`**: Rileva overflow/underflow di interi (Solidity >= 0.8.0).
* **`optimization`**: Massimizza il valore di ritorno delle funzioni con prefisso `echidna_` che restituiscono `int256` (utilizza lo stesso prefisso configurabile della modalità property).
* **`exploration`**: Raccoglie la copertura senza verificare le proprietà.
### Raccolta e visualizzazione della copertura
Al termine di una campagna, Echidna può salvare un **corpus** che massimizza la copertura in una directory speciale specificata con l'opzione di configurazione `corpusDir`. Questa directory conterrà due voci: (1) una directory denominata `coverage` con file JSON che possono essere riprodotti da Echidna e (2) un file di testo semplice denominato `covered.txt`, una copia del codice sorgente con annotazioni di copertura.
Se esegui l'esempio `tests/solidity/basic/flags.sol`, Echidna salverà alcuni file di transazioni serializzate nella directory `coverage` e un file `covered.$(date +%s).txt` con le seguenti righe:```text
*r | function set0(int val) public returns (bool){
* | if (val % 100 == 0)
* | flag0 = false;
}
*r | function set1(int val) public returns (bool){
* | if (val % 10 == 0 && !flag0)
* | flag1 = false;
}
Il nostro strumento contrassegna ogni traccia di esecuzione nel corpus con il seguente "marcatore di riga":
* se un'esecuzione è terminata con uno STOPr se un'esecuzione è terminata con un REVERTo se un'esecuzione è terminata con un errore out-of-gase se un'esecuzione è terminata con qualsiasi altro errore (divisione per zero, fallimento di un'asserzione, ecc.)Echidna può testare contratti compilati con diversi sistemi di build per contratti intelligenti, tra cui Foundry, Hardhat e Truffle, utilizzando crytic-compile. Per invocare Echidna con il framework di compilazione corrente, usa echidna ..
Inoltre, Echidna supporta due modalità per testare contratti complessi. In primo luogo, si può sfruttare lo stato di rete esistente e usarlo come stato di base per Echidna. In secondo luogo, Echidna può chiamare qualsiasi contratto con un ABI noto passando il corrispondente sorgente Solidity nella CLI. Usa allContracts: true nella tua configurazione per attivarlo.
Il nostro repository Building Secure Smart Contracts contiene un corso intensivo su Echidna, inclusi esempi, lezioni ed esercizi.
Esiste un'action di Echidna che può essere utilizzata per eseguire echidna come parte di un
workflow di GitHub Actions. Fai riferimento al
repository crytic/echidna-action per
le istruzioni d'uso e gli esempi.