Wie man Echidna verwendet, um Smart Contracts zu testen

Installation

Echidna kann über Docker oder mithilfe der vorkompilierten Binärdatei installiert werden.

Echidna über Docker

docker run -it --rm -v $PWD:/src 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 für die Dateien aus dem Docker-Container heraus ausführen.

Führen Sie im Docker-Container Folgendes aus:

echidna-test /src/contract.sol

Binärdatei

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

Einführung in eigenschaftsbasiertes Fuzzing

Echidna ist ein eigenschaftsbasierter Fuzzer, den wir in unseren vorherigen Blogbeiträgen beschrieben haben (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Fuzzing

Fuzzing (opens in a new tab) ist eine bekannte Technik in der Sicherheits-Community. Sie besteht darin, mehr oder weniger zufällige Eingaben zu generieren, um Fehler im Programm zu finden. Fuzzer für herkömmliche Software (wie AFL (opens in a new tab) oder LibFuzzer (opens in a new tab)) sind als effiziente Tools zur Fehlersuche bekannt.

Über die rein zufällige Generierung von Eingaben hinaus gibt es viele Techniken und Strategien, um gute Eingaben zu generieren, darunter:

• Feedback aus jeder Ausführung einholen und die Generierung damit steuern. Wenn beispielsweise eine neu generierte Eingabe zur Entdeckung eines neuen Pfads führt, kann es sinnvoll sein, neue Eingaben in dessen Nähe zu generieren.
• Generierung der Eingabe unter Einhaltung einer strukturellen Einschränkung. Wenn Ihre Eingabe beispielsweise einen Header mit einer Prüfsumme enthält, ist es sinnvoll, den Fuzzer Eingaben generieren zu lassen, die die Prüfsumme validieren.
• Verwendung bekannter Eingaben zur Generierung neuer Eingaben: Wenn Sie Zugriff auf einen großen Datensatz gültiger Eingaben haben, kann Ihr Fuzzer daraus neue Eingaben generieren, anstatt bei der Generierung ganz von vorn zu beginnen. Diese werden normalerweise als Seeds bezeichnet.

Eigenschaftsbasiertes Fuzzing

Echidna gehört zu einer bestimmten Familie von Fuzzern: dem eigenschaftsbasierten Fuzzing, das stark von QuickCheck (opens in a new tab) inspiriert ist. Im Gegensatz zu klassischen Fuzzern, die versuchen, Abstürze zu finden, versucht Echidna, benutzerdefinierte Invarianten zu brechen.

In Smart Contracts sind Invarianten Solidity-Funktionen, die jeden falschen oder ungültigen Zustand darstellen können, den der Vertrag erreichen kann, einschließlich:

• Falsche Zugriffskontrolle: Der Angreifer wurde zum Eigentümer des Vertrags.
• Falsche Zustandsmaschine: Die Token können übertragen werden, während der Vertrag pausiert ist.
• Falsche Arithmetik: Der Benutzer kann sein Guthaben unterschreiten (Underflow) und unbegrenzt kostenlose Token erhalten.

Testen einer Eigenschaft mit Echidna

Wir werden sehen, wie man einen Smart Contract mit Echidna testet. Das Ziel ist der folgende Smart Contract token.sol (opens in a new tab):

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Alle anzeigenKopieren

Wir gehen davon aus, dass dieser Token die folgenden Eigenschaften haben muss:

• Jeder kann maximal 1000 Token besitzen
• Der Token kann nicht übertragen werden (es ist kein ERC-20-Token)

Eine Eigenschaft schreiben

Echidna-Eigenschaften sind Solidity-Funktionen. Eine Eigenschaft muss:

• Keine Argumente haben
• true zurückgeben, wenn sie erfolgreich ist
• Einen Namen haben, der mit echidna beginnt

Echidna wird:

• Automatisch beliebige Transaktionen generieren, um die Eigenschaft zu testen.
• Alle Transaktionen melden, die dazu führen, dass eine Eigenschaft false zurückgibt oder einen Fehler auslöst.
• Nebeneffekte beim Aufruf einer Eigenschaft verwerfen (d. h. wenn die Eigenschaft eine Zustandsvariable ändert, wird diese nach dem Test verworfen)

Die folgende Eigenschaft überprüft, ob der Aufrufer nicht mehr als 1000 Token hat:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}
Kopieren

Verwenden Sie Vererbung, um Ihren Vertrag von Ihren Eigenschaften zu trennen:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }
Kopieren

token.sol (opens in a new tab) implementiert die Eigenschaft und erbt vom Token.

Einen Vertrag initiieren

Echidna benötigt einen Konstruktor ohne Argumente. Wenn Ihr Vertrag eine spezifische Initialisierung benötigt, müssen Sie diese im Konstruktor vornehmen.

Es gibt einige spezifische Adressen in Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72, welche den Konstruktor aufruft.
• 0x10000, 0x20000 und 0x00a329C0648769a73afAC7F9381e08fb43DBEA70, welche zufällig die anderen Funktionen aufrufen.

In unserem aktuellen Beispiel benötigen wir keine besondere Initialisierung, daher ist unser Konstruktor leer.

Echidna ausführen

Echidna wird gestartet mit:

echidna-test contract.sol

Wenn contract.sol mehrere Verträge enthält, können Sie das Ziel angeben:

echidna-test contract.sol --contract MyContract

Zusammenfassung: Testen einer Eigenschaft

Das Folgende fasst den Lauf von Echidna in unserem Beispiel zusammen:

echidna-test token.sol

1...
2echidna_balance_under_1000: failed!💥
3  Call sequence, shrinking (2596/5000):
4    airdrop()
5    backdoor()
6
7...

Echidna hat herausgefunden, dass die Eigenschaft verletzt wird, wenn backdoor aufgerufen wird.

Filtern von Funktionen, die während einer Fuzzing-Kampagne aufgerufen werden sollen

Wir werden sehen, wie man die zu fuzzenden Funktionen filtert. Das Ziel ist der folgende Smart Contract:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24  function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Alle anzeigenKopieren

Dieses kleine Beispiel zwingt Echidna, eine bestimmte Sequenz von Transaktionen zu finden, um eine Zustandsvariable zu ändern. Dies ist für einen Fuzzer schwierig (es wird empfohlen, ein Tool zur symbolischen Ausführung wie Manticore (opens in a new tab) zu verwenden). Wir können Echidna ausführen, um dies zu überprüfen:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
...

Funktionen filtern

Echidna hat Schwierigkeiten, die richtige Sequenz zum Testen dieses Vertrags zu finden, da die beiden Reset-Funktionen (reset1 und reset2) alle Zustandsvariablen auf false setzen. Wir können jedoch eine spezielle Echidna-Funktion verwenden, um entweder die Reset-Funktion auf die Blacklist zu setzen oder nur die Funktionen f, g, h und i auf die Whitelist zu setzen.

Um Funktionen auf die Blacklist zu setzen, können wir diese Konfigurationsdatei verwenden:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

Ein anderer Ansatz zum Filtern von Funktionen besteht darin, die auf der Whitelist stehenden Funktionen aufzulisten. Dazu können wir diese Konfigurationsdatei verwenden:

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist ist standardmäßig true.
• Die Filterung erfolgt nur nach Namen (ohne Parameter). Wenn Sie f() und f(uint256) haben, stimmt der Filter "f" mit beiden Funktionen überein.

Echidna ausführen

Um Echidna mit einer Konfigurationsdatei blacklist.yaml auszuführen:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidna wird die Sequenz von Transaktionen zur Falsifizierung der Eigenschaft fast sofort finden.

Zusammenfassung: Funktionen filtern

Echidna kann Funktionen, die während einer Fuzzing-Kampagne aufgerufen werden sollen, entweder auf die Blacklist oder die Whitelist setzen, indem Folgendes verwendet wird:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

1filterBlacklist: false
2filterFunctions: ["f1", "f2", "f3"]

Echidna startet eine Fuzzing-Kampagne, bei der entweder f1, f2 und f3 auf die Blacklist gesetzt werden oder nur diese aufgerufen werden, abhängig vom Wert des booleschen Werts filterBlacklist.

Wie man Soliditys assert mit Echidna testet

In diesem kurzen Tutorial werden wir zeigen, wie man Echidna verwendet, um die Überprüfung von Zusicherungen (Assertions) in Verträgen zu testen. Nehmen wir an, wir haben einen Vertrag wie diesen:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Alle anzeigenKopieren

Eine Zusicherung (Assertion) schreiben

Wir möchten sicherstellen, dass tmp kleiner oder gleich counter ist, nachdem die Differenz zurückgegeben wurde. Wir könnten eine Echidna-Eigenschaft schreiben, aber wir müssten den Wert von tmp irgendwo speichern. Stattdessen könnten wir eine Zusicherung wie diese verwenden:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Alle anzeigenKopieren

Echidna ausführen

Um das Testen von fehlgeschlagenen Zusicherungen zu aktivieren, erstellen Sie eine Echidna-Konfigurationsdatei (opens in a new tab) config.yaml:

1checkAsserts: true

Wenn wir diesen Vertrag in Echidna ausführen, erhalten wir die erwarteten Ergebnisse:

1echidna-test assert.sol --config config.yaml
2Analyzing contract: /tmp/assert.sol:Incrementor
3assertion in inc: failed!💥
4  Call sequence, shrinking (2596/5000):
5    inc(2161168256842006112444943630224269744548897151224254110005047115547016653207)
6    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
7    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)

Wie Sie sehen können, meldet Echidna einige fehlgeschlagene Zusicherungen in der Funktion inc. Es ist möglich, mehr als eine Zusicherung pro Funktion hinzuzufügen, aber Echidna kann nicht sagen, welche Zusicherung fehlgeschlagen ist.

Wann und wie man Zusicherungen verwendet

Zusicherungen können als Alternativen zu expliziten Eigenschaften verwendet werden, insbesondere wenn die zu überprüfenden Bedingungen direkt mit der korrekten Verwendung einer Operation f zusammenhängen. Das Hinzufügen von Zusicherungen nach einem Code erzwingt, dass die Überprüfung unmittelbar nach dessen Ausführung stattfindet:

1function f(..) public {
2    // some complex code
3    ...
4    assert (condition);
5    ...
6}
Kopieren

Im Gegensatz dazu führt die Verwendung einer expliziten Echidna-Eigenschaft Transaktionen zufällig aus, und es gibt keine einfache Möglichkeit, genau zu erzwingen, wann sie überprüft wird. Es ist jedoch möglich, diesen Workaround anzuwenden:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
Kopieren

Es gibt jedoch einige Probleme:

• Es schlägt fehl, wenn f als internal oder external deklariert ist.
• Es ist unklar, welche Argumente zum Aufrufen von f verwendet werden sollen.
• Wenn f rückgängig gemacht wird (reverts), schlägt die Eigenschaft fehl.

Im Allgemeinen empfehlen wir, John Regehrs Empfehlung (opens in a new tab) zur Verwendung von Zusicherungen zu folgen:

• Erzwingen Sie keine Nebeneffekte während der Überprüfung der Zusicherung. Zum Beispiel: assert(ChangeStateAndReturn() == 1)
• Sichern Sie keine offensichtlichen Aussagen zu. Zum Beispiel assert(var >= 0), wobei var als uint deklariert ist.

Schließlich verwenden Sie bitte nicht require anstelle von assert, da Echidna dies nicht erkennen kann (der Vertrag wird jedoch trotzdem rückgängig gemacht).

Zusammenfassung: Überprüfung von Zusicherungen

Das Folgende fasst den Lauf von Echidna in unserem Beispiel zusammen:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Alle anzeigenKopieren

echidna-test assert.sol --config config.yaml

Echidna hat herausgefunden, dass die Zusicherung in inc fehlschlagen kann, wenn diese Funktion mehrmals mit großen Argumenten aufgerufen wird.

Sammeln und Modifizieren eines Echidna-Korpus

Wir werden sehen, wie man einen Korpus von Transaktionen mit Echidna sammelt und verwendet. Das Ziel ist der folgende Smart Contract magic.sol (opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == 333);
7    require(magic_4 == 0);
8    value_found = true;
9    return;
10  }
11
12  function echidna_magic_values() public returns (bool) {
13    return !value_found;
14  }
15
16}
Alle anzeigenKopieren

Dieses kleine Beispiel zwingt Echidna, bestimmte Werte zu finden, um eine Zustandsvariable zu ändern. Dies ist für einen Fuzzer schwierig (es wird empfohlen, ein Tool zur symbolischen Ausführung wie Manticore (opens in a new tab) zu verwenden). Wir können Echidna ausführen, um dies zu überprüfen:

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
...

Wir können Echidna jedoch weiterhin verwenden, um während dieser Fuzzing-Kampagne einen Korpus zu sammeln.

Einen Korpus sammeln

Um die Korpussammlung zu aktivieren, erstellen Sie ein Korpusverzeichnis:

mkdir corpus-magic

Und eine Echidna-Konfigurationsdatei (opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

Jetzt können wir unser Tool ausführen und den gesammelten Korpus überprüfen:

echidna-test magic.sol --config config.yaml

Echidna kann die richtigen magischen Werte immer noch nicht finden, aber wir können uns den gesammelten Korpus ansehen. Eine dieser Dateien war beispielsweise:

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "9372398522078111428822382693894038718080310667565819743730492509016942339959"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [
22              256,
23              "11237882436254505637692894012452665611739945802153465936579363300050342613311"
24            ],
25            "tag": "AbiUInt"
26          },
27          {
28            "contents": [
29              256,
30              "61286718360753647151574642685169272761912591497013628221301130206320371476503"
31            ],
32            "tag": "AbiUInt"
33          },
34          {
35            "contents": [
36              256,
37              "10604007310812769281948987101818773906025658755185924380939314050119356472974"
38            ],
39            "tag": "AbiUInt"
40          }
41        ]
42      ]
43    },
44    "_gasprice'": "0xa904461f1"
45  }
46]
Alle anzeigenKopieren

Offensichtlich wird diese Eingabe den Fehler in unserer Eigenschaft nicht auslösen. Im nächsten Schritt werden wir jedoch sehen, wie wir sie dafür modifizieren können.

Einen Korpus mit Seeds versehen

Echidna braucht etwas Hilfe, um mit der Funktion magic umzugehen. Wir werden die Eingabe kopieren und modifizieren, um geeignete Parameter dafür zu verwenden:

cp corpus-magic/coverage/2712688662897926208.txt corpus-magic/coverage/new.txt

Wir werden new.txt so modifizieren, dass magic(42,129,333,0) aufgerufen wird. Jetzt können wir Echidna erneut ausführen:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)

Dieses Mal wurde sofort festgestellt, dass die Eigenschaft verletzt ist.

Finden von Transaktionen mit hohem Gasverbrauch

Wir werden sehen, wie man mit Echidna die Transaktionen mit hohem Gasverbrauch findet. Das Ziel ist der folgende Smart Contract:

1contract C {
2  uint state;
3
4  function expensive(uint8 times) public {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function echidna_test() public returns (bool) {
10    return true;
11  }
12
13}
Alle anzeigenKopieren

Hier kann expensive einen großen Gasverbrauch haben.

Derzeit benötigt Echidna immer eine Eigenschaft zum Testen: Hier gibt echidna_test immer true zurück. Wir können Echidna ausführen, um dies zu überprüfen:

echidna-test gas.sol
...
echidna_test: passed! 🎉
...

Messung des Gasverbrauchs

Um den Gasverbrauch mit Echidna zu aktivieren, erstellen Sie eine Konfigurationsdatei config.yaml:

1estimateGas: true

In diesem Beispiel werden wir auch die Größe der Transaktionssequenz reduzieren, um die Ergebnisse leichter verständlich zu machen:

1seqLen: 2
2estimateGas: true

Echidna ausführen

Sobald wir die Konfigurationsdatei erstellt haben, können wir Echidna wie folgt ausführen:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉

fuzzing time: 2.73s

C.expensive(uint8) with gas 5463708:
  expensive(255)
  expensive(255)
Alle anzeigen

• Das angezeigte Gas ist eine Schätzung, die von HEVM (opens in a new tab) bereitgestellt wird.

Herausfiltern von gasreduzierenden Aufrufen

Das obige Tutorial zum Filtern von Funktionen, die während einer Fuzzing-Kampagne aufgerufen werden sollen, zeigt, wie Sie einige Funktionen aus Ihren Tests entfernen können.
Dies kann entscheidend sein, um eine genaue Gasschätzung zu erhalten. Betrachten Sie das folgende Beispiel:

1contract C {
2  address[] addrs;
3
4  function push(address a) public {
5    addrs.push(a);
6  }
7
8  function pop() public {
9    addrs.pop();
10  }
11
12  function clear() public{
13    addrs.length = 0;
14  }
15
16  function check() public{
17    for(uint256 i = 0; i < addrs.length; i++)
18      for(uint256 j = i+1; j < addrs.length; j++)
19        if (addrs[i] == addrs[j])
20          addrs[j] = address(0x0);
21  }
22
23  function echidna_test() public returns (bool) {
24      return true;
25  }
26}
Alle anzeigenKopieren

Wenn Echidna alle Funktionen aufrufen kann, wird es nicht leicht Transaktionen mit hohen Gaskosten finden:

1C.check() with gas 8001:
2  push(0x0)
3  check()

Das liegt daran, dass die Kosten von der Größe von addrs abhängen und zufällige Aufrufe dazu neigen, das Array fast leer zu lassen. Das Setzen von pop und clear auf die Blacklist liefert uns jedoch viel bessere Ergebnisse:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1C.check() with gas 1490968:
2  push(0x0)
3  push(0x0)
4  push(0x0)
5  push(0x0)
6  push(0x0)
7  push(0x0)
8  push(0x0)
9  push(0x0)
10  push(0x0)
11  push(0x0)
12  check()
Alle anzeigen

Zusammenfassung: Finden von Transaktionen mit hohem Gasverbrauch

Echidna kann Transaktionen mit hohem Gasverbrauch mithilfe der Konfigurationsoption estimateGas finden:

1estimateGas: true

echidna-test contract.sol --config config.yaml

Echidna meldet nach Abschluss der Fuzzing-Kampagne für jede Funktion eine Sequenz mit dem maximalen Gasverbrauch.

Letzte Aktualisierung der Seite: 3. März 2026

m (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+10

Mitwirkende ansehen