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 dockera

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

zaleca się solc 0.5.11.

Uruchom skrypt

Aby uruchomić skrypt Pythona za pomocą Pythona 3:

python3 script.py

Wprowadzenie do dynamicznego wykonania symbolicznego

Dynamiczne wykonanie symboliczne w skrócie

Dynamiczne wykonanie symboliczne (DSE) to technika analizy programu, która bada przestrzeń stanów z wysokim stopniem świadomości semantycznej. Ta technika opiera się na odkryciu „ścieżek programu”, przedstawianych jako wzory matematyczne o nazwie path predicates. W ujęciu koncepcyjnym technika ta działa na ścieżce dwueatpowo:

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.

Takie podejście nie daje fałszywych alarmów w tym sensie, że wszystkie zidentyfikowane stany programu mogą zostać wyzwolone podczas konkretnego wykonania. Na przykład, jeżeli w wyniku analizy stwierdza się przepełnienie liczby całkowitej, gwarantuje się, że jest ono 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      // A bug is present
5  }
6
7}
 Kopiuj

Jako że f() zawiera dwie ścieżki, DSE będzie konstruować dwa różne predykaty ścieżki:

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

Każdy predykat ścieżki jest wzorem matematycznym, który można przypisać tak zwanemu SMT solver(opens in a new tab), który spróbuje rozwiązać to równanie. W przypadku Path 1 solver powie, że ścieżka może zostać zbadana za pomocą a = 65. Dla Path 2 solver może dać a dowolną wartość inną niż 65, na przykład a = 0.

Weryfikacja właściwości

Manticore pozwala na pełną kontrolę nad każdym wykonaniem każdej ścieżki. W rezultacie pozwala dodawać dowolne ograniczenia do prawie wszystkiego. Kontrola ta pozwala na tworzenie właściwości na kontrakcie.

Rozważ następujący przykład:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // no overflow protection
3  return c;
4}
 Kopiuj

Tutaj jest tylko jedna ścieżka do zbadania w funkcji:

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

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

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

Jeśli można znaleźć ocenę a i b, dla której powyższy predykat ścieżki jest wykonalny, oznacza to, że znaleziono przepełnienie. Na przykład solver może wygenerować wejście a = 10 , b = MAXUINT256.

Jeśli rozważasz wersję stałą:

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ązany wzór z kontrolą przepełnienia to:

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

Ten wzór nie może być rozwiązany; innymi słowy jest to dowód, że w safe_add c zawsze będzie wzrastać.

DSE jest więc potężnym narzędziem, które może weryfikować dowolne ograniczenia Twojego kodu.

Uruchamianie pod Manticore

Zobaczymy, jak zbadać inteligentny kontrakt z API Manticore. Celem jest następujący inteligentny 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}
Pokaż wszystko
 Kopiuj

Uruchom samodzielną eksplorację

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

$ manticore project

Otrzymasz wyniki takich przypadków testowych (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ą nowej transakcji symbolicznej, dopóki nie zbada nowych ścieżek w kontrakcie. Manticore nie uruchamia nowych transakcji po niepowodzeniu (np. po wycofaniu).

Manticore umieści te informacje w katalogu mcore_*. W tym katalogu znajdziesz między innymi:

• global.summary: ostrzeżenia o zakresie i kompilatorze
• test_XXXXX.summary: zakres, ostatnia instrukcja, salda konta na przypadek testowy
• test_XXXXX.tx: szczegółowa lista transakcji na przypadek testowy

W tym miejscu Manticore znajduje 7 przypadków testowych, które odpowiadają (nazwa pliku może się zmienić):

Podsumowanie eksploracji f(!=65) oznacza f o dowolnej wartości innej niż 65.

Jak możesz zauważyć, Manticore generuje unikalny przypadek testowy dla każdej udanej lub odwróconej transakcji.

Użyj flagi --quick-mode, jeśli chcesz szybko eksplorować kod (wyłącza wykrywanie błędów, obliczanie gazu, ...)

Obsługa inteligentnego kontraktu poprzez API

W tej sekcji opisano szczegóły, jak obsługiwać inteligentny kontrakt za pośrednictwem API Pythona Manticore. Możesz utworzyć nowy plik z rozszerzeniem python *.py i napisać potrzebny kod, dodając polecenia API (podstawy, które zostaną opisane poniżej) do tego pliku, a następnie uruchom go poleceniem $ 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ą powinieneś zrobić, jest uruchomienie nowego blockchaina za pomocą następujących poleceń:

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

Konto bez kontraktu jest tworzone przy użyciu m.create_account(opens in a new tab):

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

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

Podsumowanie

• Konta użytkowników i konitraktów można tworzyć za pomocą m.create_account(opens in a new tab) i m.solidity_create_contract(opens in a new tab).

Wykonywanie transakcji

Manticore obsługuje dwa rodzaje transakcji:

• Transakcja surowa: wszystkie funkcje są analizowane
• Nazwana transakcja: analizowana jest tylko jedna funkcja

Transakcja surowa

Surowa transakcja jest wykonywana przy użyciu m.transaction(opens 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_value(opens 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żeli dane są symboliczne, Manticore zbada wszystkie funkcje kontraktu podczas realizacji transakcji. Pomocne będzie zapoznanie się z wyjaśnieniem funkcji fallback w artykule wyjaśniającym, jak działa wybór funkcji: Hands on the Ethernaut CTF(opens in a new tab).

Nazwana transakcja

Funkcje mogą być wykonywane za pośrednictwem 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 wartość value transakcji nie jest określona, jest to domyślnie 0.

Podsumowanie

• Argumenty transakcji mogą być konkretne lub symboliczne
• Surowa transakcja analizuje wszystkie funkcje
• Funkcja może być wywołana przez jej nazwę

Obszar roboczy

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

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

Kończenie eksploracji

Aby zatrzymać eksplorację, użyj m.finalize()(opens in a new tab). Kolejne transakcje nie powinny być wysyłane po wywołaniu tej metody i wygenerowaniu przypadków testowych dla każdej zbadanej ścieżki.

Podsumowanie: uruchamianie pod 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() # stop the exploration
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py(opens in a new tab)

Pobieranie ścieżek zgłaszania

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

Używanie informacji o stanie

Każda wykonana ścieżka ma swój stan blockchain. Stan jest gotowy lub został zabity, co oznacza, że osiąga instrukcję THROW lub REVERT:

• m.ready_states(opens in a new tab): lista stanów, które są gotowe (nie wykonały REVERT/INVALID)
• m.killed_states(opens in a new tab): lista stanów, które są gotowe (nie wykonały REVERT/INVALID)
• m.all_states(opens in a new tab): wszystkie stany

1for state in m.all_states:
2    # do something with state
 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ę są tablicą, która może zostać przekonwertowana na wartość z 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(stan, nazwa)(opens in a new tab) aby wygenerować testcase:

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

Podsumowanie

• Możesz iterować ponad stanem za pomocą stanów m.all_states
• state.platform.get_balance(account.address) zwraca saldo konta
• State.platform.transactions zwraca listę transakcji
• transaction.return_data to dane zwrócone
• m.generate_testcase(stan, nazwa) generuje dane wejściowe dla stanu

Podsumowanie: uzyskanie ścieżki zgłaszania

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')
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py(opens in a new tab)

Zauważ, że mogliśmy wygenerować znacznie prostszy skrypt, ponieważ wszystkie stany zwrócone przez terminated_state mają w wyniku REVERT lub INVALID: ten przykład miał jedynie zademonstrować, jak obsługiwać API.

Dodawanie ograniczeń

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

Operatory

Moduł Operatorzy(opens in a new tab) ułatwia manipulowanie ograniczeniami między innymi:

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

Aby zaimportować moduł, użyj następujących elementów:

1from manticore.core.smtlib import Operators
 Kopiuj

Operators.CONCAT jest używany do dołączania tablicy do wartości. Na przykład należy zmienić wartość return_data transakcji na wartość sprawdzaną względem innej wartości:

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

Ograniczenia

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

Globalne ograniczenie

Użyj m.constrain (constraint) aby dodać globalne ograniczenie. Na przykład możesz 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że być używany do ograniczania stanu po jego eksploracji, aby sprawdzić na nim jakąś właściwość.

Sprawdzanie ograniczenia

Użyj solver.check(state.constraints), aby dowiedzieć się, czy ograniczenie jest nadal możliwe. Na przykład poniższe ograniczy symbolic_value do wartości różnej od 65 i sprawdzi, czy stan jest nadal możliwy:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # state is feasible
 Kopiuj

Podsumowanie: dodwanie 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## 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')
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py(opens in a new tab)