Comment utiliser Echidna pour tester les contrats intelligents

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 changer les fichiers depuis votre invite, 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 blogs précédents (1(opens in a new tab), 2(opens in a new tab), 3(opens in a new tab)).

Fuzzing (test à données aléatoires)

Le Fuzzing(opens in a new tab) est une technique bien connue dans la communauté concernée par la sécurité. Il 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 (comme AFL(opens in a new tab) ou LibFuzzer(opens in a new tab)) sont connus pour être des outils efficaces quant au repérage des bogues.

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

• Obtenez des commentaires en retour de chaque exécution et la génération de guides en les utilisant. Par exemple, si une entrée nouvellement générée mène à la découverte d'un nouveau chemin, il peut y avoir un sens à générer de nouvelles entrées s'en rapprochant.
• Génération d'entrée dans le respect d'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 générer de nouvelles entrées : si vous avez accès à un grand jeu de données d'entrée valide, votre fuzzer peut générer de nouvelles entrées à partir d'elles, plutôt que de faire partir de zéro sa génération. Elles sont généralement appelées seeds.

Fuzzing orienté propriétés

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

Dans les contrats intelligents, les invariants sont des fonctions Solidity qui peuvent représenter tout état incorrect ou non valide que le contrat peut atteindre, y compris :

• 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 pendant que le contrat est suspendu.
• Arithmétique incorrecte : l'utilisateur peut faire déborder son solde et obtenir des jetons gratuits en illimités.

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
 Copier

Nous prendrons comme hypothèse 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 contenir aucun argument
• Renvoyer true si elle a réussi
• Avoir son nom commençant par echidna

Echidna va :

• Générer automatiquement des transactions arbitraires pour tester la propriété.
• Signaler toute transaction menant à une propriété pour renvoyer false ou retourner une erreur.
• Ignorer l'effet secondaire lors de l'appel d'une propriété (c'est-à-dire si la propriété change une variable d'état, elle est rejetée après le test)

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

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

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  }
 Copier

token.sol(opens in a new tab) implémente la propriété et hérite du jeton.

Démarrer un contrat

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

Il existe quelques adresses spécifiques dans Echidna :

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA7 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, de fait, 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 permet de résumer le lancement d'Echidna pour 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  }
 Copier

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é sera compromise si backdoor est appelé.

Fonctions de filtrage à appeler lors d'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
 Copier

Ce petit exemple oblige Echidna à trouver une certaine séquence de transactions pour modifier une variable d'état. C'est une opération compliquée 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 ceci :

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

Fonctions de filtrage

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 sur false. Cependant, nous pouvons utiliser une fonctionnalité spéciale d'Echidna pour mettre sur liste noire la fonction reset ou pour ne mettre sur liste blanche que les fonctions f, g, h et i.

Pour bloquer les fonctions, nous pouvons utiliser ce fichier de configuration :

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

Une autre approche des fonctions de filtrage est de lister les fonctions dans une liste blanche. Pour cela, nous pouvons utiliser ce fichier de configuration :

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist est sur true par défaut.
• Le filtrage sera effectué uniquement par le nom (sans les paramètres). Si vous avez f() et f(uint256), le filtre "f" correspondra aux deux fonctions.

Exécuter Echidna

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 presque immédiatement la séquence des transactions pour falsifier la propriété.

Résumé : fonctions de filtrage

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

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidna débute une campagne de fuzzing soit en ajoutant f1, f2 et f3 sur la liste noire, ou en les appelant uniquement selon la valeur booléenne définie dans filterBlacklist.

Comment tester les assertions de Solidity avec Echidna

Dans ce court tutoriel, nous allons montrer comment utiliser Echidna pour tester la vérification des 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
 Copier

Écrire une assertion

Nous voulons nous assurer que tmp est inférieur ou égal à counter après avoir retourné sa différence. Nous pourrions écrire une propriété Echidna, mais nous devrons stocker la valeur tmp quelque part. Au lieu de cela, 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
 Copier

Exécuter Echidna

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

1checkAsserts: true

Lorsque nous exécutons ce contrat sur Echidna, nous obtenons les résultats escomptés :

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. L'ajout de plus d'une assertion par fonction est possible, 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, spécialement si les conditions à vérifier sont directement liées à l'utilisation correcte de certaines opérations f. Ajouter des assertions après certains codes garantira que la vérification se produira immédiatement après son exécution :

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

Au contraire, utiliser une propriété Echidna explicite va exécuter aléatoirement des transactions et il n'y a pas de moyen facile de forcer le moment exact où elle sera vérifiée. Il est toujours possible de faire ce contournement :

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

Cependant, il existe quelques problèmes :

• Il échoue si f est déclaré comme internal ou external.
• Il n'est pas clair de savoir quels arguments doivent être utilisés pour appeler f.
• Si f s'annule, 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 secondaire lors de la vérification de l'assertion. Par exemple : assert(ChangeStateAndReturn() == 1)
• Ne revendiquez pas des déclarations évidentes. Par exemple assert(var >= 0) où var est déclaré comme uint.

Enfin, s'il vous plaît n'utilisez pas require au lieu de assert, car dans ce cas, 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 permet de résumer le lancement d'Echidna pour 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
 Copier

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 trouvé que l'assertion dans inc peut échouer si cette fonction est appelée plusieurs fois avec de grands arguments.

Collecte et modification d'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
 Copier

Ce simple exemple oblige Echidna à trouver certaines valeurs pour changer une variable d'état. C'est une opération compliquée 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 ceci :

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.

Récupération 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
 Copier

É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.

Alimenter un corpus

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

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.

Recherche de 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
 Copier

Ici expensive peut avoir une grande consommation de gaz.

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

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

Mesurer la consommation de gaz

Pour activer avec Echidna la consommation de gaz, 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

Run 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

• Le gaz affiché est une estimation fournie par HEVM(opens in a new tab).

Filtrer les appels de réduction de gaz

Le tutoriel ci-dessus sur les fonctions de filtrage à appeler lors d'une campagne de fuzzing montre comment supprimer certaines fonctions de votre test.
Cela peut être critique pour obtenir une estimation précise de 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
 Copier

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 des 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 des transactions avec une 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.