Vai al contenuto principale

Come usare Manticore per trovare bug nei contratti intelligenti

Solidity
contratti intelligenti
sicurezza
test
verifica formale
Avanzato
Trailofbits
13 gennaio 2020
12 minuti di lettura

Lo scopo di questo tutorial è mostrare come usare Manticore per trovare automaticamente bug nei contratti intelligenti.

Installazione

Manticore richiede python >= 3.6. Può essere installato tramite pip o usando docker.

Manticore tramite docker

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

L'ultimo comando esegue eth-security-toolbox in un docker che ha accesso alla tua directory corrente. Puoi modificare i file dal tuo host ed eseguire gli strumenti sui file dal docker

All'interno di docker, esegui:

solc-select 0.5.11
cd /home/trufflecon/

Manticore tramite pip

pip3 install --user manticore

Si consiglia solc 0.5.11.

Eseguire uno script

Per eseguire uno script python con python 3:

python3 script.py

Introduzione all'esecuzione simbolica dinamica

L'esecuzione simbolica dinamica in breve

L'esecuzione simbolica dinamica (DSE) è una tecnica di analisi dei programmi che esplora uno spazio degli stati con un alto grado di consapevolezza semantica. Questa tecnica si basa sulla scoperta di "percorsi del programma", rappresentati come formule matematiche chiamate path predicates (predicati di percorso). Concettualmente, questa tecnica opera sui predicati di percorso in due passaggi:

  1. Vengono costruiti usando vincoli sull'input del programma.
  2. Vengono usati per generare input del programma che causeranno l'esecuzione dei percorsi associati.

Questo approccio non produce falsi positivi nel senso che tutti gli stati del programma identificati possono essere attivati durante l'esecuzione concreta. Ad esempio, se l'analisi trova un overflow di interi, è garantito che sia riproducibile.

Esempio di predicato di percorso

Per avere un'idea di come funziona la DSE, considera il seguente esempio:

1function f(uint a){
2
3  if (a == 65) {
4      // È presente un bug
5  }
6
7}

Poiché f() contiene due percorsi, una DSE costruirà due diversi predicati di percorso:

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

Ogni predicato di percorso è una formula matematica che può essere fornita a un cosiddetto risolutore SMT (opens in a new tab), che cercherà di risolvere l'equazione. Per il Percorso 1, il risolutore dirà che il percorso può essere esplorato con a = 65. Per il Percorso 2, il risolutore può dare ad a qualsiasi valore diverso da 65, ad esempio a = 0.

Verificare le proprietà

Manticore consente un controllo completo su tutta l'esecuzione di ogni percorso. Di conseguenza, ti permette di aggiungere vincoli arbitrari a quasi tutto. Questo controllo consente la creazione di proprietà sul contratto.

Considera il seguente esempio:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // nessuna protezione da overflow
3  return c;
4}

Qui c'è solo un percorso da esplorare nella funzione:

  • Percorso 1: c = a + b

Usando Manticore, puoi controllare l'overflow e aggiungere vincoli al predicato di percorso:

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

Se è possibile trovare una valutazione di a e b per cui il predicato di percorso sopra è fattibile, significa che hai trovato un overflow. Ad esempio, il risolutore può generare l'input a = 10 , b = MAXUINT256.

Se consideri una versione corretta:

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}

La formula associata con il controllo dell'overflow sarebbe:

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

Questa formula non può essere risolta; in altre parole questa è una prova che in safe_add, c aumenterà sempre.

La DSE è quindi uno strumento potente, che può verificare vincoli arbitrari sul tuo codice.

Esecuzione in Manticore

Vedremo come esplorare un contratto intelligente con l'API di Manticore. L'obiettivo è il seguente contratto intelligente 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}
Mostra tutto

Eseguire un'esplorazione autonoma

Puoi eseguire Manticore direttamente sul contratto intelligente con il seguente comando (project può essere un file Solidity o una directory di progetto):

$ manticore project

Otterrai l'output dei casi di test come questo (l'ordine potrebbe cambiare):

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...
Mostra tutto

Senza informazioni aggiuntive, Manticore esplorerà il contratto con nuove transazioni simboliche finché non esplorerà nuovi percorsi sul contratto. Manticore non esegue nuove transazioni dopo una fallita (es: dopo un revert).

Manticore produrrà le informazioni in una directory mcore_*. Tra le altre cose, troverai in questa directory:

  • global.summary: copertura e avvisi del compilatore
  • test_XXXXX.summary: copertura, ultima istruzione, saldi degli account per caso di test
  • test_XXXXX.tx: elenco dettagliato delle transazioni per caso di test

Qui Manticore trova 7 casi di test, che corrispondono a (l'ordine dei nomi dei file potrebbe cambiare):

Transazione 0Transazione 1Transazione 2Risultato
test_00000000.txCreazione del contrattof(!=65)f(!=65)STOP
test_00000001.txCreazione del contrattofunzione di fallbackREVERT
test_00000002.txCreazione del contrattoRETURN
test_00000003.txCreazione del contrattof(65)REVERT
test_00000004.txCreazione del contrattof(!=65)STOP
test_00000005.txCreazione del contrattof(!=65)f(65)REVERT
test_00000006.txCreazione del contrattof(!=65)funzione di fallbackREVERT

Il riepilogo dell'esplorazione f(!=65) indica f chiamata con qualsiasi valore diverso da 65.

Come puoi notare, Manticore genera un caso di test unico per ogni transazione riuscita o annullata.

Usa il flag --quick-mode se desideri un'esplorazione rapida del codice (disabilita i rilevatori di bug, il calcolo del gas, ...)

Manipolare un contratto intelligente tramite l'API

Questa sezione descrive in dettaglio come manipolare un contratto intelligente tramite l'API Python di Manticore. Puoi creare un nuovo file con estensione python *.py e scrivere il codice necessario aggiungendo i comandi dell'API (le cui basi saranno descritte di seguito) in questo file e poi eseguirlo con il comando $ python3 *.py. Inoltre puoi eseguire i comandi sottostanti direttamente nella console python; per avviare la console usa il comando $ python3.

Creare account

La prima cosa che dovresti fare è avviare una nuova blockchain con i seguenti comandi:

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

Un account non contrattuale viene creato usando m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)

Un contratto Solidity può essere distribuito usando 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# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Mostra tutto

Riepilogo

Eseguire transazioni

Manticore supporta due tipi di transazione:

  • Transazione grezza: tutte le funzioni vengono esplorate
  • Transazione nominata: viene esplorata solo una funzione

Transazione grezza

Una transazione grezza viene eseguita usando m.transaction (opens in a new tab):

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

Il chiamante, l'indirizzo, i dati o il valore della transazione possono essere concreti o simbolici:

Ad esempio:

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)

Se i dati sono simbolici, Manticore esplorerà tutte le funzioni del contratto durante l'esecuzione della transazione. Sarà utile vedere la spiegazione della funzione di fallback nell'articolo Hands on the Ethernaut CTF (opens in a new tab) per capire come funziona la selezione della funzione.

Transazione nominata

Le funzioni possono essere eseguite tramite il loro nome. Per eseguire f(uint var) con un valore simbolico, da user_account e con 0 ether, usa:

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

Se il value della transazione non è specificato, è 0 per impostazione predefinita.

Riepilogo

  • Gli argomenti di una transazione possono essere concreti o simbolici
  • Una transazione grezza esplorererà tutte le funzioni
  • Le funzioni possono essere chiamate con il loro nome

Spazio di lavoro

m.workspace è la directory usata come directory di output per tutti i file generati:

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

Terminare l'esplorazione

Per interrompere l'esplorazione usa m.finalize() (opens in a new tab). Nessuna ulteriore transazione dovrebbe essere inviata una volta chiamato questo metodo e Manticore genera casi di test per ciascuno dei percorsi esplorati.

Riepilogo: Esecuzione in Manticore

Mettendo insieme tutti i passaggi precedenti, otteniamo:

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() # interrompi l'esplorazione
Mostra tutto

Tutto il codice sopra lo puoi trovare in example_run.py (opens in a new tab)

Ottenere percorsi che generano eccezioni

Ora genereremo input specifici per i percorsi che sollevano un'eccezione in f(). L'obiettivo è ancora il seguente contratto intelligente 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}

Usare le informazioni di stato

Ogni percorso eseguito ha il suo stato della blockchain. Uno stato è pronto (ready) o è terminato (killed), il che significa che raggiunge un'istruzione THROW o REVERT:

1for state in m.all_states:
2    # fare qualcosa con lo stato

Puoi accedere alle informazioni di stato. Ad esempio:

  • state.platform.get_balance(account.address): il saldo dell'account
  • state.platform.transactions: l'elenco delle transazioni
  • state.platform.transactions[-1].return_data: i dati restituiti dall'ultima transazione

I dati restituiti dall'ultima transazione sono un array, che può essere convertito in un valore con ABI.deserialize, ad esempio:

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

Come generare un caso di test

Usa m.generate_testcase(state, name) (opens in a new tab) per generare un caso di test:

1m.generate_testcase(state, 'BugFound')

Riepilogo

  • Puoi iterare sullo stato con m.all_states
  • state.platform.get_balance(account.address) restituisce il saldo dell'account
  • state.platform.transactions restituisce l'elenco delle transazioni
  • transaction.return_data sono i dati restituiti
  • m.generate_testcase(state, name) genera input per lo stato

Riepilogo: Ottenere percorsi che generano eccezioni

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# # Verifica se un'esecuzione termina con un REVERT o 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')
Mostra tutto

Tutto il codice sopra lo puoi trovare in example_run.py (opens in a new tab)

Nota che avremmo potuto generare uno script molto più semplice, poiché tutti gli stati restituiti da terminated_state hanno REVERT o INVALID nel loro risultato: questo esempio aveva solo lo scopo di dimostrare come manipolare l'API.

Aggiungere vincoli

Vedremo come vincolare l'esplorazione. Faremo l'ipotesi che la documentazione di f() affermi che la funzione non viene mai chiamata con a == 65, quindi qualsiasi bug con a == 65 non è un vero bug. L'obiettivo è ancora il seguente contratto intelligente 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}

Operatori

Il modulo Operators (opens in a new tab) facilita la manipolazione dei vincoli, tra le altre cose fornisce:

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (maggiore di senza segno),
  • Operators.UGE (maggiore o uguale a senza segno),
  • Operators.ULT (minore di senza segno),
  • Operators.ULE (minore o uguale a senza segno).

Per importare il modulo usa quanto segue:

1from manticore.core.smtlib import Operators

Operators.CONCAT viene usato per concatenare un array a un valore. Ad esempio, il return_data di una transazione deve essere modificato in un valore per essere confrontato con un altro valore:

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

Vincoli

Puoi usare i vincoli a livello globale o per uno stato specifico.

Vincolo globale

Usa m.constrain(constraint) per aggiungere un vincolo globale. Ad esempio, puoi chiamare un contratto da un indirizzo simbolico e vincolare questo indirizzo a valori specifici:

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)

Vincolo di stato

Usa state.constrain(constraint) (opens in a new tab) per aggiungere un vincolo a uno stato specifico. Può essere usato per vincolare lo stato dopo la sua esplorazione per verificare alcune proprietà su di esso.

Verificare i vincoli

Usa solver.check(state.constraints) per sapere se un vincolo è ancora fattibile. Ad esempio, quanto segue vincolerà symbolic_value a essere diverso da 65 e verificherà se lo stato è ancora fattibile:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # lo stato è fattibile

Riepilogo: Aggiungere vincoli

Aggiungendo il vincolo al codice precedente, otteniamo:

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# # Verifica se un'esecuzione termina con un REVERT o INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # non consideriamo il percorso in cui a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
Mostra tutto

Tutto il codice sopra lo puoi trovare in example_run.py (opens in a new tab)

Ultimo aggiornamento della pagina: 26 aprile 2024

nhszn (opens in a new tab)
rex4539r (opens in a new tab)
hursittarcanh (opens in a new tab)
+6

Questo tutorial è stato utile?