Come usare Manticore per trovare bug negli smart contract

Lo scopo 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 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 container Docker che ha accesso alla tua directory corrente. Puoi modificare i file dal tuo host ed eseguire gli strumenti sui file dal container 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 di stato con un alto grado di consapevolezza semantica. Questa tecnica si basa sulla scoperta di "percorsi di programma", rappresentati come formule matematiche chiamate path predicates. 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:

function f(uint a){

  if (a == 65) {
      // È presente un bug
  }

}

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 cercherà di risolvere l'equazione. Per Path 1, il risolutore dirà che il percorso può essere esplorato con a = 65. Per Path 2, il risolutore può assegnare a a qualsiasi valore diverso da 65, ad esempio a = 0.

Verifica delle 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:

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // nessuna protezione contro l'overflow
  return c;
}

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

• Percorso 1: c = a + b

Usando Manticore, puoi verificare la presenza di 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:

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

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 uno smart contract con l'API di Manticore. L'obiettivo è il seguente smart contract 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();
        }
    }
}

Eseguire un'esplorazione autonoma

Puoi eseguire Manticore direttamente sullo smart contract 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):

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

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, in questa directory troverai:

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

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 andata a buon fine o che ha subito un revert.

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

Manipolare uno smart contract tramite l'API

Questa sezione descrive in dettaglio come manipolare uno smart contract 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, per 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.

Creazione di account

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

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

Un contratto Solidity può essere distribuito usando 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)

Riepilogo

• Puoi creare account utente e account di 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 (raw): vengono esplorate tutte le funzioni
• Transazione nominata (named): viene esplorata solo una funzione

Transazione grezza

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

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

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 simbolico.

Ad esempio:

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)

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

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:

symbolic_var = m.make_symbolic_value()
contract_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 esplorerà 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:

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

Terminare l'esplorazione

Per interrompere l'esplorazione usa m.finalize() (opens in a new tab). Non dovrebbero essere inviate ulteriori transazioni 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:

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

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

Ottenere i percorsi che generano eccezioni

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

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:

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

for state in m.all_states:
    # fai 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:

data = state.platform.transactions[0].return_data
data = 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:

m.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 i percorsi che generano eccezioni

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)

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

Tutto il codice sopra riportato si trova 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. Supporremo 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 smart contract 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();
        }
    }
}

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:

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

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

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)

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.

Verifica dei 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:

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

Riepilogo: Aggiungere vincoli

Aggiungendo il vincolo al codice precedente, otteniamo:

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

## Controlla se un'esecuzione termina con un REVERT o INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # non consideriamo il percorso in cui 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')

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