Comment utiliser Manticore pour trouver des bugs dans les contrats intelligents

Solidity

contrats intelligents

sécurité

tests

vérification formelle

Avancé

Trailofbits

Building secure contracts

13 janvier 2020

12 minutes de lecture

L'objectif de ce tutoriel est de montrer comment utiliser Manticore pour trouver automatiquement des bugs dans les contrats intelligents.

Installation

Manticore nécessite 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 conteneur 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 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 haut degré de conscience sémantique. Cette technique est basée sur la découverte de « chemins de programme », représentés sous forme de formules mathématiques appelées path predicates. Conceptuellement, cette technique opère sur les prédicats de chemin en deux étapes :

Ils sont construits en utilisant des contraintes sur les entrées du programme.
Ils sont utilisés pour générer des entrées de programme qui provoqueront 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 d'une exécution concrète. Par exemple, si l'analyse trouve un dépassement de capacité d'entier, il est garanti d'être reproductible.

Exemple de prédicat de chemin

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

function f(uint a){

  if (a == 65) {
      // Un bug est présent
  }

}

Comme f() contient deux chemins, une 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 à ce qu'on appelle un solutionneur SMT (opens in a new tab), qui essaiera de résoudre l'équation. Pour Path 1, le solutionneur dira que le chemin peut être exploré avec a = 65. Pour Path 2, le solutionneur peut donner à a n'importe quelle valeur autre que 65, par exemple a = 0.

Vérification des propriétés

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

Considérez l'exemple suivant :

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // aucune protection contre le dépassement de capacité
  return c;
}

Ici, il n'y a qu'un seul chemin à explorer dans la fonction :

Chemin 1 : c = a + b

En utilisant Manticore, vous pouvez vérifier le dépassement de capacité 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 évaluation 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 de capacité. Par exemple, le solutionneur peut générer l'entrée a = 10 , b = MAXUINT256.

Si vous considérez une version corrigée :

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

La formule associée avec la vérification de dépassement de capacité 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.

La 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) :

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Exécuter 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 la sortie des cas de test comme celle-ci (l'ordre peut changer) :

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

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

Manticore affichera les informations dans un répertoire mcore_*. Entre autres, vous trouverez 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 trouve 7 cas de test, qui correspondent à (l'ordre des noms de fichiers peut changer) :

	Transaction 0	Transaction 1	Transaction 2	Résultat
test_00000000.tx	Création de contrat	f(!=65)	f(!=65)	STOP
test_00000001.tx	Création de contrat	fonction de repli		REVERT
test_00000002.tx	Création de contrat			RETURN
test_00000003.tx	Création de contrat	f(65)		REVERT
test_00000004.tx	Création de contrat	f(!=65)		STOP
test_00000005.tx	Création de contrat	f(!=65)	f(65)	REVERT
test_00000006.tx	Création de contrat	f(!=65)	fonction de repli	REVERT

Le résumé de l'exploration f(!=65) indique que f est appelée avec n'importe quelle valeur différente de 65.

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

Utilisez l'indicateur --quick-mode si vous souhaitez une exploration rapide du code (cela désactive les détecteurs de bugs, le calcul du gaz, ...)

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 écrire le code nécessaire en ajoutant les commandes de l'API (dont les bases seront décrites ci-dessous) dans ce fichier, 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éation de comptes

La première chose que vous devez faire est d'initier une nouvelle chaîne de blocs avec les commandes suivantes :

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

Un compte non contractuel est créé en utilisant m.create_account (opens in a new tab) :

user_account = m.create_account(balance=1000)

Un contrat Solidity peut être déployé en utilisant m.solidity_create_contract (opens in a new tab) :

source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}
'''
# Initiate the contract
contract_account = m.solidity_create_contract(source_code, owner=user_account)

Résumé

Vous pouvez créer des comptes d'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 de 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 en utilisant m.transaction (opens in a new tab) :

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

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 :

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

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 repli 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, depuis user_account, et avec 0 ether, utilisez :

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

Si value de la transaction n'est pas spécifié, il 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 :

print("Results are in {}".format(m.workspace))

Terminer l'exploration

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

Résumé : Exécution sous Manticore

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

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

print("Results are in {}".format(m.workspace))
m.finalize() # arrêter l'exploration

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

Obtenir les chemins d'erreur

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

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Utilisation des informations d'état

Chaque chemin exécuté a son état de la chaîne de blocs. Un état est soit prêt, soit 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) : la liste des états qui sont tués
m.all_states (opens in a new tab) : tous les états

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

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 renvoyées par la dernière transaction

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

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

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 :

m.generate_testcase(state, 'BugFound')

Résumé

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

Résumé : Obtenir le chemin d'erreur

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

## Vérifier si une exécution se termine par une annulation ou INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        m.generate_testcase(state, 'ThrowFound')

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

Notez que 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 à démontrer comment manipuler l'API.

Ajout de 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) :

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Opérateurs

Le module Operators (opens in a new tab) facilite la manipulation des contraintes, il fournit entre autres :

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

Pour importer le module, utilisez ce qui suit :

from manticore.core.smtlib import Operators

Operators.CONCAT est utilisé pour concaténer un tableau à une valeur. Par exemple, le return_data d'une transaction doit être modifié en une valeur pour être vérifié par rapport à une autre valeur :

last_return = Operators.CONCAT(256, *last_return)

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 :

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

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 :

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

Résumé : Ajout de contraintes

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

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

m = ManticoreEVM()

with open("example.sol") as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

no_bug_found = True

## Vérifier si une exécution se termine par une annulation ou INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # nous ne considérons pas le chemin où a == 65
        condition = symbolic_var != 65
        if m.generate_testcase(state, name="BugFound", only_if=condition):
            print(f'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

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