Jak používat Manticore k vyhledávání chyb v chytrých kontraktech

Cílem tohoto tutoriálu je ukázat, jak používat Manticore k automatickému vyhledávání chyb v chytrých kontraktech.

Instalace

Manticore vyžaduje python >= 3.6. Lze jej nainstalovat pomocí pip nebo s použitím dockeru.

Manticore přes docker

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

Poslední příkaz spustí eth-security-toolbox v dockeru, který má přístup k vašemu aktuálnímu adresáři. Můžete měnit soubory z vašeho hostitele a spouštět nástroje na souborech z dockeru

Uvnitř dockeru spusťte:

solc-select 0.5.11
cd /home/trufflecon/

Manticore přes pip

pip3 install --user manticore

Doporučuje se solc 0.5.11.

Spuštění skriptu

Pro spuštění pythonového skriptu v pythonu 3:

python3 script.py

Úvod do dynamického symbolického provádění

Dynamické symbolické provádění v kostce

Dynamické symbolické provádění (DSE) je technika analýzy programů, která prozkoumává stavový prostor s vysokou mírou sémantického povědomí. Tato technika je založena na objevování „cest programu“, které jsou reprezentovány jako matematické vzorce zvané path predicates. Koncepčně tato technika pracuje s predikáty cest ve dvou krocích:

1. Jsou vytvořeny pomocí omezení na vstupu programu.
2. Používají se ke generování vstupů programu, které způsobí provedení příslušných cest.

Tento přístup neprodukuje žádné falešně pozitivní výsledky v tom smyslu, že všechny identifikované stavy programu mohou být spuštěny během konkrétního provádění. Pokud například analýza najde celočíselné přetečení, je zaručeno, že bude reprodukovatelné.

Příklad predikátu cesty

Pro lepší představu o tom, jak DSE funguje, zvažte následující příklad:

1function f(uint a){
2
3  if (a == 65) {
4      // Je přítomna chyba
5  }
6
7}
Kopírovat

Protože f() obsahuje dvě cesty, DSE vytvoří dva různé predikáty cest:

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

Každý predikát cesty je matematický vzorec, který lze předat takzvanému řešiči SMT (opens in a new tab), který se pokusí rovnici vyřešit. Pro Cestu 1 řešič řekne, že cestu lze prozkoumat s a = 65. Pro Cestu 2 může řešič dát a jakoukoli jinou hodnotu než 65, například a = 0.

Ověřování vlastností

Manticore umožňuje plnou kontrolu nad veškerým prováděním každé cesty. V důsledku toho vám umožňuje přidat libovolná omezení téměř k čemukoli. Tato kontrola umožňuje vytváření vlastností kontraktu.

Zvažte následující příklad:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // žádná ochrana proti přetečení
3  return c;
4}
Kopírovat

Zde je ve funkci k prozkoumání pouze jedna cesta:

• Cesta 1: c = a + b

Pomocí Manticore můžete zkontrolovat přetečení a přidat omezení k predikátu cesty:

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

Pokud je možné najít ohodnocení a a b, pro které je výše uvedený predikát cesty proveditelný, znamená to, že jste našli přetečení. Řešič může například vygenerovat vstup a = 10, b = MAXUINT256.

Pokud zvážíte opravenou verzi:

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}
Kopírovat

Přidružený vzorec s kontrolou přetečení by byl:

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

Tento vzorec nelze vyřešit; jinými slovy, je to důkaz, že v safe_add se c vždy zvýší.

DSE je proto mocný nástroj, který dokáže ověřit libovolná omezení ve vašem kódu.

Spuštění pod Manticore

Podíváme se, jak prozkoumat chytrý kontrakt s Manticore API. Cílem je následující chytrý kontrakt 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}
Zobrazit vše
Kopírovat

Spustit samostatné prozkoumávání

Manticore můžete spustit přímo na chytrém kontraktu pomocí následujícího příkazu (project může být soubor Solidity nebo adresář projektu):

$ manticore project

Získáte výstup testovacích případů, jako je tento (pořadí se může změnit):

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...
Zobrazit vše

Bez dalších informací bude Manticore prozkoumávat kontrakt s novými symbolickými transakcemi, dokud neprozkoumá nové cesty v kontraktu. Manticore nespouští nové transakce po neúspěšné (např. po revertu).

Manticore vypíše informace do adresáře mcore_*. V tomto adresáři mimo jiné najdete:

• global.summary: pokrytí a varování kompilátoru
• test_XXXXX.summary: pokrytí, poslední instrukce, zůstatky na účtech pro každý testovací případ
• test_XXXXX.tx: podrobný seznam transakcí pro každý testovací případ

Zde Manticore našel 7 testovacích případů, které odpovídají (pořadí souborů se může změnit):

Shrnutí prozkoumávání f(!=65) označuje volání f s jakoukoliv hodnotou jinou než 65.

Jak si můžete všimnout, Manticore generuje jedinečný testovací případ pro každou úspěšnou nebo vrácenou transakci.

Použijte příznak --quick-mode, pokud chcete rychlé prozkoumání kódu (vypíná detektory chyb, výpočet gasu atd.)

Manipulace s chytrým kontraktem přes API

Tato část popisuje podrobnosti o tom, jak manipulovat s chytrým kontraktem prostřednictvím Python API Manticore. Můžete vytvořit nový soubor s příponou pythonu *.py a napsat potřebný kód přidáním příkazů API (jejichž základy budou popsány níže) do tohoto souboru a poté jej spustit příkazem $ python3 *.py. Níže uvedené příkazy můžete také provést přímo v konzoli pythonu. Konzoli spustíte příkazem $ python3.

Vytváření účtů

První věc, kterou byste měli udělat, je inicializovat nový blockchain pomocí následujících příkazů:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Kopírovat

Účet, který není kontraktem, se vytváří pomocí m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)
Kopírovat

Kontrakt v Solidity lze nasadit pomocí 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# Inicializace kontraktu
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Zobrazit vše
Kopírovat

Shrnutí

• Uživatelské účty a účty kontraktů můžete vytvořit pomocí m.create_account (opens in a new tab) a m.solidity_create_contract (opens in a new tab).

Provádění transakcí

Manticore podporuje dva typy transakcí:

• Nezpracovaná transakce: prozkoumány jsou všechny funkce
• Pojmenovaná transakce: je prozkoumána pouze jedna funkce

Nezpracovaná transakce

Nezpracovaná transakce se provádí pomocí m.transaction (opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Kopírovat

Volající, adresa, data nebo hodnota transakce mohou být buď konkrétní, nebo symbolické:

• m.make_symbolic_value (opens in a new tab) vytvoří symbolickou hodnotu.
• m.make_symbolic_buffer(size) (opens in a new tab) vytvoří symbolické bajtové pole.

Například:

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)
Kopírovat

Pokud jsou data symbolická, Manticore prozkoumá všechny funkce kontraktu během provádění transakce. Pro pochopení toho, jak funguje výběr funkcí, bude užitečné podívat se na vysvětlení záložní funkce v článku Hands on the Ethernaut CTF (opens in a new tab).

Pojmenovaná transakce

Funkce lze spouštět prostřednictvím jejich názvu. Pro spuštění f(uint var) se symbolickou hodnotou z user_account a s 0 ethery použijte:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
Kopírovat

Pokud není hodnota transakce specifikována, je ve výchozím nastavení 0.

Shrnutí

• Argumenty transakce mohou být konkrétní nebo symbolické
• Nezpracovaná transakce prozkoumá všechny funkce
• Funkci lze volat podle jejího jména

Pracovní prostor

m.workspace je adresář používaný jako výstupní adresář pro všechny generované soubory:

1print("Výsledky jsou v {}".format(m.workspace))
Kopírovat

Ukončení prozkoumávání

Pro zastavení prozkoumávání použijte m.finalize() (opens in a new tab). Po zavolání této metody by se neměly odesílat žádné další transakce a Manticore vygeneruje testovací případy pro každou prozkoumanou cestu.

Shrnutí: Spuštění pod Manticore

Když spojíme všechny předchozí kroky, získáme:

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("Výsledky jsou v {}".format(m.workspace))
15m.finalize() # zastavení prozkoumávání
Zobrazit vše
Kopírovat

Veškerý výše uvedený kód najdete v example_run.py (opens in a new tab)

Získání cest s výjimkami

Nyní vygenerujeme specifické vstupy pro cesty, které vyvolávají výjimku v f(). Cílem je stále následující chytrý kontrakt 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}
Kopírovat

Použití informací o stavu

Každá provedená cesta má svůj stav blockchainu. Stav je buď připraven, nebo je ukončen, což znamená, že dosáhne instrukce THROW nebo REVERT:

• m.ready_states (opens in a new tab): seznam stavů, které jsou připraveny (neprovedly REVERT/INVALID)
• m.killed_states (opens in a new tab): seznam stavů, které jsou ukončeny
• m.all_states (opens in a new tab): všechny stavy

1for state in m.all_states:
2    # udělat něco se stavem
Kopírovat

Můžete přistupovat k informacím o stavu. Například:

• state.platform.get_balance(account.address): zůstatek účtu
• state.platform.transactions: seznam transakcí
• state.platform.transactions[-1].return_data: data vrácená poslední transakcí

Data vrácená poslední transakcí jsou pole, které lze převést na hodnotu pomocí ABI.deserialize, například:

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

Jak generovat testovací případ

Pro generování testovacího případu použijte m.generate_testcase(state, name) (opens in a new tab):

1m.generate_testcase(state, 'BugFound')
Kopírovat

Shrnutí

• Stav můžete iterovat pomocí m.all_states
• state.platform.get_balance(account.address) vrací zůstatek účtu
• state.platform.transactions vrací seznam transakcí
• transaction.return_data jsou vrácená data
• m.generate_testcase(state, name) generuje vstupy pro daný stav

Shrnutí: Získání cesty s výjimkou

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## Zkontrolujte, zda provádění končí s REVERT nebo INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Nalezena výjimka {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Zobrazit vše
Kopírovat

Veškerý výše uvedený kód naleznete v example_run.py (opens in a new tab)

Poznámka: mohli jsme vygenerovat mnohem jednodušší skript, protože všechny stavy vrácené terminated_state mají ve svém výsledku REVERT nebo INVALID: tento příklad měl pouze demonstrovat, jak manipulovat s API.

Přidávání omezení

Podíváme se, jak omezit prozkoumávání. Budeme vycházet z předpokladu, že dokumentace funkce f() uvádí, že funkce se nikdy nevolá s a == 65, takže jakákoli chyba s a == 65 není skutečnou chybou. Cílem je stále následující chytrý kontrakt 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}
Kopírovat

Operátory

Modul Operators (opens in a new tab) usnadňuje manipulaci s omezeními, mimo jiné poskytuje:

• Operators.AND,
• Operators.OR,
• Operators.UGT (větší než bez znaménka),
• Operators.UGE (větší nebo rovno bez znaménka),
• Operators.ULT (menší než bez znaménka),
• Operators.ULE (menší nebo rovno bez znaménka).

Pro import modulu použijte následující příkaz:

1from manticore.core.smtlib import Operators
Kopírovat

Operators.CONCAT se používá ke zřetězení pole na hodnotu. Například return_data transakce musí být změněna na hodnotu, která se má porovnat s jinou hodnotou:

1last_return = Operators.CONCAT(256, *last_return)
Kopírovat

Omezení

Omezení můžete použít globálně nebo pro určitý stav.

Globální omezení

Použijte m.constrain(constraint) pro přidání globálního omezení. Můžete například zavolat kontrakt ze symbolické adresy a omezit tuto adresu na konkrétní hodnoty:

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)
Kopírovat

Omezení stavu

Použijte state.constrain(constraint) (opens in a new tab) k přidání omezení ke konkrétnímu stavu. Lze jej použít k omezení stavu po jeho prozkoumání a ke kontrole nějaké jeho vlastnosti.

Kontrola omezení

Použijte solver.check(state.constraints), abyste zjistili, zda je omezení stále proveditelné. Následující příklad například omezí symbolic_value tak, aby se lišila od 65, a zkontroluje, zda je stav stále proveditelný:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # stav je proveditelný
Kopírovat

Shrnutí: Přidání omezení

Přidáním omezení k předchozímu kódu získáme:

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## Zkontrolujte, zda provádění končí s REVERT nebo INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # nebereme v úvahu cestu, kde a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Byla nalezena chyba, výsledky jsou v {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Nebyla nalezena žádná chyba')
Zobrazit vše
Kopírovat

Veškerý výše uvedený kód naleznete v example_run.py (opens in a new tab)

Stránka naposledy aktualizována: 26. dubna 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Zobrazit přispěvatele