crytic/echidnaFuzzer de contrats intelligents Ethereum
Echidna est une créature étrange qui se nourrit de bugs et est hautement électrosensible (avec toutes nos excuses à Jacob Stanley)
Plus sérieusement, Echidna est un programme Haskell conçu pour le fuzzing et les tests basés sur les propriétés des contrats intelligents Ethereum. Il utilise des campagnes de fuzzing sophistiquées basées sur une grammaire et sur une ABI de contrat pour falsifier des prédicats définis par l'utilisateur ou des assertions Solidity. Nous avons conçu Echidna avec la modularité à l'esprit, afin qu'il puisse être facilement étendu pour inclure de nouvelles mutations ou tester des contrats spécifiques dans des cas particuliers.
.. et un magnifique logo artisanal en haute résolution.
La fonctionnalité principale d'Echidna est un exécutable appelé echidna, qui prend en entrée un contrat et une liste
d'invariants (propriétés qui doivent toujours rester vraies). Pour chaque invariant, il génère
des séquences aléatoires d'appels au contrat et vérifie si l'invariant tient. S'il parvient à trouver un moyen
de falsifier l'invariant, il affiche la séquence d'appels correspondante. S'il n'y parvient pas, vous avez une certaine
assurance que le contrat est sûr.
Les invariants sont exprimés sous forme de fonctions Solidity dont les noms commencent par echidna_, ne prennent aucun argument et renvoient un booléen. Par exemple, si vous avez une variable balance qui ne doit jamais descendre en dessous de 20, vous pouvez écrire une fonction supplémentaire dans votre contrat comme celle-ci :```solidity
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
Pour vérifier ces invariants, exécutez :```sh
$ echidna myContract.sol
Un exemple de contrat avec des tests se trouve dans tests/solidity/basic/flags.sol. Pour l'exécuter, vous devez exécuter :```sh $ echidna tests/solidity/basic/flags.sol
Echidna devrait trouver une séquence d'appels qui falsifie `echidna_sometimesfalse` et devrait être incapable de trouver une entrée falsifiante pour `echidna_alwaystrue`.
### Modes de test
L'exemple ci-dessus utilise le mode **property** par défaut, mais Echidna prend en charge plusieurs modes de test, configurés via `testMode` dans le fichier de configuration ou `--test-mode` sur la CLI :
* **`property`** (par défaut) : Teste les fonctions préfixées par `echidna_` qui renvoient un `bool`.
* **`assertion`** : Détecte les échecs d'assertion provenant de `assert()` et des helpers `assertX` de Foundry (`assertTrue`, `assertEq`, etc.).
* **`foundry`** : Exécute des tests de style Foundry, en suivant ses conventions de nommage : tests unitaires et de fuzzing préfixés par `test` (ceux préfixés par `testFail` sont censés revert) et invariants stateful préfixés par `invariant` ou `statefulFuzz`. Les fonctions préfixées par `check` et `prove` sont des points d'entrée symboliques, mais comme ce mode est une campagne de fuzzing, elles sont fuzzées comme n'importe quelle autre fonction de test.
* **`verification`** : Vérifie symboliquement chaque fonction du contrat à l'aide d'une seule transaction. Les fonctions préfixées par `check` et `prove` sont toujours utilisées comme points d'entrée.
* **`overflow`** : Détecte les dépassements/sous-dépassements d'entiers (Solidity >= 0.8.0).
* **`optimization`** : Maximise la valeur de retour des fonctions préfixées par `echidna_` qui renvoient un `int256` (utilise le même préfixe configurable que le mode property).
* **`exploration`** : Collecte la couverture sans vérifier les propriétés.
### Collecte et visualisation de la couverture
Après avoir terminé une campagne, Echidna peut sauvegarder un **corpus** maximisant la couverture dans un répertoire spécial spécifié avec l'option de configuration `corpusDir`. Ce répertoire contiendra deux entrées : (1) un répertoire nommé `coverage` avec des fichiers JSON qui peuvent être rejoués par Echidna et (2) un fichier en texte brut nommé `covered.txt`, une copie du code source avec des annotations de couverture.
Si vous exécutez l'exemple `tests/solidity/basic/flags.sol`, Echidna sauvegardera quelques fichiers de transactions sérialisées dans le répertoire `coverage` et un fichier `covered.$(date +%s).txt` avec les lignes suivantes :```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;
}
Notre outil signale chaque trace d'exécution du corpus avec le « marqueur de ligne » suivant :
* si une exécution s'est terminée par un STOPr si une exécution s'est terminée par un REVERTo si une exécution s'est terminée par une erreur out-of-gase si une exécution s'est terminée par toute autre erreur (division par zéro, échec d'assertion, etc.)Echidna peut tester des contrats compilés avec différents systèmes de build de contrats intelligents, notamment Foundry, Hardhat et Truffle, en utilisant crytic-compile. Pour invoquer Echidna avec le framework de compilation actuel, utilisez echidna ..
En outre, Echidna prend en charge deux modes de test de contrats complexes. Premièrement, on peut tirer parti d'un état réseau existant et l'utiliser comme état de base pour Echidna. Deuxièmement, Echidna peut appeler n'importe quel contrat dont l'ABI est connue en passant le code source Solidity correspondant dans la CLI. Utilisez allContracts: true dans votre configuration pour activer cette option.
Notre dépôt Building Secure Smart Contracts contient un cours accéléré sur Echidna, incluant des exemples, des leçons et des exercices.
Il existe une action Echidna qui peut être utilisée pour exécuter echidna dans le cadre d'un workflow GitHub Actions. Veuillez consulter le dépôt crytic/echidna-action pour les instructions d'utilisation et des exemples.