Come usare Manticore per trovare bug negli Smart Contract

L'obiettivo di questo tutorial è mostrare come usare Manticore per trovare automaticamente bug negli Smart Contract.

Installazione

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

Manticore con 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 avente accesso alla tua directory corrente. Puoi cambiare i file dal tuo host ed eseguire gli strumenti sui file dal docker

In docker, esegui:

solc-select 0.5.11
cd /home/trufflecon/

Manticore con pip

pip3 install --user manticore

È consigliato solc 0.5.11.

Esecuzione di uno script

Per eseguire uno script Python con Python 3:

python3 script.py

Introduzione all'esecuzione simbolica dinamica

Esecuzione simbolica dinamica in pillole

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

1. Vengono costruiti usando vincoli nell'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. Per esempio, se le analisi trova un overflow di valori interi, è garantito che sia riproducibile.

Esempio di predicato di percorso

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

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

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 passata a un cosiddetto risolutore SMT(opens in a new tab), che proverà a 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ò assegnare ad a tutti i valori diversi da 65, per esempio a = 0.

Verifica delle proprietà

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

Considera l'esempio seguente:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // no overflow protection
3  return c;
4}
 Copia

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

• Percorso 1: c = a + b

Usando Manticore, si può 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 qui sopra sia fattibile, significa che è stato trovato un overflow. Ad esempio, il risolutore può generare l'input a = 10 , b = MAXUINT256.

Se consideri una versione fissa:

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

La formula associata al controllo dell'overflow sarebbe:

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

Questa formula non è risolvibile; in altri mondi questa è una prova che in safe_add, c aumenterà sempre.

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

Esecuzione in Manticore

Vedremo come esplorare uno Smart Contract con l'API Manticore. La destinazione è il seguente Smart Contract 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
 Copia

Esplorazione indipendente

Manticore può essere eseguito direttamente sullo Smart Contract con il comando seguente (project può essere un file Solidity o una directory del progetto):

$ manticore project

Otterrai l'output dei casi di prova, come il seguente (l'ordine potrebbe variare):

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 Contract Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Mostra tutto

Senza altre informazioni, Manticore esplorerà il contratto con nuove transazioni simboliche, finché non esplorerà nuovi percorsi sul contratto. Manticore non esegue nuove transazioni se una non riesce (ad esempio dopo un ripristino).

Manticore restituirà le informazioni un una directory mcore_*. In questa directory troverai, tra altre cose:

• global.summary: copertura e avvisi del compilatore
• test_XXXXX.summary: copertura, ultima istruzione, saldi del conto per casi di prova
• test_XXXXX.tx: elenco dettagliato delle transazioni per test case

Qui Manticore trova 7 test case che corrispondono a (l'ordine dei nomi dei file potrebbe variare):

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

Come puoi notare, Manticore genera un test case univoco per ogni transazione riuscita o ripristinata.

Usa il flag --quick-mode se desideri un'esplorazione veloce del codice (disabilita rilevatori di bug, calcolo del carburante, etc.)

Manipolazione di uno Smart Contract tramite l'API

Questa sezione contiene informazioni su come manipolare uno Smart Contract tramite l'API Python di Manticore. Puoi creare un nuovo file con l'estensione di Python *.py e scrivere il codice necessario aggiungendo i comandi dell'API (le basi saranno descritte di seguito) in questo file e poi eseguirlo con il comando $ python3 *.py. Puoi anche eseguire i comandi qui sotto direttamente nella console Python. Per eseguirla usa il comando $ python3.

Creare i Conti

La prima da fare è inizializzare una nuova blockchain con i comandi seguenti:

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

Un conto privo di contratto è creato usando m.create_account(opens in a new tab):

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

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# Inizializza il contratto
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Mostra tutto
 Copia

Riepilogo

• Puoi creare conti dell'utente e del contratto con m.create_account(opens in a new tab) e m.solidity_create_contract(opens in a new tab).

Esecuzione di transazioni

Manticore supporta due tipi di transazione:

• Transazione grezza: vengono esplorate tutte le funzioni
• Transazione con nome: 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)
 Copia

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

• m.make_symbolic_value(opens in a new tab) crea un valore simbolico.
• m.make_symbolic_buffer(size)(opens in a new tab) crea un array di byte 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)
 Copia

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

Transazione con nome

Le funzioni sono eseguibili 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)
 Copia

Se value della transazione non è specificato, è 0 di default.

Riepilogo

• Gli argomenti di una transazione possono essere concreti o simbolici
• Una transazione grezza esplorerà tutte le funzioni
• La funzione può essere chiamata con il suo nome

Area di lavoro

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

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

Chiusura dell'esplorazione

Per interrompere l'esplorazione usa m.finalize()(opens in a new tab). Nessun'altra transazione dovrebbe essere inviata una volta chiamato questo metodo e dopo che Manticore ha generato test case per ognuno 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() # stop the exploration
Mostra tutto
 Copia

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

Ottenere i percorsi che generano eccezioni

Ora creeremo input specifici per i percorsi che generano un'eccezione in f(). La destinazione è ancora il seguente Smart Contract 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}
 Copia

Uso delle informazioni di stato

Ogni percorso eseguito ha il proprio stato della blockchain. Uno stato è pronto o terminato, a significare che ha raggiunto un'istruzione THROW o REVERT:

• m.ready_states(opens in a new tab): l'elenco degli stati pronti (cioè che non hanno eseguito un REVERT/INVALID)
• m.killed_states(opens in a new tab): l'elenco degli stati terminati
• m.all_states(opens in a new tab): tutti gli stati

1for state in m.all_states:
2    # esegue un'operazione con lo stato
 Copia

Puoi accedere alle informazioni sullo stato. Per esempio:

• state.platform.get_balance(account.address): il saldo del conto
• 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, convertibile in un valore con ABI.deserialize, per esempio:

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

Come generare test case

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

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

Riepilogo

• Puoi eseguire iterazioni sullo stato con m.all_states
• state.platform.get_balance(account.address) restituisce il saldo del conto
• 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 il percorso che genera 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## Controlla se l'esecuzione termina con 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
 Copia

Tutto il codice qui sopra si trova in example_run.py(opens in a new tab)

Nota: avremmo potuto generare uno script molto più semplice poiché tutti gli stati restituiti da terminated_state hanno REVERT o INVALID nel risultato. Questo esempio era inteso solo per dimostrare come manipolare l'API.

Aggiunta di vincoli

Vediamo ora come vincolare l'esplorazione. Presumiamo che la documentazione di f() indichi che la funzione non viene mai chiamata con a == 65, quindi ogni bug con a == 65 non è un vero bug. La destinazione è ancora il seguente Smart Contract 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}
 Copia

Operatori

Il modulo Operators(opens in a new tab) facilita la manipolazione dei vincoli, fornendo tra l'altro:

• 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:

1from manticore.core.smtlib import Operators
 Copia

Operators.CONCAT è usato per concatenare un array a un valore. Per esempio, return_data di una transazione deve essere modificato in valore per poter essere verificato a fronte di un altro valore:

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

Vincoli

Puoi usare vincoli globalmente o per uno stato specifico.

Vincolo globale

Usa m.constrain(constraint) per aggiungere un vincolo globale. Per esempio, puoi chiamare un contratto da un indirizzo simbolico e limitare quest'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)
 Copia

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 verificarvi della proprietà.

Controllo di un vincolo

Usa solver.check(state.constraints) per sapere se un vincolo è ancora fattibile. Per esempio, il codice seguente vincola symbolic_value ad essere diverso da 65 e controlla se lo stato è ancora fattibile:

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

Riepilogo: aggiunta di 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## Controlla se l'esecuzione termina con 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        # we do not consider the path were 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
 Copia

Tutto il codice sopra si può trovare in example_run.py(opens in a new tab)