Vai al contenuto principale

Aiuta ad aggiornare questa pagina

🌏

C'è una nuova versione di questa pagina, ma al momento è solo in inglese. Aiutaci a tradurre l'ultima versione.

Traduci la pagina
Visualizza in inglese

Nessun bug qui!🐛

Questa pagina non è stata tradotta. Per il momento, è stata intenzionalmente lasciata in inglese.

Come usare Manticore per trovare bug negli Smart Contract

Solidity
Smart Contract
sicurezza
test
verifica formale
Advanced
✍Trailofbits
📚Creare contratti sicuri
📆13 gennaio 2020
⏱️11 minuti letti

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}
8
📋 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, 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}
5
📋 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}
7
📋 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:

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}
10
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...
11
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 dell'account per test case
  • 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):

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) 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, ecc.)

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.

Creazione di account

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

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

Un account senza contratto viene creato usando m.create_account:

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

Un contratto Solidity può essere distribuito usando m.solidity_create_contract:

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)
13
Mostra tutto
📋 Copia

Riepilogo

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:

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

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)
7
📋 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 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)
3
📋 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))
2
📋 Copia

Chiusura dell'esplorazione

Per interrompere l'esplorazione usa m.finalize(). 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
16
Mostra tutto
📋 Copia

Tutto il codice sopra lo puoi trovare in example_run.py

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:

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}
9
📋 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:

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

Puoi accedere alle informazioni sullo stato. Per 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, convertibile in un valore con ABI.deserialize, per esempio:

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

Come generare test case

Usa m.generate_testcase(state, name) per generare test case:

1m.generate_testcase(state, 'BugFound')
2
📋 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')
20
Mostra tutto
📋 Copia

Tutto il codice qui sopra si trova in example_run.py

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:

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

Operatori

Il modulo Operators 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
2
📋 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)
2
📋 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)
7
📋 Copia

Vincolo di stato

Usa state.constrain(constraint) 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
4
📋 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')
31
Mostra tutto
📋 Copia

Tutto il codice sopra si può trovare in example_run.py

Ultima modifica: , Invalid DateTime
Modifica la pagina

Questa pagina è stata utile?