Passer au contenu principal

Comment utiliser Echidna pour tester les contrats intelligents

Solidity
contrats intelligents
sécurité
test
fuzzing
Avancé
Trailofbits
10 avril 2020
14 minutes de lecture

Installation

Echidna peut être installé via Docker ou en utilisant un binaire précompilé.

Echidna via Docker

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

La dernière commande exécute eth-security-toolbox dans un docker qui a accès à votre répertoire actuel. Vous pouvez modifier les fichiers depuis votre hôte, et exécuter les outils sur les fichiers depuis le docker

Dans Docker, exécutez :

solc-select 0.5.11
cd /home/training

Binaire

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

Introduction au fuzzing basé sur les propriétés

Echidna est un fuzzer basé sur les propriétés, que nous avons décrit dans nos précédents articles de blog (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Fuzzing

Le fuzzing (opens in a new tab) est une technique bien connue dans la communauté de la sécurité. Elle consiste à générer des entrées plus ou moins aléatoires pour trouver des bogues dans le programme. Les fuzzers pour les logiciels traditionnels (tels que AFL (opens in a new tab) ou LibFuzzer (opens in a new tab)) sont connus pour être des outils efficaces pour trouver des bogues.

Au-delà de la génération purement aléatoire d'entrées, il existe de nombreuses techniques et stratégies pour générer de bonnes entrées, notamment :

  • Obtenir des retours de chaque exécution et les utiliser pour guider la génération. Par exemple, si une nouvelle entrée générée mène à la découverte d'un nouveau chemin, il peut être judicieux de générer de nouvelles entrées proches de celle-ci.
  • Générer l'entrée en respectant une contrainte structurelle. Par exemple, si votre entrée contient un en-tête avec une somme de contrôle, il sera logique de laisser le fuzzer générer une entrée validant la somme de contrôle.
  • Utiliser des entrées connues pour en générer de nouvelles : si vous avez accès à un grand jeu de données d'entrées valides, votre fuzzer peut générer de nouvelles entrées à partir de celles-ci, plutôt que de commencer la génération à partir de zéro. On les appelle généralement des seeds.

Fuzzing basé sur les propriétés

Echidna appartient à une famille spécifique de fuzzer : le fuzzing basé sur les propriétés, fortement inspiré de QuickCheck (opens in a new tab). Contrairement à un fuzzer classique qui essaiera de trouver des plantages, Echidna essaiera de rompre des invariants définis par l'utilisateur.

Dans les contrats intelligents, les invariants sont des fonctions Solidity, qui peuvent représenter n'importe quel état incorrect ou invalide que le contrat peut atteindre, notamment :

  • Contrôle d'accès incorrect : l'attaquant est devenu le propriétaire du contrat.
  • Machine d'état incorrecte : les jetons peuvent être transférés alors que le contrat est en pause.
  • Arithmétique incorrecte : l'utilisateur peut provoquer un underflow de son solde et obtenir un nombre illimité de jetons gratuits.

Tester une propriété avec Echidna

Nous verrons comment tester un contrat intelligent avec Echidna. La cible est le contrat intelligent suivant 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}
Afficher tout

Nous supposerons que ce jeton doit avoir les propriétés suivantes :

  • N'importe qui peut avoir au maximum 1000 jetons
  • Le jeton ne peut pas être transféré (ce n'est pas un jeton ERC20)

Écrire une propriété

Les propriétés Echidna sont des fonctions Solidity. Une propriété doit :

  • Ne pas avoir d'argument
  • Renvoyer true si elle réussit
  • Avoir un nom qui commence par echidna

Echidna :

  • Générer automatiquement des transactions arbitraires pour tester la propriété.
  • Signaler toute transaction qui amène une propriété à renvoyer false ou à lever une erreur.
  • Ignorer les effets de bord lors de l'appel d'une propriété (c.-à-d. que si la propriété modifie une variable d'état, la modification est annulée après le test)

La propriété suivante vérifie que l'appelant n'a pas plus de 1000 jetons :

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

Utilisez l'héritage pour séparer votre contrat de vos propriétés :

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) met en œuvre la propriété et hérite du jeton.

Initialiser un contrat

Echidna a besoin d'un constructeur sans argument. Si votre contrat nécessite une initialisation spécifique, vous devez la faire dans le constructeur.

Il y a quelques adresses spécifiques dans Echidna :

  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 qui appelle le constructeur.
  • 0x10000, 0x20000 et 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 qui appellent aléatoirement les autres fonctions.

Nous n'avons pas besoin d'initialisation particulière dans notre exemple actuel, par conséquent notre constructeur est vide.

Exécuter Echidna

Echidna se lance avec :

echidna-test contract.sol

Si contract.sol contient plusieurs contrats, vous pouvez spécifier la cible :

echidna-test contract.sol --contract MyContract

Résumé : Tester une propriété

Ce qui suit résume l'exécution d'Echidna sur notre exemple :

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  }
echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Afficher tout

Echidna a trouvé que la propriété est violée si backdoor est appelée.

Filtrer les fonctions à appeler pendant une campagne de fuzzing

Nous verrons comment filtrer les fonctions à fuzzer. La cible est le contrat intelligent suivant :

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}
Afficher tout

Ce petit exemple force Echidna à trouver une certaine séquence de transactions pour modifier une variable d'état. C'est difficile pour un fuzzer (il est recommandé d'utiliser un outil d'exécution symbolique comme Manticore (opens in a new tab)). Nous pouvons exécuter Echidna pour vérifier cela :

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

Filtrage des fonctions

Echidna a du mal à trouver la séquence correcte pour tester ce contrat, car les deux fonctions de réinitialisation (reset1 et reset2) mettront toutes les variables d'état à false. Cependant, nous pouvons utiliser une fonctionnalité spéciale d'Echidna pour soit mettre sur liste noire la fonction de réinitialisation, soit mettre sur liste blanche uniquement les fonctions f, g, h et i.

Pour mettre des fonctions sur liste noire, nous pouvons utiliser ce fichier de configuration :

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

Une autre approche pour filtrer les fonctions consiste à lister les fonctions sur liste blanche. Pour ce faire, nous pouvons utiliser ce fichier de configuration :

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]
  • filterBlacklist est true par défaut.
  • Le filtrage sera effectué uniquement par nom (sans les paramètres). Si vous avez f() et f(uint256), le filtre "f" correspondra aux deux fonctions.

Exécuter Echidna

Pour exécuter Echidna avec un fichier de configuration blacklist.yaml :

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

Echidna trouvera la séquence de transactions pour falsifier la propriété presque immédiatement.

Résumé : Filtrage des fonctions

Echidna peut soit mettre sur liste noire, soit mettre sur liste blanche les fonctions à appeler pendant une campagne de fuzzing en utilisant :

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

Echidna lance une campagne de fuzzing soit en mettant sur liste noire f1, f2 et f3, soit en appelant uniquement celles-ci, en fonction de la valeur du booléen filterBlacklist.

Comment tester l'assertion de Solidity avec Echidna

Dans ce court tutoriel, nous allons montrer comment utiliser Echidna pour tester la vérification d'assertions dans les contrats. Supposons que nous ayons un contrat comme celui-ci :

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}
Afficher tout

Écrire une assertion

Nous voulons nous assurer que tmp est inférieur ou égal à counter après avoir renvoyé leur différence. Nous pourrions écrire une propriété Echidna, mais nous devrons stocker la valeur de tmp quelque part. À la place, nous pourrions utiliser une assertion comme celle-ci :

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}
Afficher tout

Exécuter Echidna

Pour activer le test d'échec d'assertion, créez un fichier de configuration Echidna (opens in a new tab) config.yaml :

1checkAsserts: true

Lorsque nous exécutons ce contrat dans Echidna, nous obtenons les résultats attendus :

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
Afficher tout

Comme vous pouvez le voir, Echidna signale un échec d'assertion dans la fonction inc. Il est possible d'ajouter plus d'une assertion par fonction, mais Echidna ne peut pas dire quelle assertion a échoué.

Quand et comment utiliser les assertions

Les assertions peuvent être utilisées comme alternatives aux propriétés explicites, surtout si les conditions à vérifier sont directement liées à l'utilisation correcte d'une opération f. L'ajout d'assertions après un morceau de code garantira que la vérification aura lieu immédiatement après son exécution :

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

Au contraire, l'utilisation d'une propriété Echidna explicite exécutera des transactions de manière aléatoire et il n'y a aucun moyen simple de forcer le moment exact où elle sera vérifiée. Il est toujours possible d'utiliser cette solution de contournement :

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

Cependant, il y a quelques problèmes :

  • Elle échoue si f est déclarée comme internal ou external.
  • On ne sait pas clairement quels arguments devraient être utilisés pour appeler f.
  • Si f revert, la propriété échouera.

En général, nous recommandons de suivre la recommandation de John Regehr (opens in a new tab) sur la façon d'utiliser les assertions :

  • Ne forcez aucun effet de bord lors de la vérification de l'assertion. Par exemple : assert(ChangeStateAndReturn() == 1)
  • Ne faites pas d'assertions sur des déclarations évidentes. Par exemple assert(var >= 0) où var est déclaré en tant que uint.

Enfin, veuillez ne pas utiliser require à la place d'assert, car Echidna ne sera pas en mesure de le détecter (mais le contrat sera annulé de toute façon).

Résumé : Vérification d'assertion

Ce qui suit résume l'exécution d'Echidna sur notre exemple :

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}
Afficher tout
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
Afficher tout

Echidna a découvert que l'assertion dans inc peut échouer si cette fonction est appelée plusieurs fois avec de grands arguments.

Collecter et modifier un corpus Echidna

Nous verrons comment collecter et utiliser un corpus de transactions avec Echidna. La cible est le contrat intelligent suivant 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 == 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}
Afficher tout

Ce simple exemple oblige Echidna à trouver certaines valeurs pour changer une variable d'état. C'est difficile pour un fuzzer (il est recommandé d'utiliser un outil d'exécution symbolique comme Manticore (opens in a new tab)). Nous pouvons exécuter Echidna pour vérifier cela :

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

Cependant, nous pouvons toujours utiliser Echidna pour collecter le corpus lors de l'exécution de cette campagne de fuzzing.

Collecte d'un corpus

Pour activer la collecte de corpus, créez un répertoire de corpus :

mkdir corpus-magic

Et un fichier de configuration Echidna (opens in a new tab) config.yaml :

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

Maintenant nous pouvons exécuter notre outil et vérifier le corpus collecté :

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

Echidna ne peut toujours pas trouver les bonnes valeurs magiques, mais nous pouvons jeter un œil sur le corpus qu'il a collecté. Par exemple, l'un de ces fichiers était :

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]
Afficher tout

Évidemment, cette entrée ne déclenchera pas l'échec de notre propriété. Cependant, au cours de la prochaine étape, nous verrons comment la modifier en ce sens.

Amorcer un corpus

Echidna a besoin d'aide pour gérer la fonction magic. Nous allons copier et modifier l'entrée pour utiliser des paramètres appropriés pour elle :

cp corpus/2712688662897926208.txt corpus/new.txt

Nous allons modifier new.txt pour appeler magic(42,129,333,0). Maintenant, nous pouvons relancer 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
Afficher tout

Cette fois-ci, il a conclu immédiatement que la propriété a été compromise.

Trouver les transactions à forte consommation de gaz

Nous verrons comment trouver avec Echida les transactions à forte consommation de gaz. La cible est le contrat intelligent suivant :

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}
Afficher tout

Ici, expensive peut avoir une grande consommation de gaz.

Actuellement, Echidna a toujours besoin d'une propriété pour tester : ici, echidna_test renvoie toujours true. Nous pouvons exécuter Echidna pour vérifier cela :

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

Mesurer la consommation de gaz

Pour activer la consommation de gaz avec Echidna, créez un fichier de configuration config.yaml :

1estimateGas: true

Dans cet exemple, nous allons également réduire la taille de la séquence de transaction pour faciliter la compréhension des résultats :

1seqLen: 2
2estimateGas: true

Exécuter Echidna

Une fois que nous avons créé le fichier de configuration, nous pouvons exécuter Echidna comme ceci :

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
Afficher tout

Filtrer les appels qui réduisent le gaz

Le tutoriel ci-dessus sur le filtrage des fonctions à appeler pendant une campagne de fuzzing montre comment supprimer certaines fonctions de vos tests.
Cela peut être essentiel pour obtenir une estimation précise du gaz. Prenons l'exemple suivant :

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}
Afficher tout

Si Echidna peut appeler toutes les fonctions, il ne trouvera pas facilement les transactions avec un coût de gaz élevé :

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
Afficher tout

C'est parce que le coût dépend de la taille de addrs et que les appels aléatoires ont tendance à laisser le tableau presque vide. Mettre sur liste noire pop et clear nous donne de bien meilleurs résultats :

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

Résumé : Trouver les transactions à forte consommation de gaz

Echidna peut trouver des transactions avec une forte consommation de gaz en utilisant l'option de configuration estimateGas :

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

Echidna rapportera une séquence avec la consommation maximale de gaz pour chaque fonction, une fois que la campagne de fuzzing est terminée.

Dernière mise à jour de la page : 21 octobre 2025

pete-vielhaberp (opens in a new tab)
pettinaripp (opens in a new tab)
nhszn (opens in a new tab)
+9

Ce tutoriel vous a été utile ?