Jak korzystać z Manticore, aby znaleźć błędy w inteligentnych kontraktach

Celem tego samouczka jest pokazanie, jak używać Manticore do automatycznego wyszukiwania błędów w inteligentnych kontraktach.

Instalacja

Manticore wymaga Pythona >= 3.6. Można go zainstalować za pomocą pip lub dockera.

Manticore przez docker

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

Ostatnie polecenie uruchamia eth-security-toolbox w dockerze, który ma dostęp do bieżącego katalogu. Możesz zmienić pliki z hosta i uruchomić narzędzia na plikach z dockera

Wewnątrz dockera uruchom:

solc-select 0.5.11
cd /home/trufflecon/

Manticore przez pip

pip3 install --user manticore

Zalecany jest solc w wersji 0.5.11.

Uruchamianie skryptu

Aby uruchomić skrypt Pythona za pomocą Pythona 3:

python3 script.py

Wprowadzenie do dynamicznej egzekucji symbolicznej

Dynamiczna egzekucja symboliczna w pigułce

Dynamiczna egzekucja symboliczna (DSE) to technika analizy programu, która bada przestrzeń stanów z wysokim stopniem świadomości semantycznej. Technika ta opiera się na odkrywaniu „ścieżek programu” reprezentowanych jako formuły matematyczne zwane path predicates. Koncepcyjnie, technika ta operuje na predykatach ścieżek w dwóch krokach:

1. Są one konstruowane przy użyciu ograniczeń na wejściu programu.
2. Są one używane do generowania danych wejściowych programu, które spowodują wykonanie powiązanych ścieżek.

Podejście to nie generuje fałszywych alarmów, w tym sensie, że wszystkie zidentyfikowane stany programu mogą zostać wywołane podczas konkretnej egzekucji. Na przykład, jeśli analiza znajdzie przepełnienie liczby całkowitej, jest ono gwarantowanie odtwarzalne.

Przykład predykatu ścieżki

Aby zrozumieć, jak działa DSE, rozważmy następujący przykład:

1function f(uint a){
2
3  if (a == 65) {
4      // Występuje błąd
5  }
6
7}
Kopiuj

Ponieważ f() zawiera dwie ścieżki, DSE skonstruuje dwa różne predykaty ścieżek:

• Ścieżka 1: a == 65
• Ścieżka 2: Not (a == 65)

Każdy predykat ścieżki jest formułą matematyczną, którą można przekazać do tak zwanego solvera SMTopens in a new tab, który spróbuje rozwiązać równanie. Dla Ścieżki 1 solver stwierdzi, że ścieżka może być zbadana przy a = 65. Dla Ścieżki 2 solver może podać dla a dowolną wartość inną niż 65, na przykład a = 0.

Weryfikacja właściwości

Manticore pozwala na pełną kontrolę nad wykonaniem każdej ścieżki. W rezultacie pozwala na dodawanie dowolnych ograniczeń do prawie wszystkiego. Taka kontrola pozwala na tworzenie właściwości w kontrakcie.

Rozważmy następujący przykład:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // brak zabezpieczenia przed przepełnieniem
3  return c;
4}
Kopiuj

W tej funkcji istnieje tylko jedna ścieżka do zbadania:

• Ścieżka 1: c = a + b

Używając Manticore, można sprawdzić przepełnienie i dodać ograniczenia do predykatu ścieżki:

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

Jeśli możliwe jest znalezienie takich wartości a i b, dla których powyższy predykat ścieżki jest spełnialny, oznacza to, że znaleziono przepełnienie. Na przykład solver może wygenerować dane wejściowe a = 10, b = MAXUINT256.

Rozważmy poprawioną wersję:

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

Powiązana formuła ze sprawdzaniem przepełnienia wyglądałaby następująco:

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

Ta formuła nie może zostać rozwiązana; innymi słowy jest to dowód na to, że w safe_add, c zawsze będzie rosło.

Dlatego DSE jest potężnym narzędziem, które może weryfikować dowolne ograniczenia w Twoim kodzie.

Uruchamianie w Manticore

W tej sekcji pokazano, jak eksplorować inteligentny kontrakt przy użyciu API Manticore. Celem jest następujący inteligentny kontrakt example.solopens 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}
Pokaż wszystko
Kopiuj

Uruchomienie samodzielnej eksploracji

Możesz uruchomić Manticore bezpośrednio na inteligentnym kontrakcie za pomocą następującego polecenia (project może być plikiem Solidity lub katalogiem projektu):

$ manticore project

Otrzymasz dane wyjściowe przypadków testowych, takie jak te (kolejność może się zmienić):

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...
Pokaż wszystko

Bez dodatkowych informacji Manticore będzie badać kontrakt za pomocą nowych transakcji symbolicznych, dopóki nie zbada nowych ścieżek w kontrakcie. Manticore nie uruchamia nowych transakcji po nieudanej transakcji (np. po operacji revert).

Manticore zapisze informacje w katalogu mcore_*. W tym katalogu znajdziesz między innymi:

• global.summary: pokrycie kodu i ostrzeżenia kompilatora
• test_XXXXX.summary: pokrycie kodu, ostatnia instrukcja, salda kont dla każdego przypadku testowego
• test_XXXXX.tx: szczegółowa lista transakcji dla każdego przypadku testowego

Manticore znajduje tutaj 7 przypadków testowych, które odpowiadają (kolejność nazw plików może się zmienić):

Podsumowanie eksploracji: f(!=65) oznacza wywołanie f z dowolną wartością inną niż 65.

Jak można zauważyć, Manticore generuje unikalny przypadek testowy dla każdej pomyślnej lub anulowanej (reverted) transakcji.

Użyj flagi --quick-mode, jeśli chcesz szybkiej eksploracji kodu (wyłącza ona wykrywacze błędów, obliczanie gazu, ...)

Manipulowanie inteligentnym kontraktem poprzez API

Ta sekcja opisuje szczegółowo, jak manipulować inteligentnym kontraktem za pośrednictwem API Manticore dla Pythona. Możesz utworzyć nowy plik z rozszerzeniem Pythona *.py i napisać niezbędny kod, dodając polecenia API (których podstawy zostaną opisane poniżej) do tego pliku, a następnie uruchomić go za pomocą polecenia $ python3 *.py. Możesz również wykonać poniższe polecenia bezpośrednio w konsoli Pythona. Aby uruchomić konsolę, użyj polecenia $ python3.

Tworzenie kont

Pierwszą rzeczą, którą należy zrobić, jest zainicjowanie nowego blockchaina za pomocą następujących poleceń:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Kopiuj

Konto niebędące kontraktem jest tworzone za pomocą m.create_accountopens in a new tab:

1user_account = m.create_account(balance=1000)
Kopiuj

Kontrakt Solidity można wdrożyć za pomocą m.solidity_create_contractopens 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# Zainicjuj kontrakt
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Pokaż wszystko
Kopiuj

Podsumowanie

• Można tworzyć konta użytkowników i konta kontraktów za pomocą m.create_accountopens in a new tab i m.solidity_create_contractopens in a new tab.

Wykonywanie transakcji

Manticore obsługuje dwa typy transakcji:

• Surowa transakcja: wszystkie funkcje są badane
• Nazwana transakcja: tylko jedna funkcja jest badana

Surowa transakcja

Surowa transakcja jest wykonywana za pomocą m.transactionopens in a new tab:

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

Wywołujący, adres, dane lub wartość transakcji mogą być konkretne lub symboliczne:

• m.make_symbolic_valueopens in a new tab tworzy wartość symboliczną.
• m.make_symbolic_buffer(size)opens in a new tab tworzy symboliczną tablicę bajtów.

Na przykład:

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

Jeśli dane są symboliczne, Manticore zbada wszystkie funkcje kontraktu podczas wykonywania transakcji. Pomocne będzie zapoznanie się z wyjaśnieniem funkcji fallback w artykule Hands on the Ethernaut CTFopens in a new tab, aby zrozumieć, jak działa wybór funkcji.

Nazwana transakcja

Funkcje mogą być wykonywane za pomocą ich nazwy. Aby wykonać f(uint var) z wartością symboliczną, z user_account i 0 etherów, użyj:

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

Jeśli value transakcji nie jest określone, domyślnie wynosi 0.

Podsumowanie

• Argumenty transakcji mogą być konkretne lub symboliczne
• Surowa transakcja zbada wszystkie funkcje
• Funkcje mogą być wywoływane po nazwie

Przestrzeń robocza

m.workspace to katalog używany jako katalog wyjściowy dla wszystkich wygenerowanych plików:

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

Zakończenie eksploracji

Aby zatrzymać eksplorację, użyj m.finalize()opens in a new tab. Po wywołaniu tej metody nie należy wysyłać żadnych dalszych transakcji, a Manticore generuje przypadki testowe dla każdej zbadanej ścieżki.

Podsumowanie: Uruchamianie w Manticore

Łącząc wszystkie poprzednie kroki, otrzymujemy:

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("Results are in {}".format(m.workspace))
15m.finalize() # zatrzymaj eksplorację
Pokaż wszystko
Kopiuj

Cały powyższy kod można znaleźć w example_run.pyopens in a new tab

Uzyskiwanie ścieżek powodujących błąd

Teraz wygenerujemy określone dane wejściowe dla ścieżek zgłaszających wyjątek w f(). Celem nadal jest następujący inteligentny kontrakt example.solopens 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}
Kopiuj

Korzystanie z informacji o stanie

Każda wykonana ścieżka ma swój stan blockchaina. Stan jest gotowy albo zakończony (killed), co oznacza, że osiąga instrukcję THROW lub REVERT:

• m.ready_statesopens in a new tab: lista stanów, które są gotowe (nie wykonały REVERT/INVALID)
• m.killed_statesopens in a new tab: lista stanów, które są zakończone (killed)
• m.all_statesopens in a new tab: wszystkie stany

1for state in m.all_states:
2    # zrób coś ze stanem
Kopiuj

Możesz uzyskać dostęp do informacji o stanie. Na przykład:

• state.platform.get_balance(account.address): saldo konta
• state.platform.transactions: lista transakcji
• state.platform.transactions[-1].return_data: dane zwrócone przez ostatnią transakcję

Dane zwrócone przez ostatnią transakcję to tablica, którą można przekonwertować na wartość za pomocą ABI.deserialize, na przykład:

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

Jak wygenerować przypadek testowy

Użyj m.generate_testcase(state, name)opens in a new tab, aby wygenerować przypadek testowy:

1m.generate_testcase(state, 'BugFound')
Kopiuj

Podsumowanie

• Można iterować po stanach za pomocą m.all_states
• state.platform.get_balance(account.address) zwraca saldo konta
• state.platform.transactions zwraca listę transakcji
• transaction.return_data to zwrócone dane
• m.generate_testcase(state, name) generuje dane wejściowe dla stanu

Podsumowanie: uzyskiwanie ścieżki powodującej błąd

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## Sprawdź, czy wykonanie kończy się instrukcją REVERT lub 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('Throw found {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Pokaż wszystko
Kopiuj

Cały powyższy kod można znaleźć w example_run.pyopens in a new tab

Uwaga: mogliśmy wygenerować znacznie prostszy skrypt, ponieważ wszystkie stany zwrócone przez terminated_states mają w wyniku REVERT lub INVALID: ten przykład miał jedynie na celu zademonstrowanie, jak manipulować API.

Dodawanie ograniczeń

Zobaczymy, jak ograniczyć eksplorację. Przyjmiemy założenie, że dokumentacja funkcji f() stwierdza, że funkcja nigdy nie jest wywoływana z a == 65, więc każdy błąd przy a == 65 nie jest prawdziwym błędem. Celem nadal jest następujący inteligentny kontrakt example.solopens 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}
Kopiuj

Operatory

Moduł Operatorsopens in a new tab ułatwia manipulowanie ograniczeniami, między innymi udostępnia:

• Operators.AND,
• Operators.OR,
• Operators.UGT (większe niż bez znaku),
• Operators.UGE (większe lub równe niż bez znaku),
• Operators.ULT (mniejsze niż bez znaku),
• Operators.ULE (mniejsze lub równe niż bez znaku).

Aby zaimportować moduł, użyj następującego polecenia:

1from manticore.core.smtlib import Operators
Kopiuj

Operators.CONCAT służy do łączenia tablicy z wartością. Na przykład return_data transakcji musi zostać zmienione na wartość, aby można było je porównać z inną wartością:

1last_return = Operators.CONCAT(256, *last_return)
Kopiuj

Ograniczenia

Można używać ograniczeń globalnie lub dla określonego stanu.

Ograniczenie globalne

Użyj m.constrain(constraint), aby dodać ograniczenie globalne. Na przykład, można wywołać kontrakt z adresu symbolicznego i ograniczyć ten adres do określonych wartości:

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

Ograniczenie stanu

Użyj state.constrain(constraint)opens in a new tab, aby dodać ograniczenie do określonego stanu. Można go użyć do ograniczenia stanu po jego eksploracji, aby sprawdzić na nim pewną właściwość.

Sprawdzanie ograniczenia

Użyj solver.check(state.constraints), aby dowiedzieć się, czy ograniczenie jest nadal możliwe do spełnienia. Na przykład, poniższy kod ograniczy symbolic_value do wartości innej niż 65 i sprawdzi, czy stan jest nadal możliwy do spełnienia:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # stan jest możliwy do spełnienia
Kopiuj

Podsumowanie: dodawanie ograniczeń

Dodając ograniczenie do poprzedniego kodu, otrzymujemy:

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## Sprawdź, czy wykonanie kończy się instrukcją REVERT lub INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # nie bierzemy pod uwagę ścieżki, w której a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Bug found, results are in {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'No bug found')
Pokaż wszystko
Kopiuj

Cały powyższy kod można znaleźć w example_run.pyopens in a new tab