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

solidity

inteligentne kontrakty

ochrona

testing

weryfikacja formalna

zaawansowane

️Trailofbits

Tworzenie bezpiecznych kontraktów

January 13, 2020

5 minuta czytania

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:

Są one konstruowane przy użyciu ograniczeń na wejściu programu.
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}
8
 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, 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}
5
 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}
7
 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:

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
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...
11
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ć):

	Transakcja 0	Transakcja 1	Transakcja 2	Wynik
test_00000000.tx	Tworzenie kontraktu	f(!=65)	f(!=65)	STOP
test_00000001.tx	Tworzenie kontraktu	funkcja zastępcza		REVERT
test_00000002.tx	Tworzenie kontraktu			RETURN
test_00000003.tx	Tworzenie kontraktu	f(65)		REVERT
test_00000004.tx	Tworzenie kontraktu	f(!=65)		STOP
test_00000005.tx	Tworzenie kontraktu	f(!=65)	f(65)	REVERT
test_00000006.tx	Tworzenie kontraktów	f(!=65)	funkcja zastępcza	REVERT

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

Konto bez kontraktu jest tworzone przy użyciu m.create_account:

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

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

Podsumowanie

Konta użytkowników i konitraktów można tworzyć za pomocą m.create_account i [m.solidity_create_contract](https://manticore.readthedocs.io/en/latest/api.html#manticore.ethereum.ManticoreEVM.solidity_create_contract.

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:

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

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

m.make_symbolic_value tworzy wartość symboliczną.
m.make_symbolic_buffer(size) 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)
7
 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.

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

Kończenie eksploracji

Aby zatrzymać eksplorację, użyj m.finalize(). 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
16
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py

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:

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
 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: lista stanów, które są gotowe (nie wykonały REVERT/INVALID)
m.killed_states: lista stanów, które są gotowe (nie wykonały REVERT/INVALID)
m.all_states: wszystkie stany

1for state in m.all_states:
2    # do something with state
3
 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)
3
 Kopiuj

Jak wygenerować przypadek testowy

Użyj m.generate_testcase(stan, nazwa) aby wygenerować testcase:

1m.generate_testcase(state, 'BugFound')
2
 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')
20
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py

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:

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
 Kopiuj

Operatory

Moduł Operatorzy 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
2
 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)
2
 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)
7
 Kopiuj

Ograniczenie stanu

Użyj state.constrain(constraint), 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
4
 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')
31
Pokaż wszystko
 Kopiuj

Cały powyższy kod można znaleźć w example_run.py

Ostatnia edycja: , Invalid DateTime

Edit page

Pomóż nam zaktualizować tę stronę

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

Instalacja

Manticore przez dockera

Manticore przez pip

Uruchom skrypt

Wprowadzenie do dynamicznego wykonania symbolicznego

Dynamiczne wykonanie symboliczne w skrócie

Przykład predykatu ścieżki

Weryfikacja właściwości

Uruchamianie pod Manticore

Uruchom samodzielną eksplorację

Obsługa inteligentnego kontraktu poprzez API

Tworzenie kont

Podsumowanie

Wykonywanie transakcji

Transakcja surowa

Nazwana transakcja

Podsumowanie

Obszar roboczy

Kończenie eksploracji

Podsumowanie: uruchamianie pod Manticore

Pobieranie ścieżek zgłaszania

Używanie informacji o stanie

Jak wygenerować przypadek testowy

Podsumowanie

Podsumowanie: uzyskanie ścieżki zgłaszania

Dodawanie ograniczeń

Operatory

Ograniczenia

Globalne ograniczenie

Ograniczenie stanu

Sprawdzanie ograniczenia

Podsumowanie: dodwanie ograniczeń