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

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

Instalace

Manticore vyžaduje >= Python 3.6. Lze jej nainstalovat přes pip nebo pomocí 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 ze svého hostitelského systému 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í skriptu v Pythonu pomocí Python 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í „programových cest“, reprezentovaných jako matematické vzorce zvané path predicates. Koncepčně tato technika pracuje s predikáty cest ve dvou krocích:

1. Jsou konstruovány pomocí omezení na vstupu programu.
2. Používají se ke generování vstupů programu, které způsobí spuštění přidružených cest.

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

Příklad predikátu cesty

Chcete-li získat představu o tom, jak DSE funguje, zvažte následující příklad:

function f(uint a){

  if (a == 65) {
      // Je přítomna chyba
  }

}

Vzhledem k tomu, že f() obsahuje dvě cesty, DSE zkonstruuje 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 SMT řešiteli (opens in a new tab), jenž se pokusí rovnici vyřešit. Pro Path 1 řešitel řekne, že cestu lze prozkoumat s a = 65. Pro Path 2 může řešitel přiřadit a jakoukoli hodnotu jinou než 65, například a = 0.

Ověřování vlastností

Manticore umožňuje plnou kontrolu nad celým prováděním každé cesty. Díky tomu vám umožňuje přidávat libovolná omezení téměř k čemukoli. Tato kontrola umožňuje vytváření vlastností na kontraktu.

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

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

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í do 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 splnitelný, znamená to, že jste našli přetečení. Řešitel může například vygenerovat vstup a = 10 , b = MAXUINT256.

Pokud zvážíte opravenou verzi:

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

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 tak 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 pomocí Manticore API. Cílem je následující chytrý kontrakt 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();
        }
    }
}

Spuštění samostatného průzkumu

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ů podobný tomuto (pořadí se může změnit):

...
... m.c.manticore:INFO: Vygenerován testovací případ č. 0 - STOP
... m.c.manticore:INFO: Vygenerován testovací případ č. 1 - REVERT
... m.c.manticore:INFO: Vygenerován testovací případ č. 2 - RETURN
... m.c.manticore:INFO: Vygenerován testovací případ č. 3 - REVERT
... m.c.manticore:INFO: Vygenerován testovací případ č. 4 - STOP
... m.c.manticore:INFO: Vygenerován testovací případ č. 5 - REVERT
... m.c.manticore:INFO: Vygenerován testovací případ č. 6 - REVERT
... m.c.manticore:INFO: Výsledky v /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

Bez dalších informací bude Manticore prozkoumávat kontrakt pomocí nových symbolických transakcí, dokud na kontraktu neobjeví nové cesty. Manticore nespouští nové transakce po té, která selhala (např. po zvrácení).

Manticore vypíše informace do adresáře mcore_*. Mimo jiné v tomto adresáři 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í názvů souborů se může změnit):

Shrnutí průzkumu: f(!=65) označuje volání f s jakoukoli hodnotou odlišnou od 65.

Jak si můžete všimnout, Manticore generuje unikátní testovací případ pro každou úspěšnou nebo zvrácenou transakci.

Použijte příznak --quick-mode, pokud chcete rychlý průzkum kódu (zakáže detektory chyb, výpočet gasu atd.).

Manipulace s chytrým kontraktem přes API

Tato část podrobně popisuje, jak manipulovat s chytrým kontraktem prostřednictvím Manticore Python API. 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é spouštět přímo v konzoli Pythonu; pro spuštění konzole použijte příkaz $ python3.

Vytváření účtů

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

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

Kontrakt v Solidity lze nasadit pomocí 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)

Shrnutí

• Uživatelské a kontraktové účty můžete vytvářet 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í:

• Surová transakce (raw transaction): prozkoumají se všechny funkce
• Pojmenovaná transakce (named transaction): prozkoumá se pouze jedna funkce

Surová transakce

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

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

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é pole bajtů.

Například:

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)

Pokud jsou data symbolická, Manticore během provádění transakce prozkoumá všechny funkce kontraktu. 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 Prakticky s 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:

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

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

Shrnutí

• Argumenty transakce mohou být konkrétní nebo symbolické
• Surová transakce prozkoumá všechny funkce
• Funkce lze volat jejich jménem

Pracovní prostor

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

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

Ukončení průzkumu

K zastavení průzkumu použijte m.finalize() (opens in a new tab). Jakmile je tato metoda zavolána, neměly by být odesílány žádné další transakce a Manticore vygeneruje testovací případy pro každou prozkoumanou cestu.

Shrnutí: Spuštění pod Manticore

Spojením všech předchozích kroků dohromady získáme:

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() # zastavit průzkum

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

Získání cest vyvolávajících výjimky

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

Použití informací o stavu

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

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

for state in m.all_states:
    # udělat něco se stavem

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

• state.platform.get_balance(account.address): zůstatek na úč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:

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint", data)

Jak vygenerovat testovací případ

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

m.generate_testcase(state, 'BugFound')

Shrnutí

• Můžete iterovat přes stavy 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 vyvolávající výjimku

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)

## Zkontrolujte, zda provádění končí ZVRÁCENÍM nebo 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')

Veškerý výše uvedený kód najdete 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 průzkum. Budeme předpokládat, že dokumentace f() uvádí, že funkce není nikdy volána 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):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Operátory

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

• Operators.AND,
• Operators.OR,
• Operators.UGT (unsigned greater than - neznaménkové větší než),
• Operators.UGE (unsigned greater than or equal to - neznaménkové větší než nebo rovno),
• Operators.ULT (unsigned lower than - neznaménkové menší než),
• Operators.ULE (unsigned lower than or equal to - neznaménkové menší než nebo rovno).

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

from manticore.core.smtlib import Operators

Operators.CONCAT se používá ke zřetězení pole na hodnotu. Například return_data transakce je třeba změnit na hodnotu, aby ji bylo možné porovnat s jinou hodnotou:

last_return = Operators.CONCAT(256, *last_return)

Omezení

Omezení můžete použít globálně nebo pro konkrétní stav.

Globální omezení

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

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)

Omezení stavu

K přidání omezení pro konkrétní stav použijte state.constrain(constraint) (opens in a new tab). Lze jej použít k omezení stavu po jeho prozkoumání za účelem kontroly nějaké jeho vlastnosti.

Kontrola omezení

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

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # stav je proveditelný

Shrnutí: Přidávání omezení

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

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

## Zkontrolujte, zda provádění končí ZVRÁCENÍM nebo INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # neuvažujeme cestu, kde 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')

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

Poslední aktualizace stránky: 3. dubna 2026

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+6

Zobrazit přispěvatele