Comment utiliser Manticore pour trouver des bugs dans les contrats intelligents

Le but de ce tutoriel est de montrer comment utiliser Manticore pour trouver automatiquement des bugs dans les contrats intelligents.

Installation

Manticore requiert python >= 3.6. Il peut être installé via pip ou en utilisant docker.

Manticore 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

À l'intérieur de docker, exécutez :

solc-select 0.5.11
cd /home/trufflecon/

Manticore via pip

pip3 install --user manticore

solc 0.5.11 est recommandé.

Exécuter un script

Pour exécuter un script python avec python 3 :

python3 script.py

Introduction à l'exécution symbolique dynamique

L'exécution symbolique dynamique en bref

L'exécution symbolique dynamique (DSE) est une technique d'analyse de programme qui explore un espace d'état avec un degré élevé de conscience sémantique. Cette technique est basée sur la découverte de « chemins de programme », représentés par des formules mathématiques appelées prédicats de chemin. Conceptuellement, cette technique opère sur les prédicats de chemin en deux étapes :

1. Ils sont construits en utilisant des contraintes sur les entrées du programme.
2. Ils sont utilisés pour générer des entrées de programme qui entraîneront l'exécution des chemins associés.

Cette approche ne produit aucun faux positif dans le sens où tous les états de programme identifiés peuvent être déclenchés lors de l'exécution concrète. Par exemple, si l'analyse trouve un dépassement d'entier, sa reproductibilité est garantie.

Exemple de prédicat de chemin

Pour avoir un aperçu du fonctionnement du DSE, considérez l'exemple suivant :

1function f(uint a){
2
3  if (a == 65) {
4      // Un bug est présent
5  }
6
7}
Copier

Comme f() contient deux chemins, un DSE construira deux prédicats de chemin différents :

• Chemin 1 : a == 65
• Chemin 2 : Not (a == 65)

Chaque prédicat de chemin est une formule mathématique qui peut être donnée à un solveur SMT (opens in a new tab), qui tentera de résoudre l'équation. Pour le Chemin 1, le solveur dira que le chemin peut être exploré avec a = 65. Pour le Chemin 2, le solveur peut donner à a n'importe quelle valeur autre que 65, par exemple a = 0.

Vérifier les propriétés

Manticore permet un contrôle total sur l'exécution de chaque chemin. En conséquence, il vous permet d'ajouter des contraintes arbitraires à pratiquement n'importe quoi. Ce contrôle permet la création de propriétés sur le contrat.

Prenons l'exemple suivant :

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // aucune protection contre le dépassement
3  return c;
4}
Copier

Il n'y a ici qu'un seul chemin à explorer dans la fonction :

• Chemin 1 : c = a + b

En utilisant Manticore, vous pouvez vérifier le dépassement et ajouter des contraintes au prédicat de chemin :

• c = a + b AND (c < a OR c < b)

S'il est possible de trouver des valeurs pour a et b pour lesquelles le prédicat de chemin ci-dessus est réalisable, cela signifie que vous avez trouvé un dépassement. Par exemple, le solveur peut générer l'entrée a = 10, b = MAXUINT256.

Si vous considérez une version corrigée :

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
Copier

La formule associée à la vérification de dépassement serait :

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Cette formule ne peut pas être résolue ; en d'autres termes, c'est une preuve que dans safe_add, c augmentera toujours.

DSE est donc un outil puissant, qui peut vérifier des contraintes arbitraires sur votre code.

Exécution sous Manticore

Nous allons voir comment explorer un contrat intelligent avec l'API Manticore. La cible est le contrat intelligent suivant example.sol (opens in a new tab) :

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Afficher tout
Copier

Lancer une exploration autonome

Vous pouvez exécuter Manticore directement sur le contrat intelligent avec la commande suivante (project peut être un fichier Solidity, ou un répertoire de projet) :

$ manticore project

Vous obtiendrez en sortie des cas de test comme celui-ci (l'ordre peut changer) :

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Afficher tout

Sans informations supplémentaires, Manticore explorera le contrat avec de nouvelles transactions symboliques jusqu’à ce qu’il n’explore plus de nouveaux chemins dans le contrat. Manticore n'exécute pas de nouvelles transactions après un échec (p. ex., après une annulation).

Manticore générera les informations dans un répertoire mcore_*. Vous trouverez notamment dans ce répertoire :

• global.summary : couverture et avertissements du compilateur
• test_XXXXX.summary : couverture, dernière instruction, soldes des comptes par cas de test
• test_XXXXX.tx : liste détaillée des transactions par cas de test

Ici, Manticore a trouvé 7 cas de test, qui correspondent à (l'ordre des noms de fichier peut changer) :

Le résumé d'exploration f(!=65) indique que f est appelée avec une valeur différente de 65.

Comme vous pouvez le constater, Manticore génère un cas de test unique pour chaque transaction réussie ou annulée.

Utilisez l'option --quick-mode si vous voulez une exploration rapide du code (elle désactive les détecteurs de bugs, le calcul du gaz, etc.)

Manipuler un contrat intelligent via l'API

Cette section décrit en détail comment manipuler un contrat intelligent via l'API Python de Manticore. Vous pouvez créer un nouveau fichier avec l'extension python .py et y écrire le code nécessaire en ajoutant les commandes de l'API (dont les bases sont décrites ci-dessous), puis l'exécuter avec la commande $ python3 *.py. Vous pouvez également exécuter les commandes ci-dessous directement dans la console Python ; pour lancer la console, utilisez la commande $ python3.

Créer des comptes

La première chose à faire est d'initialiser une nouvelle blockchain avec les commandes suivantes :

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Copier

Un compte externe (non-contrat) est créé à l'aide de m.create_account (opens in a new tab) :

1user_account = m.create_account(balance=1000)
Copier

Un contrat Solidity peut être déployé à l'aide de m.solidity_create_contract (opens in a new tab) :

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initialiser le contrat
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Afficher tout
Copier

Résumé

• Vous pouvez créer des comptes d'utilisateur et des comptes de contrat avec m.create_account (opens in a new tab) et m.solidity_create_contract (opens in a new tab).

Exécuter des transactions

Manticore prend en charge deux types de transactions :

• Transaction brute : toutes les fonctions sont explorées
• Transaction nommée : une seule fonction est explorée

Transaction brute

Une transaction brute est exécutée à l'aide de m.transaction (opens in a new tab) :

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Copier

L'appelant, l'adresse, les données ou la valeur de la transaction peuvent être soit concrets, soit symboliques :

• m.make_symbolic_value (opens in a new tab) crée une valeur symbolique.
• m.make_symbolic_buffer(size) (opens in a new tab) crée un tableau d'octets symbolique.

Par exemple :

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
Copier

Si les données sont symboliques, Manticore explorera toutes les fonctions du contrat pendant l'exécution de la transaction. Il sera utile de consulter l'explication de la fonction de secours dans l'article Hands on the Ethernaut CTF (opens in a new tab) pour comprendre comment fonctionne la sélection de fonction.

Transaction nommée

Les fonctions peuvent être exécutées via leur nom. Pour exécuter f(uint var) avec une valeur symbolique, à partir de user_account et avec 0 ether, utilisez :

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Copier

Si la valeur de la transaction n'est pas spécifiée, elle est de 0 par défaut.

Résumé

• Les arguments d'une transaction peuvent être concrets ou symboliques
• Une transaction brute explorera toutes les fonctions
• Les fonctions peuvent être appelées par leur nom

Espace de travail

m.workspace est le répertoire utilisé comme répertoire de sortie pour tous les fichiers générés :

1print("Les résultats se trouvent dans {}".format(m.workspace))
Copier

Terminer l'exploration

Pour arrêter l'exploration, utilisez m.finalize() (opens in a new tab). Aucune autre transaction ne devrait être envoyée une fois cette méthode appelée. Manticore génère alors des cas de test pour chaque chemin exploré.

Résumé : Exécution sous Manticore

En réunissant toutes les étapes précédentes, nous obtenons :

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Les résultats se trouvent dans {}".format(m.workspace))
15m.finalize() # arrête l'exploration
Afficher tout
Copier

Vous pouvez retrouver tout le code ci-dessus dans example_run.py (opens in a new tab)

Obtenir les chemins qui lèvent une exception

Nous allons maintenant générer des entrées spécifiques pour les chemins levant une exception dans f(). La cible est toujours le contrat intelligent suivant example.sol (opens in a new tab) :

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copier

Utiliser les informations d'état

Chaque chemin exécuté a son propre état de la blockchain. Un état est soit prêt, soit il est tué, ce qui signifie qu'il atteint une instruction THROW ou REVERT :

• m.ready_states (opens in a new tab) : la liste des états qui sont prêts (ils n'ont pas exécuté d'instruction REVERT/INVALID)
• m.killed_states (opens in a new tab) : la liste des états qui sont tués
• m.all_states (opens in a new tab) : tous les états

1for state in m.all_states:
2    # faire quelque chose avec l'état
Copier

Vous pouvez accéder aux informations d'état. Par exemple :

• state.platform.get_balance(account.address) : le solde du compte
• state.platform.transactions : la liste des transactions
• state.platform.transactions[-1].return_data : les données retournées par la dernière transaction

Les données retournées par la dernière transaction sont un tableau, qui peut être converti en une valeur avec ABI.deserialize, par exemple :

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Copier

Comment générer un cas de test

Utilisez m.generate_testcase(state, name) (opens in a new tab) pour générer un cas de test :

1m.generate_testcase(state, 'BugFound')
Copier

Résumé

• Vous pouvez itérer sur l'état avec m.all_states
• state.platform.get_balance(account.address) retourne le solde du compte
• state.platform.transactions retourne la liste des transactions
• transaction.return_data correspond aux données retournées
• m.generate_testcase(state, name) génère des entrées pour l'état

Résumé : Obtenir le chemin qui lève une exception

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Vérifier si une exécution se termine par REVERT ou INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Exception trouvée {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Afficher tout
Copier

Vous pouvez retrouver tout le code ci-dessus dans example_run.py (opens in a new tab)

Remarque : nous aurions pu générer un script beaucoup plus simple, car tous les états renvoyés par terminated_state ont REVERT ou INVALID dans leur résultat. Cet exemple visait uniquement à montrer comment manipuler l'API.

Ajouter des contraintes

Nous allons voir comment contraindre l'exploration. Nous ferons l'hypothèse que la documentation de f() indique que la fonction n'est jamais appelée avec a == 65, donc tout bug avec a == 65 n'est pas un vrai bug. La cible est toujours le contrat intelligent suivant example.sol (opens in a new tab) :

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
Copier

Opérateurs

Le module Opérateurs (opens in a new tab) facilite la manipulation des contraintes. Il fournit entre autres :

• Operators.AND,
• Operators.OR,
• Operators.UGT (supérieur à, non signé),
• Operators.UGE (supérieur ou égal à, non signé),
• Operators.ULT (inférieur à, non signé),
• Operators.ULE (inférieur ou égal à, non signé).

Pour importer le module, utilisez ce qui suit :

1from manticore.core.smtlib import Operators
Copier

Operators.CONCAT est utilisé pour concaténer un tableau à une valeur. Par exemple, les return_data d'une transaction doivent être transformées en une valeur pour être comparées à une autre valeur :

1last_return = Operators.CONCAT(256, *last_return)
Copier

Contraintes

Vous pouvez utiliser des contraintes de manière globale ou pour un état spécifique.

Contrainte globale

Utilisez m.constrain(constraint) pour ajouter une contrainte globale. Par exemple, vous pouvez appeler un contrat depuis une adresse symbolique et restreindre cette adresse à des valeurs spécifiques :

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
Copier

Contrainte d'état

Utilisez state.constrain(constraint) (opens in a new tab) pour ajouter une contrainte à un état spécifique. Cela peut être utilisé pour contraindre l'état après son exploration afin de vérifier une propriété sur celui-ci.

Vérification de contrainte

Utilisez solver.check(state.constraints) pour savoir si une contrainte est toujours réalisable. Par exemple, ce qui suit contraindra symbolic_value à être différent de 65 et vérifiera si l'état est toujours réalisable :

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # l'état est réalisable
Copier

Résumé : Ajouter des contraintes

En ajoutant une contrainte au code précédent, nous obtenons :

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Vérifier si une exécution se termine par REVERT ou INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # nous ne considérons pas le chemin où a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Bug trouvé, les résultats sont dans {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Aucun bug trouvé')
Afficher tout
Copier

Vous pouvez retrouver tout le code ci-dessus dans example_run.py (opens in a new tab)

Dernière mise à jour de la page : 26 avril 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Voir les contributeurs