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

solidity

contracte inteligente

securitate

testare

verificare formală

avansat

️Trailofbits

Construirea de contracte sigure

January 13, 2020

5 minute de citit

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}
8
 Copiere

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)

Fiecare operator de cale este o formulă matematică ce poate fi dată unui așa-numit rezolvator SMT, care va încerca să rezolve ecuația. 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}
5
 Copiere

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

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:

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

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: Caz de test generat No. 0 - STOP
3... m.c.manticore:INFO: Caz de test generat No. 1 - REVERT
4... m.c.manticore:INFO: Caz de test generat No. 2 - RETURN
5... m.c.manticore:INFO: Caz de test generat No. 3 - REVERT
6... m.c.manticore:INFO: Caz de test generat No. 4 - STOP
7... m.c.manticore:INFO: Caz de test generat No. 5 - REVERT
8... m.c.manticore:INFO: Caz de test generat No. 6 - REVERT
9... m.c.manticore:INFO: Rezultat in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
11
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ă.

Utilizează indicatorul --quick-mode dacă dorești o explorare rapidă a codului (dezactivează detectoarele de erori, 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()
4
 Copiere

Un cont non-contract este creat utilizând m.create_account:

1user_account = m.create_account(balance=1000)
2
 Copiere

Un contract Solidity poate fi implementat utilizând 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# inițiază contractul
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
Afișează tot
 Copiere

Rezumat

• Poți crea conturi de utilizator și contracte cu m.create_account și [m.solidity_create_contract](https://manticore.readthedocs.io/en/latest/api.html#manticore.ethereum.ManticoreEVM.solidity_create_contract.

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ă

O tranzacție brută este executată utilizând m.transaction:

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

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

• m.make_symbolic_value creează o valoare simbolică.
• m.make_symbolic_buffer(size) creează o matrice simbolică de byți.

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)
7
 Copiere

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 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)
3
 Copiere

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("Rezultatele sunt în {}".format(m.workspace))
2
 Copiere

Terminarea explorării

Pentru a opri utilizarea explorării folosește m.finalize(). 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
16
Afișează tot
 Copiere

Tot codul de mai sus îl poți găsi în example_run.py

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:

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
 Copiere

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: Lista stărilor care sunt pregătite (acestea nu au executat REVERT/INVALID)
• m.killed_states: Lista stărilor care sunt pregătite (acestea nu au executat REVERT/INVALID)
• m.all_states: toate stările

1for state in m.all_states:
2    # fă ceva cu starea
3
 Copiere

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)
3
 Copiere

Cum să generezi un caz de test

Utilizează m.generate_testcase(state, name) pentru a genera un caz de test:

1m.generate_testcase(state, 'BugFound')
2
 Copiere

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## Verifică dacă o execuție se încheie cu un a REVERT sau INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Aruncare găsită {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
20
Afișează tot
 Copiere

Tot codul de mai sus îl poți găsi în example_run.py

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:

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
 Copiere

Operatori

Modulul Operatori 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
2
 Copiere

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)
2
 Copiere

Restricții

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

Restricție globală

Folosește m.constrain(constraint) pentru a adăuga o restricție globală. 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)
7
 Copiere

Restricție de stare

Utilizează state.constrain(constraint) pentru a adăuga o restricție unei anumită stări Aceasta poate fi folosită pentru a restrânge starea ca după explorare să verifice unele proprietăți pe ea.

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ă
4
 Copiere

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## Verifică dacă o execuție se încheie cu un REVERT sau INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # nu considerăm calea unde a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Eroare găsită, rezultatele sunt în {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'Nicio eroare')
31
Afișează tot
 Copiere

Tot codul de mai sus îl poți găsi în example_run.py

Ultima editare: , Invalid DateTime

Vezi colaboratorii

Edit page