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

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

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 (DSE) ist eine Programmanalysetechnik, die einen Zustandsraum mit einem hohen Maß an semantischem Bewusstsein untersucht. Diese Technik basiert auf der Erkennung von „Programmpfaden“, die als mathematische Formeln dargestellt werden, die path predicates genannt werden. Konzeptionell arbeitet diese Technik in zwei Schritten mit Pfadprädikaten:

1. Sie werden unter Verwendung von Einschränkungen (Constraints) für die Eingabe des Programms konstruiert.
2. Sie werden verwendet, um Programmeingaben zu generieren, die dazu führen, dass die zugehörigen Pfade ausgeführt werden.

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-Ü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:

function f(uint a){

  if (a == 65) {
      // Ein Fehler ist vorhanden
  }

}

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

• 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 Path 1 wird der Solver sagen, dass der Pfad mit a = 65 erkundet werden kann. Für Path 2 kann der Solver a jeden anderen Wert als 65 geben, zum Beispiel a = 0.

Eigenschaften verifizieren

Manticore ermöglicht eine 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 Vertrag.

Betrachten Sie das folgende Beispiel:

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

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

• Pfad 1: c = a + b

Mit Manticore können Sie 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 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:

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

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 ist dies ein Beweis, dass in safe_add der Wert c immer steigen 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):

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

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

...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

Ohne zusätzliche Informationen wird Manticore den Vertrag mit neuen symbolischen Transaktionen untersuchen, bis es keine neuen Pfade im Vertrag mehr entdeckt. 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 (Coverage) 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) 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 Transaktion einen eindeutigen Testfall.

Verwenden Sie das Flag --quick-mode, wenn Sie eine schnelle Code-Untersuchung wünschen (es deaktiviert Fehlererkennungen, 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:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

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

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)

Zusammenfassung

• Sie können Benutzer- und Contract-Konten mit m.create_account (opens in a new tab) und m.solidity_create_contract (opens in a new tab) erstellen.

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:

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

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.

Zum Beispiel:

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)

Wenn die Daten symbolisch sind, wird Manticore während der Transaktionsausführung alle Funktionen des Vertrags untersuchen. Es ist hilfreich, sich die Erklärung zur Fallback-Funktion im Artikel Hands on the Ethernaut CTF (opens in a new tab) anzusehen, 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:

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

Wenn value der Transaktion nicht angegeben ist, ist der Standardwert 0.

Zusammenfassung

• Argumente einer Transaktion können konkret oder symbolisch sein.
• Eine rohe Transaktion wird alle Funktionen untersuchen.
• Funktionen können bei ihrem Namen aufgerufen werden.

Arbeitsbereich (Workspace)

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

print("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 der untersuchten Pfade.

Zusammenfassung: Ausführen unter Manticore

Wenn wir alle vorherigen Schritte zusammenfassen, erhalten wir:

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() # die Erkundung stoppen

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

Pfade mit Ausnahmen (Throwing Paths) erhalten

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

Zustandsinformationen verwenden

Jeder ausgeführte Pfad hat seinen Zustand der Blockchain. Ein Zustand ist entweder bereit (ready) oder er wird 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 Zustände, die beendet wurden
• m.all_states (opens in a new tab): alle Zustände

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

Sie können auf Zustandsinformationen zugreifen. Zum Beispiel:

• state.platform.get_balance(account.address): der Kontostand
• 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 konvertiert werden kann:

data = state.platform.transactions[0].return_data
data = 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:

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

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)

## Prüfen, ob eine Ausführung mit einem REVERT oder INVALID endet
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')

Den gesamten obigen Code finden Sie in der 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):

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

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:

from manticore.core.smtlib import Operators

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

last_return = Operators.CONCAT(256, *last_return)

Einschränkungen (Constraints)

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 Vertrag von einer symbolischen Adresse aus aufrufen und diese Adresse auf bestimmte Werte beschränken:

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)

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. Zum Beispiel wird Folgendes symbolic_value darauf beschränken, ungleich 65 zu sein, und prüfen, ob der Zustand noch machbar ist:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # Zustand ist möglich

Zusammenfassung: Einschränkungen hinzufügen

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

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

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

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