Jak używać Manticore do znajdowania błędów w inteligentnych kontraktach

Solidity

inteligentne kontrakty

bezpieczeństwo

testowanie

weryfikacja formalna

Zaawansowany

Trailofbits

Building secure contracts

13 stycznia 2020

11 minut czytania

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

Instalacja

Manticore wymaga języka Python w wersji >= 3.6. Można go zainstalować za pomocą pip lub używając narzędzia Docker.

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 kontenerze Docker, który ma dostęp do bieżącego katalogu. Możesz zmieniać pliki na swoim hoście i uruchamiać narzędzia na plikach z poziomu Dockera

Wewnątrz Dockera uruchom:

solc-select 0.5.11
cd /home/trufflecon/

Manticore przez pip

pip3 install --user manticore

Zalecana jest wersja solc 0.5.11.

Uruchamianie skryptu

Aby uruchomić skrypt w języku Python za pomocą Python 3:

python3 script.py

Wprowadzenie do dynamicznego wykonywania symbolicznego

Dynamiczne wykonywanie symboliczne w pigułce

Dynamiczne wykonywanie symboliczne (DSE) to technika analizy programów, 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 (predykatami ścieżek). Koncepcyjnie technika ta operuje na predykatach ścieżek w dwóch krokach:

Są one konstruowane przy użyciu ograniczeń nałożonych na dane wejściowe programu.
Są one używane do generowania danych wejściowych programu, które spowodują wykonanie powiązanych ścieżek.

Takie podejście nie generuje fałszywych alarmów (false positives) w tym sensie, że wszystkie zidentyfikowane stany programu mogą zostać wywołane podczas konkretnego wykonania. Na przykład, jeśli analiza znajdzie przepełnienie liczby całkowitej, gwarantuje to, że jest ono powtarzalne.

Przykład predykatu ścieżki

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

function f(uint a){

  if (a == 65) {
      // Występuje błąd
  }

}

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 solwera SMT (opens in a new tab), który spróbuje rozwiązać równanie. Dla Path 1 solwer stwierdzi, że ścieżkę można zbadać za pomocą a = 65. Dla Path 2 solwer może przypisać a dowolną wartość inną niż 65, na przykład a = 0.

Weryfikacja właściwości

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

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

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // brak ochrony przed przepełnieniem
  return c;
}

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

Ścieżka 1: c = a + b

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

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

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

Jeśli weźmiesz pod uwagę naprawioną wersję:

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

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

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

Tej formuły nie da się rozwiązać; innymi słowy jest to dowód, że w safe_add wartość c zawsze będzie rosła.

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

Uruchamianie pod Manticore

Zobaczymy, jak badać inteligentny kontrakt za pomocą API Manticore. Celem jest następujący inteligentny 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();
        }
    }
}

Uruchamianie 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 wyniki przypadków testowych podobne do tych (kolejność może ulec zmianie):

...
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 0 - STOP
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 1 - REVERT
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 2 - RETURN
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 3 - REVERT
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 4 - STOP
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 5 - REVERT
... m.c.manticore:INFO: Wygenerowano przypadek testowy nr 6 - REVERT
... m.c.manticore:INFO: Wyniki w /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

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

Manticore wypisze 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

Tutaj Manticore znajduje 7 przypadków testowych, które odpowiadają (kolejność nazw plików może ulec zmianie):

	Transakcja 0	Transakcja 1	Transakcja 2	Wynik
test_00000000.tx	Utworzenie kontraktu	f(!=65)	f(!=65)	STOP
test_00000001.tx	Utworzenie kontraktu	funkcja rezerwowa		REVERT
test_00000002.tx	Utworzenie kontraktu			RETURN
test_00000003.tx	Utworzenie kontraktu	f(65)		REVERT
test_00000004.tx	Utworzenie kontraktu	f(!=65)		STOP
test_00000005.tx	Utworzenie kontraktu	f(!=65)	f(65)	REVERT
test_00000006.tx	Utworzenie kontraktu	f(!=65)	funkcja rezerwowa	REVERT

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

Jak można zauważyć, Manticore generuje unikalny przypadek testowy dla każdej udanej lub wycofanej transakcji.

Użyj flagi --quick-mode, jeśli zależy Ci na szybkiej eksploracji kodu (wyłącza to detektory błędów, obliczanie gazu itp.).

Manipulowanie inteligentnym kontraktem przez API

Ta sekcja opisuje szczegóły manipulowania inteligentnym kontraktem za pomocą API Manticore w języku Python. Możesz utworzyć nowy plik z rozszerzeniem Pythona *.py i napisać niezbędny kod, dodając do niego polecenia API (których podstawy zostaną opisane poniżej), a następnie uruchomić go za pomocą polecenia $ python3 *.py. Możesz również wykonywać poniższe polecenia bezpośrednio w konsoli Pythona; aby uruchomić konsolę, użyj polecenia $ python3.

Tworzenie kont

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

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

Konto niebędące kontraktem tworzy się za pomocą m.create_account (opens in a new tab):

user_account = m.create_account(balance=1000)

Kontrakt w języku Solidity można wdrożyć za 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)

Podsumowanie

Możesz tworzyć konta użytkowników i konta kontraktów za pomocą m.create_account (opens in a new tab) oraz m.solidity_create_contract (opens in a new tab).

Wykonywanie transakcji

Manticore obsługuje dwa typy transakcji:

Transakcja surowa (raw transaction): badane są wszystkie funkcje
Transakcja nazwana (named transaction): badana jest tylko jedna funkcja

Transakcja surowa

Surową transakcję wykonuje się za pomocą m.transaction (opens in a new tab):

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

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:

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)

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

Transakcja nazwana

Funkcje można wykonywać poprzez ich nazwę. Aby wykonać f(uint var) z wartością symboliczną, z konta user_account i z wartością 0 ether, użyj:

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

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

Podsumowanie

Argumenty transakcji mogą być konkretne lub symboliczne
Surowa transakcja zbada wszystkie funkcje
Funkcje można wywoływać po ich nazwie

Przestrzeń robocza

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

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

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 wygeneruje przypadki testowe dla każdej zbadanej ścieżki.

Podsumowanie: Uruchamianie pod Manticore

Łącząc wszystkie poprzednie kroki, otrzymujemy:

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() # zatrzymaj eksplorację

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

Uzyskiwanie ścieżek zgłaszających wyjątki

Wygenerujemy teraz 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):

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

Korzystanie z informacji o stanie

Każda wykonana ścieżka ma swój stan blockchaina. Stan jest albo gotowy (ready), albo zabity (killed), 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 zostały zabite
m.all_states (opens in a new tab): wszystkie stany

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

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:

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

Jak wygenerować przypadek testowy

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

m.generate_testcase(state, 'BugFound')

Podsumowanie

Możesz iterować po stanie 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 zgłaszającej wyjątek

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)

## Sprawdź, czy wykonanie kończy się wycofaniem lub 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')

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

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

Dodawanie ograniczeń

Zobaczymy, jak ograniczyć eksplorację. Założymy, ż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 prawdziwym błędem. Celem jest nadal następujący inteligentny 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();
        }
    }
}

Operatory

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

Operators.AND,
Operators.OR,
Operators.UGT (unsigned greater than - bez znaku większe niż),
Operators.UGE (unsigned greater than or equal to - bez znaku większe lub równe),
Operators.ULT (unsigned lower than - bez znaku mniejsze niż),
Operators.ULE (unsigned lower than or equal to - bez znaku mniejsze lub równe).

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

from manticore.core.smtlib import Operators

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

last_return = Operators.CONCAT(256, *last_return)

Ograniczenia

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

Ograniczenie globalne

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

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)

Ograniczenie stanu

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

Sprawdzanie ograniczenia

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

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # stan jest wykonalny

Podsumowanie: Dodawanie ograniczeń

Dodając ograniczenie do poprzedniego kodu, otrzymujemy:

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

## Sprawdź, czy wykonanie kończy się wycofaniem lub INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # nie rozważamy ścieżki, w której 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')

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