Zum Hauptinhalt springen

Wie man Manticore verwendet, um Fehler in Smart Contracts zu finden

Solidity
Smart Contracts
Sicherheit
Testen
formale Verifizierung
Experte
Trailofbits
13. Januar 2020
12 Minuten Lesezeit

Ziel dieses Tutorials ist es zu zeigen, wie man Manticore verwendet, um automatisch Fehler in Smart Contracts zu finden.

Installation

Manticore erfordert >= Python 3.6. Es kann über pip oder mit Docker installiert werden.

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-Container aus, der Zugriff auf Ihr aktuelles Verzeichnis hat. Sie können die Dateien von Ihrem Host aus ändern und die Tools auf die Dateien aus dem Docker-Container anwenden.

Führen Sie innerhalb von Docker Folgendes 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

Um ein Python-Skript mit Python 3 auszuführen:

python3 script.py

Einführung in die dynamische symbolische Ausführung

Dynamische symbolische Ausführung auf den Punkt gebracht

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

  1. Sie werden unter Verwendung von Einschränkungen (Constraints) 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-positiven Ergebnisse in dem Sinne, dass alle identifizierten Programmzustände während der konkreten Ausführung ausgelöst werden können. Wenn die Analyse beispielsweise einen Integer-Overflow (Ganzzahlüberlauf) findet, ist dieser garantiert reproduzierbar.

Beispiel für ein Pfadprädikat

Um einen Einblick in die Funktionsweise von DSE zu erhalten, betrachten Sie das folgende Beispiel:

1function f(uint a){
2

3  if (a == 65) {
4      // Ein Bug ist vorhanden
5  }
6

7}

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 versuchen wird, die Gleichung zu lösen. Für Pfad 1 wird der Solver angeben, dass der Pfad mit a = 65 erkundet werden kann. Für Pfad 2 kann der Solver a jeden anderen Wert als 65 zuweisen, zum Beispiel a = 0.

Eigenschaften verifizieren

Manticore ermöglicht die vollständige Kontrolle über die gesamte Ausführung jedes Pfades. Infolgedessen können Sie fast allem beliebige Einschränkungen hinzufügen. Diese Kontrolle ermöglicht die Erstellung von Eigenschaften für den Smart Contract.

Betrachten Sie das folgende Beispiel:

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

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

  • Pfad 1: c = a + b

Mit Manticore können Sie auf Überläufe 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 von a und b zu finden, für die das obige Pfadprädikat machbar ist, bedeutet dies, dass Sie einen Überlauf gefunden haben. Zum Beispiel kann der Solver die Eingabe a = 10 , b = MAXUINT256 generieren.

Wenn Sie eine korrigierte Version betrachten:

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}

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, dies ist ein Beweis, dass in safe_add c immer größer wird.

DSE ist somit ein leistungsstarkes Werkzeug, das beliebige Einschränkungen in Ihrem Code verifizieren kann.

Ausführen unter 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}

Eine eigenständige Untersuchung ausführen

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

$ manticore project

Sie erhalten 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...

Ohne zusätzliche Informationen wird Manticore den Smart Contract mit neuen symbolischen Transaktionen untersuchen, bis keine neuen Pfade im Smart Contract mehr gefunden werden. 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 finden Sie 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):

Transaktion 0Transaktion 1Transaktion 2Ergebnis
test_00000000.txVertragserstellungf(!=65)f(!=65)STOP
test_00000001.txVertragserstellungFallback-FunktionREVERT
test_00000002.txVertragserstellungRETURN
test_00000003.txVertragserstellungf(65)REVERT
test_00000004.txVertragserstellungf(!=65)STOP
test_00000005.txVertragserstellungf(!=65)f(65)REVERT
test_00000006.txVertragserstellungf(!=65)Fallback-FunktionREVERT

Die Untersuchungszusammenfassung f(!=65) bedeutet, dass f mit einem beliebigen Wert ungleich 65 aufgerufen wird.

Wie Sie feststellen können, generiert Manticore für jede erfolgreiche oder rückgängig gemachte (reverted) Transaktion einen eindeutigen Testfall.

Verwenden Sie das Flag --quick-mode, wenn Sie eine schnelle Code-Untersuchung wünschen (es deaktiviert Fehlerdetektoren, Gasberechnung, ...).

Einen Smart Contract über die API manipulieren

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

Konten erstellen

Das Erste, was Sie tun sollten, ist, eine neue Blockchain mit den folgenden Befehlen zu initiieren:

1from manticore.ethereum import ManticoreEVM
2

3m = ManticoreEVM()

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

1user_account = m.create_account(balance=1000)

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)

Zusammenfassung

Transaktionen ausführen

Manticore unterstützt zwei Arten von Transaktionen:

  • Rohe Transaktion (Raw transaction): Alle Funktionen werden untersucht.
  • Benannte Transaktion (Named transaction): Nur eine Funktion wird untersucht.

Rohe Transaktion

Eine rohe 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)

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

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

Wenn die Daten symbolisch sind, untersucht Manticore während der Transaktionsausführung alle Funktionen des Smart Contracts. Es ist hilfreich, die Erklärung zur 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, verwenden Sie:

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

Wenn der value (Wert) der Transaktion nicht angegeben ist, beträgt er standardmäßig 0.

Zusammenfassung

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

Arbeitsbereich

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

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

Die Untersuchung beenden

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

Zusammenfassung: Ausführen unter 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("Results are in {}".format(m.workspace))
15m.finalize() # die Erkundung stoppen

Den gesamten obigen Code finden Sie in der Datei example_run.py (opens in a new tab).

Pfade mit Ausnahmen (Throwing Paths) abrufen

Wir werden nun spezifische Eingaben für die Pfade generieren, die in f() eine Ausnahme auslösen. Das Ziel ist weiterhin 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}

Statusinformationen verwenden

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

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

Sie können auf Statusinformationen zugreifen. Zum 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 mit ABI.deserialize in einen Wert konvertiert werden kann, zum Beispiel:

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

Wie man einen Testfall generiert

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

1m.generate_testcase(state, 'BugFound')

Zusammenfassung

  • Sie können mit m.all_states über den Zustand iterieren.
  • state.platform.get_balance(account.address) gibt den Kontostand 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: Pfade mit Ausnahmen abrufen

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 einem REVERT oder INVALID endet
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')

Den gesamten obigen Code finden Sie in der Datei example_run.py (opens in a new tab).

Beachten Sie, dass wir ein viel einfacheres Skript hätten 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.

Einschränkungen hinzufügen

Wir werden sehen, wie man die Untersuchung einschränkt. Wir gehen davon aus, dass die Dokumentation von f() besagt, dass die Funktion niemals mit a == 65 aufgerufen wird, sodass jeder Fehler mit a == 65 kein echter Fehler ist. Das Ziel ist weiterhin 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}

Operatoren

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

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (unsigned greater than - vorzeichenlos größer als),
  • Operators.UGE (unsigned greater than or equal to - vorzeichenlos größer als oder gleich),
  • Operators.ULT (unsigned lower than - vorzeichenlos kleiner als),
  • Operators.ULE (unsigned lower than or equal to - vorzeichenlos kleiner als oder gleich).

Um das Modul zu importieren, verwenden Sie Folgendes:

1from manticore.core.smtlib import Operators

Operators.CONCAT wird verwendet, um ein Array mit einem Wert zu verketten. Zum Beispiel müssen die return_data einer Transaktion in einen Wert geändert werden, um gegen einen anderen Wert geprüft zu werden:

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

Einschränkungen

Sie können Einschränkungen global oder für einen bestimmten Zustand verwenden.

Globale Einschränkung

Verwenden Sie m.constrain(constraint), um eine globale Einschränkung hinzuzufügen. Zum Beispiel können Sie einen Smart Contract 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)

Zustandseinschränkung

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

Einschränkung überprüfen

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

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # Zustand ist zulässig

Zusammenfassung: Einschränkungen hinzufügen

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 einem REVERT oder INVALID endet
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # wir berücksichtigen den Pfad nicht, bei dem a == 65 ist
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')

Den gesamten obigen Code finden Sie in der Datei example_run.py (opens in a new tab).

Letzte Aktualisierung der Seite: 3. März 2026

myelinated-wackerowm (opens in a new tab)
nhszn (opens in a new tab)
rex4539r (opens in a new tab)
+7

War dieses Tutorial hilfreich?