Comment utiliser Manticore pour trouver des bugs dans les contrats intelligents

Le but de ce tutoriel est de dé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 avec 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 actif. Vous pouvez changer les fichiers depuis votre invite, et exécuter les outils sur les fichiers depuis le docker

Dans docker, lancez :

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 quelques mots

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ée sous la forme de 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, il est garanti reproductible.

Exemple de prédicat de chemin

Pour avoir une idée du fonctionnement du DSE, prenez 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 attribuer à a toute valeur autre que 65, par exemple a = 0.

Vérification des propriétés

Manticore permet un contrôle total sur toutes les exécutions 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; // pas de protections d’overflow
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 une valorisation de a et b pour laquelle 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 envisagez une version fixe:

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 au contrôle de l'overflow serait :

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

Cette formule ne peut pas être résolue, autrement dit c’est la preuve que la valeur safe_add, c augmentera toujours.

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

Lancer dans 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 par la commande suivante (project peut être un fichier Solidity, ou un répertoire de projet) :

$ manticore project

Vous obtiendrez une liste des cas de tests comme par exemple (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 ne lance pas de nouvelle transactions après le premier echec (par exemple : après un revert).

Le type de donnée que Manticore produira comme résultat sera de type dossier mcore_*. Parmi d’autres, vous trouverez dans le dossier :

• global.summary : avertissements de couverture de code et de compilateur
• test_XXXXX.summary: couverture de code, dernière instruction, soldes du compte 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 f appelé avec une valeur différente de 65.

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

Utilisez le flag --quick-mode si vous voulez une exploration rapide du code (il désactive les détecteurs de bugs, le calcul du gaz, ...)

Manipuler un contrat intelligent via l'API

Cette section décrit comment manipuler un contrat intelligent à travers l'API Python de Manticore. Vous pouvez créer un nouveau fichier avec l'extension python *.py et écrivez le code nécessaire en ajoutant les commandes API (dont les bases seront décrites ci-dessous) dans ce fichier, puis exécutez-le avec la commande $ python3 *. py. Vous pouvez également exécuter les commandes ci-dessous directement dans la console python, pour exécuter la console en utilisant la commande $ python3.

Création des comptes

La première chose que vous devriez faire est d'initier une nouvelle blockchain avec les commandes suivantes :

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

Une transaction brute est exécutée en utilisant m.create_account(opens in a new tab):

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

Une transaction brute est exécutée en utilisant 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# Init le contrat
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Afficher tout
 Copier

Résumé

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

Exécution des transactions

Manticore supporte 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 en utilisant 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 peut être soit concrète ou symbolique :

• 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 une valeur 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 voir l'explication de la fonction de repli dans l'article Hands on the Ethernaut CTF(opens in a new tab) pour comprendre comment fonctionne la sélection de fonctions.

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 value 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 exécutées via leurs noms

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 resultats sont 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 que cette méthode est appelée et Manticore génère des scénarios 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("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
Afficher tout
 Copier

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

Obtenir des chemins de lancement

Nous allons maintenant générer des entrées spécifiques pour les chemins soulevant une exception dans f(). La cible est 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 sur l'état d'objet

Chaque chemin exécuté a son é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é de REVERT/INVALID)
• m.killed_states(opens in a new tab) : liste des états qui sont morts
• m.all_states(opens in a new tab) : tous les états

1for state in m.all_states:
2    # do something with state
 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 des 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 constitue les données retournées
• m.generate_testcase(state, name) génère des entrées pour l'état

Résumé : Obtenir un chemin de lancement

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## Verifie si l’execution se termine avec REVERT ou INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
Afficher tout
 Copier

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

Notez que nous aurions pu générer un script beaucoup plus simple, comme tous les états retournés par terminated_state ont REVERT ou INVALID dans leur résultat : cet exemple était uniquement destiné à montrer comment manipuler l'API.

Ajouter des contraintes

Nous verrons comment limiter 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 bogue avec a == 65 n'est pas un vrai bogue. La cible est 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, entre autres il fournit :

• Operators.AND,
• Operators.OR,
• Operators.UGT (unsigned greater than),
• Operators.UGE (unsigned greater than or equal to),
• Operators.ULT (unsigned lower than),
• Operators.ULE (unsigned lower than or equal to).

Pour importer le module, utilisez ce qui suit :

1from manticore.core.smtlib import Operators
 Copier

Operators.CONCAT est utilisé pour concaténer une table à une valeur. Par exemple, la valeur return_data d'une transaction doit être remplacée par une valeur à vérifier avec une autre valeur :

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

Contraintes

Vous pouvez utiliser des contraintes globalement ou pour un état spécifique.

Contrainte globale

Utilisez m.constrain(constraint) pour ajouter une contrainte globale. Par exemple, vous pouvez appeler un contrat à partir d'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

Utiliser l'état state.constrain(contrainte)(opens in a new tab) pour ajouter une contrainte à un état spécifique Il peut être utilisé pour contraindre l'état après son exploration pour vérifier une propriété dessus.

Vérifier les contraintes

Utilisez solver.check(state.contraints) pour savoir si une contrainte est toujours faisable. 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’etat est possible
 Copier

Résumé: Ajouter des contraintes

En ajoutant des contraintes 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## Verifie si l’execution se termine par REVERT ou INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # on ne considere pas le chemin quand a==65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug trouve, les resultats sont dans {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'Pas de bug trouve')
Afficher tout
 Copier

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