Cum se folosește Manticore pentru a găsi erori în contractele inteligente

Scopul acestui tutorial este de a arăta cum să utilizezi Manticore pentru a găsi automat erori în contractele inteligente.

Instalare

Manticore necesită >= python 3.6. Poate fi instalat prin pip sau folosind docker.

Manticore prin docker

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

Ultima comandă rulează „eth-security-toolbox” într-un docker, care are acces la directorul curent. Poți schimba fișierele de la gazda ta și poți rula instrumentele de pe fișierele din docker

În docker, rulează:

solc-select 0.5.11
cd /home/trufflecon/

Manticore prin pip

pip3 install --user manticore

solc 0.5.11 este recomandat.

Rularea unui script

Pentru a rula un script python cu python 3:

python3 script.py

Introducere în execuția simbolică dinamică

Execuția simbolică dinamică pe scurt

Execuția simbolică dinamică (DSE) este o tehnică de analiză a programului care explorează un spațiu de stare cu un grad ridicat de conștientizare semantică. Această tehnică se bazează pe descoperirea „căii programului”, reprezentată ca o formulă matematică numită path predicate (operator de cale). Conceptual, această tehnică funcționează pe operatori de cale în doi pași:

1. Aceștia sunt construiți folosind restricții la intrarea programului.
2. Ei sunt folosiți pentru a genera intrări de program care vor determina executarea căilor asociate.

Această abordare nu produce falsuri pozitive în sensul că toate stările identificate ale programului pot fi declanșate în timpul execuției concrete. De exemplu, dacă analiza găsește o depășire de întreg, este garantat se poate reproduce.

Exemplu de operatori de cale

Pentru a avea o perspectivă despre cum funcționează DSE, ia în considerare următorul exemplu:

1function f(uint a){
2
3  if (a == 65) {
4      // A apărut o eroare
5  }
6
7}
 Copiați

Deoarece f() conține două căi, un DSE va construi doi operatori de cale diferiți:

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

Each path predicate is a mathematical formula that can be given to a so-called SMT solver(opens in a new tab), which will try to solve the equation. Pentru Path 1, rezolvatorul va spune că această cale poate fi explorată cu a = 65. Pentru Path 2, rezolvatorul îi poate da lui a orice altă valoare diferită de 65, de exemplu a = 0.

Verificarea proprietăților

Manticore permite un control complet asupra întregii execuții a fiecărei căi. Ca rezultat, permite adăugarea de restricții arbitrare la aproape orice. Acest control permite crearea de proprietăți în contract.

Să considerăm următorul exemplu:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // fără protecție de overflow
3  return c;
4}
 Copiați

Aici există o singură cale de explorat în funcție:

• Calea 1: c = a + b

Folosind Manticore, poți verifica dacă există depășiri și poți adăuga constrângeri la operatorii căii:

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

Dacă se poate găsi o evaluare lui a și lui b pentru care operatorul de cale de mai sus este fezabil, înseamnă că ai găsit o depășire. De exemplu, rezolvatorul poate genera intrarea a = 10, b = MAXUINT256.

Dacă iei în considerare o versiune fixă:

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ți

Formula asociată cu verificarea pentru depășire va fi:

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

Această formulă nu poate fi rezolvată; într-o lume imaginară, aceasta ar fi o dovadă că în safe_add, c va crește întotdeauna.

DSE este, prin urmare, un instrument puternic, care poate să verifice constrângeri arbitrare în codul tău.

Rularea sub Manticore

Vom vedea cum să explorăm un contract inteligent cu API-ul Manticore. Obiectivul este următorul contract inteligent 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}
Afișează tot
 Copiați

Rulează o explorare independentă

Poți rula Manticore direct pe contractul inteligent prin următoarea comandă (project poate fi un fișier Solidity sau un director de proiect):

$ manticore project

Vei obține ieșirea unor cazuri de testare, cum ar fi acestea (ordinea se poate schimba):

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...
Afișează tot

Fără informații suplimentare, Manticore va explora contractul cu noi tranzacții simbolice până când nu explorează noi căi în contract. Manticore nu execută tranzacții noi după o eroare (de exemplu: după o revenire).

Manticore va afișa informațiile într-un director mcore_*. Printre altele, vei găsi în acest director:

• global.summary: acoperire și avertismente ale compilatorului
• test_XXXXX.summary: acoperire, ultima instrucțiune, solduri de cont pe caz de testare
• test_XXXXX.tx: lista detaliată a tranzacțiilor pe caz de testare

Aici Manticore găsește 7 cazuri de testare, care corespund (ordinea numelui fișierului se poate modifica):

Rezumatul explorării f (! = 65) reprezintă f apelat cu orice valoare diferită de 65.

După cum poți observa, Manticore generează un caz de test unic pentru fiecare tranzacție reușită sau revenită.

Utilizați flagul --quick-mode dacă doriți o explorare rapidă a codului (dezactivează detectoarele de bug-uri, calculul gazului, ...)

Manipulează un contract inteligent prin API

Această secțiune descrie în detaliu modul de manipulare a unui contract inteligent cu API-ului Manticore Python. Poți crea un fișier nou cu extensia python *.py și scrie codul necesar adăugând comenzile API (ale căror elemente de bază vor fi descrise mai jos) în acest fișier și apoi îl poți rula cu comanda $ python3 *.py . De asemenea, poți executa comenzile de mai jos direct în consola python; pentru a rula consola utilizează comanda $ python3.

Crearea conturilor

Primul lucru care trebuie făcut este să inițiezi un nou blockchain cu următoarele comenzi:

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

A non-contract account is created using m.create_account(opens in a new tab):

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

A Solidity contract can be deployed using 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# inițiază contractul
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Afișează tot
 Copiați

Rezumat

• You can create user and contract accounts with m.create_account(opens in a new tab) and m.solidity_create_contract(opens in a new tab).

Executarea tranzacțiilor

Manticore acceptă două tipuri de tranzacții:

• Tranzacția brută: explorează toate funcțiile
• Tranzacția denumită: explorează o singură funcție

Tranzacția brută

A raw transaction is executed using m.transaction(opens in a new tab):

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

Apelantul, adresa, datele sau valoarea tranzacției pot să fie concrete sau simbolice:

• m.make_symbolic_value(opens in a new tab) creates a symbolic value.
• m.make_symbolic_buffer(size)(opens in a new tab) creates a symbolic byte array.

De exemplu:

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ți

Dacă datele sunt simbolice, Manticore va explora toate funcțiile contractului în timpul executării tranzacției. Va fi util să vezi explicația funcției Fallback în articolul Hands on the Ethernaut CTF(opens in a new tab) pentru a înțelege cum funcționează selecția funcțiilor.

Tranzacția denumită

Funcțiile pot fi executate prin numele lor. Pentru a executa f(uint var) cu o valoare simbolică, din contul utilizatorului și cu 0 eter, utilizează:

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

Dacă argumentul valoare al tranzacției nu este specificată, este 0 în mod implicit.

Rezumat

• Argumentele unei tranzacții pot fi concrete sau simbolice
• O tranzacție brută va explora toate funcțiile
• Funcția poate fi apelată după numele ei

Spațiu de lucru

m.workspace este directorul folosit ca director de ieșire pentru toate fișierele generate:

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

Terminarea explorării

To stop the exploration use m.finalize()(opens in a new tab). Nu trebuie trimise alte tranzacții odată ce această metodă este apelată și Manticore generează cazuri de testare pentru fiecare cale explorată.

Rezumat: Rularea sub Manticore

Punând împreună toți pașii anteriori, obținem:

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("Rezultatele sunt în {}".format(m.workspace))
15m.finalize() # oprește explorarea
Afișează tot
 Copiați

Tot codul de mai sus îl poți găsi în example_run.py(opens in a new tab)

Obținerea căilor de aruncare

Acum vom genera intrări specifice pentru căile care ridică o excepție în f(). Obiectivul este în continuare următorul contract inteligent 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ți

Utilizarea informațiilor de stare

Fiecare cale executată are starea sa de blockchain. O stare este fie pregătită, fie ucisă, ceea ce înseamnă că ajunge la instrucțiunea THROW sau REVERT:

• m.ready_states(opens in a new tab): Lista stărilor care sunt pregătite (acestea nu au executat REVERT/INVALID)
• m.killed_states(opens in a new tab): lista stărilor care sunt ucise
• m.all_states(opens in a new tab): toate stările

1for state in m.all_states:
2    # fă ceva cu starea
 Copiați

Poți accesa informațiile despre stare. De exemplu:

• state.platform.get_balance(account.address): soldul contului
• state.platform.transactions: lista tranzacțiilor
• state.platform.transactions[-1].return_data: datele returnate de ultima tranzacție

Datele returnate de ultima tranzacție sunt o matrice, care poate fi convertită într-o valoare cu „ABI.deserialize”, de exemplu:

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

Cum să generezi un caz de test

Use m.generate_testcase(state, name)(opens in a new tab) to generate testcase:

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

Rezumat

• Poți itera starea cu m.all_states
• state.platform.get_balance(account.address) returnează soldul contului
• state.platform.transactions returnează lista tranzacțiilor
• transaction.return_data sunt datele returnate
• m.generate_testcase(state, name) generează intrări pentru stare

Rezumat: Obținerea căilor de aruncare

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## Check if an execution ends with a REVERT or 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')
Afișează tot
 Copiați

Tot codul de mai sus îl poți găsi în example_run.py(opens in a new tab)

Notează că am fi putut genera un script mult mai simplu, ca toate stările returnate de terminat_state având REVERT sau INVALID în rezultatul lor: Acest exemplu a fost menit doar să demonstreze modul de manipulare API.

Adăugarea de restricții

Vom vedea cum să constrângem explorarea. Vom face presupunerea că documentația din f() afirmă că funcția nu este apelată niciodată cu a == 65, deci orice eroare cu a == 65 nu este o eroarea adevărată. Obiectivul este în continuare următorul contract inteligent 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ți

Operatori

Modulul Operatori(opens in a new tab) facilitează manipularea restricțiilor, printre altele oferind:

• Operators.AND,
• Operators.OR,
• Operators.UGT (nesemnat mai mare de),
• Operators.UGE (nesemnat mai mare sau egal cu),
• Operators.ULT (nesemnat mai mic de),
• Operators.ULE (nesemnat mai mic sau egal cu).

Pentru a importa modulul, utilizează următoarele:

1from manticore.core.smtlib import Operators
 Copiați

Operators.CONCAT este utilizat pentru a concatena o matrice la o valoare. De exemplu, return_data ale unei tranzacții trebuie să fie modificate la o valoare care trebuie verificată cu o altă valoare:

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

Restricții

Poți utiliza constrângeri la nivel global sau pentru o anumită stare.

Restricție globală

Use m.constrain(constraint) to add a global constraint. De exemplu, poți apela un contract de la o adresă simbolică și împiedica această adresă să aibă o valoare specifică:

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ți

Restricție de stare

Use state.constrain(constraint)(opens in a new tab) to add a constraint to a specific state It can be used to constrain the state after its exploration to check some property on it.

Verificarea restricțiilor

Utilizează solver.check(state.constraints) pentru a afla dacă o restricție este încă fezabilă. De exemplu, următoarele vor restrânge „symbolic_value” să fie diferite de 65 și să verifice dacă starea este încă fezabilă:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # starea este fezabilă
 Copiați

Sumar: Adăugarea restricțiilor

Adăugând restricții codului anterior, obținem:

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## Check if an execution ends with a REVERT or 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')
Afișează tot
 Copiați

Tot codul de mai sus îl poți găsi în example_run.py(opens in a new tab)