So nutzt du Manticore, um Fehler in Smart Contracts zu finden

Das Ziel dieses Tutorials ist es zu zeigen, wie du Manticore nutzt, um automatisch Fehler in Smart Contracts zu finden.

Installation

Manticore erfordert Python >= 3.6. Die Installation kann über pip oder Docker erfolgen.

Manticore über Docker

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

Der letzte Befehl führt die eth-security-toolbox in einem Docker aus, der Zugriff auf dein aktuelles Verzeichnis hat. Du kannst die Dateien von deinem Host aus ändern und die Tools für die Dateien aus dem Docker ausführen

Führe im Docker aus:

solc-select 0.5.11
cd /home/trufflecon/

Manticore über pip

pip3 install --user manticore

solc 0.5.11 wird empfohlen.

Ausführen eines Skripts

So führst du ein Python-Skript mit Python 3 aus:

python3 script.py

Einführung in die dynamische symbolische Ausführung

Dynamische symbolische Ausführung – kurz erklärt

Die dynamische symbolische Ausführung (DSE) ist eine Programmanalysetechnik, die einen Zustandsraum mit einem hohen Grad an semantischem Bewusstsein untersucht. Diese Technik basiert auf der Entdeckung von „Programmpfaden“, die als mathematische Formeln, sogenannte path predicates, dargestellt werden. Konzeptionell arbeitet diese Technik in zwei Schritten mit Pfadprädikaten:

1. Sie werden unter Verwendung von Einschränkungen für die Programmeingabe konstruiert.
2. Sie werden verwendet, um Programmeingaben zu generieren, die die Ausführung der zugehörigen Pfade bewirken.

Dieser Ansatz erzeugt keine Falsch-Positiv-Meldungen, da alle identifizierten Programmzustände während einer konkreten Ausführung ausgelöst werden können. Findet die Analyse beispielsweise einen Integer-Überlauf, ist dieser garantiert reproduzierbar.

Beispiel für ein Pfadprädikat

Um einen Einblick in die Funktionsweise von DSE zu erhalten, sieh dir das folgende Beispiel an:

1function f(uint a){
2
3  if (a == 65) {
4      // Ein Fehler ist vorhanden
5  }
6
7}
Kopieren

Da f() zwei Pfade enthält, konstruiert eine DSE zwei verschiedene Pfadprädikate:

• Pfad 1: a == 65
• Pfad 2: Not (a == 65)

Jedes Pfadprädikat ist eine mathematische Formel, die an einen sogenannten SMT-Solver (opens in a new tab) übergeben werden kann, der versucht, die Gleichung zu lösen. Für Pfad 1 wird der Solver ausgeben, dass der Pfad mit a = 65 untersucht werden kann. Für Pfad 2 kann der Solver für a einen beliebigen anderen Wert als 65 angeben, zum Beispiel a = 0.

Überprüfen von Eigenschaften

Manticore ermöglicht die vollständige Kontrolle über die gesamte Ausführung jedes Pfades. Dadurch kannst du beliebige Einschränkungen für fast alles hinzufügen. Diese Kontrolle ermöglicht das Erstellen von Eigenschaften für den Vertrag.

Betrachte das folgende Beispiel:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // kein Überlaufschutz
3  return c;
4}
Kopieren

Hier gibt es in der Funktion nur einen Pfad zu untersuchen:

• Pfad 1: c = a + b

Mit Manticore kannst du auf einen Überlauf prüfen und dem Pfadprädikat Einschränkungen hinzufügen:

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

Wenn es möglich ist, eine Bewertung für a und b zu finden, für die das obige Pfadprädikat erfüllbar ist, bedeutet das, dass du einen Überlauf gefunden hast. Der Solver kann beispielsweise die Eingabe a = 10 , b = MAXUINT256 generieren.

Wenn du eine korrigierte Version betrachtest:

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

Die zugehörige Formel mit Überlaufprüfung wäre:

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

Diese Formel kann nicht gelöst werden; mit anderen Worten, das ist ein Beweis dafür, dass in safe_add der Wert c immer größer wird.

DSE ist somit ein leistungsfähiges Tool, das beliebige Einschränkungen in deinem Code überprüfen kann.

Ausführung mit Manticore

Wir werden sehen, wie man einen Smart Contract mit der Manticore-API untersucht. Das Ziel ist der folgende Smart Contract 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}
Alles anzeigen
Kopieren

Eine eigenständige Untersuchung ausführen

Du kannst Manticore mit dem folgenden Befehl direkt auf dem Smart Contract ausführen (project kann eine Solidity-Datei oder ein Projektverzeichnis sein):

$ manticore project

Du erhältst die Ausgabe von Testfällen wie diesem (die Reihenfolge kann sich ändern):

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...
Alles anzeigen

Ohne zusätzliche Informationen untersucht Manticore den Vertrag mit neuen symbolischen Transaktionen, bis es keine neuen Pfade mehr auf dem Vertrag untersucht. Manticore führt nach einer fehlgeschlagenen Transaktion (z. B. nach einem Revert) keine neuen Transaktionen aus.

Manticore gibt die Informationen in einem mcore_*-Verzeichnis aus. Unter anderem findest du in diesem Verzeichnis:

• global.summary: Abdeckung und Compiler-Warnungen
• test_XXXXX.summary: Abdeckung, letzte Anweisung, Kontostände pro Testfall
• test_XXXXX.tx: detaillierte Liste der Transaktionen pro Testfall

Hier findet Manticore 7 Testfälle, die Folgendem entsprechen (die Reihenfolge der Dateinamen kann sich ändern):

Zusammenfassung der Untersuchung: f(!=65) bezeichnet einen Aufruf von f mit einem beliebigen Wert, der nicht 65 ist.

Wie du sehen kannst, generiert Manticore für jede erfolgreiche oder rückgängig gemachte (reverted) Transaktion einen eindeutigen Testfall.

Verwende das --quick-mode-Flag, wenn du eine schnelle Code-Untersuchung wünschst (es deaktiviert Fehlerdetektoren, Gas-Berechnung, ...)

Einen Smart Contract über die API manipulieren

Dieser Abschnitt beschreibt im Detail, wie man einen Smart Contract über die Manticore-Python-API manipuliert. Du kannst eine neue Datei mit der Python-Erweiterung *.py erstellen und den notwendigen Code schreiben, indem du die API-Befehle (deren Grundlagen unten beschrieben werden) in diese Datei einfügst und sie dann mit dem Befehl $ python3 *.py ausführst. Du kannst die folgenden Befehle auch direkt in der Python-Konsole ausführen. Um die Konsole zu starten, verwende den Befehl $ python3.

Erstellen von Konten

Als Erstes solltest du mit den folgenden Befehlen eine neue Blockchain initialisieren:

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

Ein Nicht-Vertragskonto wird mit m.create_account (opens in a new tab) erstellt:

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

Ein Solidity-Vertrag kann mit m.solidity_create_contract (opens in a new tab) bereitgestellt werden:

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)
Alles anzeigen
Kopieren

Zusammenfassung

• Du kannst Benutzer- und Vertragskonten mit m.create_account (opens in a new tab) und m.solidity_create_contract (opens in a new tab) erstellen.

Ausführen von Transaktionen

Manticore unterstützt zwei Arten von Transaktionen:

• Raw-Transaktion: Alle Funktionen werden untersucht
• Benannte Transaktion: Es wird nur eine Funktion untersucht

Raw-Transaktion

Eine Raw-Transaktion wird mit m.transaction (opens in a new tab) ausgeführt:

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

Der Aufrufer, die Adresse, die Daten oder der Wert der Transaktion können entweder konkret oder symbolisch sein:

• m.make_symbolic_value (opens in a new tab) erstellt einen symbolischen Wert.
• m.make_symbolic_buffer(size) (opens in a new tab) erstellt ein symbolisches Byte-Array.

Beispiel:

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

Wenn die Daten symbolisch sind, untersucht Manticore während der Transaktionsausführung alle Funktionen des Vertrags. Es ist hilfreich, die Erklärung der Fallback-Funktion im Artikel Hands on the Ethernaut CTF (opens in a new tab) zu lesen, um zu verstehen, wie die Funktionsauswahl funktioniert.

Benannte Transaktion

Funktionen können über ihren Namen ausgeführt werden. Um f(uint var) mit einem symbolischen Wert, von user_account und mit 0 Ether auszuführen, verwende:

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

Wenn der value der Transaktion nicht angegeben ist, ist er standardmäßig 0.

Zusammenfassung

• Argumente einer Transaktion können konkret oder symbolisch sein
• Eine Raw-Transaktion untersucht alle Funktionen
• Funktionen können über ihren Namen aufgerufen werden

Arbeitsbereich

m.workspace ist das Verzeichnis, das als Ausgabeverzeichnis für alle erzeugten Dateien verwendet wird:

1print("Ergebnisse sind in {}".format(m.workspace))
Kopieren

Die Untersuchung beenden

Um die Untersuchung zu beenden, verwende m.finalize() (opens in a new tab). Sobald diese Methode aufgerufen wird, sollten keine weiteren Transaktionen gesendet werden. Manticore generiert dann Testfälle für jeden untersuchten Pfad.

Zusammenfassung: Ausführung mit Manticore

Wenn wir alle vorherigen Schritte zusammenfassen, erhalten wir:

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("Ergebnisse sind in {}".format(m.workspace))
15m.finalize() # die Untersuchung anhalten
Alles anzeigen
Kopieren

Den gesamten obigen Code findest du in example_run.py (opens in a new tab)

Pfade erhalten, die eine Ausnahme auslösen

Wir generieren nun spezifische Eingaben für die Pfade, die in f() eine Ausnahme auslösen. Das Ziel ist nach wie vor der folgende Smart Contract 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}
Kopieren

Verwenden von Zustandsinformationen

Jeder ausgeführte Pfad hat seinen eigenen Zustand der Blockchain. Ein Zustand ist entweder bereit (ready) oder beendet (killed), was bedeutet, dass er eine THROW- oder REVERT-Anweisung erreicht:

• m.ready_states (opens in a new tab): die Liste der Zustände, die bereit sind (sie haben kein REVERT/INVALID ausgeführt)
• m.killed_states (opens in a new tab): die Liste der beendeten Zustände
• m.all_states (opens in a new tab): alle Zustände

1for state in m.all_states:
2    # etwas mit dem Zustand tun
Kopieren

Du kannst auf Zustandsinformationen zugreifen. Beispiel:

• state.platform.get_balance(account.address): der Kontostand des Kontos
• state.platform.transactions: die Liste der Transaktionen
• state.platform.transactions[-1].return_data: die von der letzten Transaktion zurückgegebenen Daten

Die von der letzten Transaktion zurückgegebenen Daten sind ein Array, das beispielsweise mit ABI.deserialize in einen Wert umgewandelt werden kann:

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

So generierst du einen Testfall

Verwende m.generate_testcase(state, name) (opens in a new tab), um einen Testfall zu generieren:

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

Zusammenfassung

• Du kannst mit m.all_states über die Zustände iterieren
• state.platform.get_balance(account.address) gibt den Kontostand des Kontos zurück
• state.platform.transactions gibt die Liste der Transaktionen zurück
• transaction.return_data sind die zurückgegebenen Daten
• m.generate_testcase(state, name) generiert Eingaben für den Zustand

Zusammenfassung: Pfad erhalten, der eine Ausnahme auslöst

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## Prüfen, ob eine Ausführung mit REVERT oder INVALID endet
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Ausnahme gefunden {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Alles anzeigen
Kopieren

Den gesamten obigen Code findest du in example_run.py (opens in a new tab)

Hinweis: Wir hätten ein viel einfacheres Skript generieren können, da alle von terminated_state zurückgegebenen Zustände REVERT oder INVALID in ihrem Ergebnis haben: Dieses Beispiel sollte nur demonstrieren, wie man die API manipuliert.

Hinzufügen von Einschränkungen

Wir werden sehen, wie man die Untersuchung einschränken kann. Wir gehen von der Annahme aus, dass die Dokumentation von f() besagt, dass die Funktion niemals mit a == 65 aufgerufen wird, sodass jeder Fehler bei a == 65 kein echter Fehler ist. Das Ziel ist nach wie vor der folgende Smart Contract 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}
Kopieren

Operatoren

Das Operators (opens in a new tab)-Modul erleichtert die Bearbeitung von Einschränkungen und bietet unter anderem Folgendes:

• Operators.AND,
• Operators.OR,
• Operators.UGT (unsigned greater than),
• Operators.UGE (unsigned greater than or equal to),
• Operators.ULT (unsigned lower than),
• Operators.ULE (unsigned lower than or equal to).

Verwende Folgendes, um das Modul zu importieren:

1from manticore.core.smtlib import Operators
Kopieren

Operators.CONCAT wird verwendet, um ein Array mit einem Wert zu verketten. Zum Beispiel muss return_data einer Transaktion in einen Wert geändert werden, um ihn mit einem anderen Wert zu vergleichen:

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

Einschränkungen

Du kannst Einschränkungen global oder für einen bestimmten Zustand verwenden.

Globale Einschränkung

Verwende m.constrain(constraint), um eine globale Einschränkung hinzuzufügen. Du kannst zum Beispiel einen Vertrag von einer symbolischen Adresse aus aufrufen und diese Adresse auf bestimmte Werte beschränken:

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

Zustandsbeschränkung

Verwende state.constrain(constraint) (opens in a new tab), um eine Einschränkung zu einem bestimmten Zustand hinzuzufügen. Dies kann verwendet werden, um den Zustand nach seiner Untersuchung einzuschränken, um eine Eigenschaft darin zu überprüfen.

Einschränkung prüfen

Verwende solver.check(state.constraints), um zu erfahren, ob eine Einschränkung noch erfüllbar ist. Das folgende Beispiel schränkt beispielsweise symbolic_value so ein, dass es sich von 65 unterscheidet, und prüft, ob der Zustand noch erfüllbar ist:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # Zustand ist erfüllbar
Kopieren

Zusammenfassung: Hinzufügen von Einschränkungen

Wenn wir dem vorherigen Code eine Einschränkung hinzufügen, erhalten wir:

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## Prüfen, ob eine Ausführung mit REVERT oder INVALID endet
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # wir betrachten den Pfad nicht, in dem a == 65 ist
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Fehler gefunden, Ergebnisse sind in {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Kein Fehler gefunden')
Alles anzeigen
Kopieren

Den gesamten obigen Code findest du in example_run.py (opens in a new tab)

Seite zuletzt aktualisiert: 26. April 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Siehe Mitwirkende