So verwenden Sie Echidna zum Testen von Smart Contracts

Installation

Echidna kann über Docker oder durch Verwendung des vorkompilierten Binärprogramms installiert werden.

Echidna ü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ühren Sie in Docker Folgendes aus:

solc-select 0.5.11
cd /home/training

Binär

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

Einführung in das eigenschaftsbasierte 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 traditionelle Software (wie AFL (opens in a new tab) oder LibFuzzer (opens in a new tab)) sind als effiziente Werkzeuge 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 zum Beispiel eine neu generierte Eingabe zur Entdeckung eines neuen Pfades führt, kann es sinnvoll sein, neue Eingaben in dessen Nähe zu generieren.
• Generierung der Eingabe unter Einhaltung einer strukturellen Beschränkung. Wenn Ihre Eingabe zum Beispiel 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 die Generierung von Grund auf neu zu starten. Diese werden in der Regel Seeds genannt.

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, wird Echidna versuchen, benutzerdefinierte Invarianten zu brechen.

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

• Falsche Zugriffskontrolle: Der Angreifer wurde zum Eigentümer des Vertrags.
• Falsche Statusmaschine: Die Token können übertragen werden, während der Vertrag pausiert ist.
• Falsche Arithmetik: der Benutzer kann sein Guthaben unterlaufen lassen 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}
Alles anzeigen
Kopieren

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

• Jeder kann maximal 1000 Token haben
• Der Token kann nicht übertragen werden (es ist kein ERC20-Token)

Eine Eigenschaft schreiben

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

• Kein Argument haben
• true zurückgeben, wenn es erfolgreich ist
• Der Name muss mit echidna beginnen

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 Aufrufen einer Eigenschaft verwerfen (d. h., wenn die Eigenschaft eine Zustandsvariable ändert, wird sie nach dem Test verworfen)

Die folgende Eigenschaft prüft, dass 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 Argument. Wenn Ihr Vertrag eine spezifische Initialisierung benötigt, müssen Sie dies im Konstruktor tun.

Es gibt einige spezifische Adressen in Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72, die den Konstruktor aufruft.
• 0x10000, 0x20000, und 0x00a329C0648769a73afAC7F9381e08fb43DBEA70, die 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 die Ausführung von Echidna an unserem Beispiel zusammen:

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

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Alles anzeigen

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

Dieses kleine Beispiel zwingt Echidna, eine bestimmte Sequenz von Transaktionen zu finden, um eine Zustandsvariable zu ändern. Das ist schwierig für einen Fuzzer (es wird empfohlen, ein symbolisches Ausführungswerkzeug 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! 🎉
Seed: -3684648582249875403

Filterfunktionen

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 eine schwarze Liste zu setzen oder nur die Funktionen f, g, h und i auf eine weiße Liste zu setzen.

Um Funktionen auf die schwarze Liste 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 weißen Liste 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, wird der Filter "f" auf beide Funktionen passen.

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 der Transaktionen, um die Eigenschaft zu widerlegen, fast sofort finden.

Zusammenfassung: Filterfunktionen

Echidna kann während einer Fuzzing-Kampagne entweder Funktionen auf eine schwarze oder eine weiße Liste setzen, indem es Folgendes verwendet:

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

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

Echidna startet eine Fuzzing-Kampagne, bei der f1, f2 und f3 entweder auf der schwarzen Liste stehen oder nur diese aufgerufen werden, je nach dem Wert des filterBlacklist-Booleans.

Wie man Soliditys assert mit Echidna testet

In diesem kurzen Tutorial zeigen wir, wie man Echidna zum Testen der Assertionsprüfung in Verträgen verwendet. 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}
Alles anzeigen
Kopieren

Eine Assertion schreiben

Wir wollen 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 tmp-Wert irgendwo speichern. Stattdessen könnten wir eine Assertion 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}
Alles anzeigen
Kopieren

Echidna ausführen

Um das Testen von Assertionsfehlern 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:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Alles anzeigen

Wie Sie sehen können, meldet Echidna einen Assertionsfehler in der inc-Funktion. Das Hinzufügen von mehr als einer Assertion pro Funktion ist möglich, aber Echidna kann nicht sagen, welche Assertion fehlgeschlagen ist.

Wann und wie man Assertions verwendet

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

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

Im Gegenteil, die Verwendung einer expliziten Echidna-Eigenschaft führt zu einer zufälligen Ausführung von Transaktionen, und es gibt keine einfache Möglichkeit, genau zu erzwingen, wann sie überprüft wird. Es ist immer noch möglich, diesen Workaround zu verwenden:

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 fehlschlägt, wird die Eigenschaft ebenfalls fehlschlagen.

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

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

Schließlich, bitte verwenden Sie nicht require anstelle von assert, da Echidna es nicht erkennen kann (aber der Vertrag wird trotzdem fehlschlagen).

Zusammenfassung: Assertionsprüfung

Das Folgende fasst die Ausführung von Echidna an 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}
Alles anzeigen
Kopieren

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Alles anzeigen

Echidna hat herausgefunden, dass die Assertion 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 mit Echidna einen Korpus von Transaktionen 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 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Alles anzeigen
Kopieren

Dieses kleine Beispiel zwingt Echidna, bestimmte Werte zu finden, um eine Zustandsvariable zu ändern. Das ist schwierig für einen Fuzzer (es wird empfohlen, ein symbolisches Ausführungswerkzeug 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! 🎉
Seed: 2221503356319272685

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

Einen Korpus sammeln

Um die Korpus-Sammlung zu aktivieren, erstellen Sie ein Korpus-Verzeichnis:

mkdir corpus-magic

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

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

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

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

Echidna kann immer noch nicht die richtigen magischen Werte finden, aber wir können uns den Korpus ansehen, den es gesammelt hat. Eine dieser Dateien war zum Beispiel:

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              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Alles anzeigen
Kopieren

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 Startwerten versehen

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

cp corpus/2712688662897926208.txt corpus/new.txt

Wir werden new.txt modifizieren, um magic(42,129,333,0) aufzurufen. 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)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
Alles anzeigen

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

Transaktionen mit hohem Gasverbrauch finden

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) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Alles anzeigen
Kopieren

Hier kann expensive einen hohen 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:

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

Gasverbrauch messen

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 so ausführen:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
Alles anzeigen

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

Gasreduzierende Aufrufe herausfiltern

Das Tutorial zum Filtern von Funktionen, die während einer Fuzzing-Kampagne aufgerufen werden oben zeigt, wie man einige Funktionen aus dem Test entfernt.
Dies kann entscheidend sein, um eine genaue Gasschätzung zu erhalten. Betrachte das folgende Beispiel:

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

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

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Alles anzeigen

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 schwarze Liste liefert uns jedoch viel bessere Ergebnisse:

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

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

Zusammenfassung: Finden von Transaktionen mit hohem Gasverbrauch

Echidna kann Transaktionen mit hohem Gasverbrauch finden, indem es die Konfigurationsoption estimateGas verwendet:

1estimateGas: true

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

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

Seite zuletzt aktualisiert: 21. Oktober 2025

p (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+8

Siehe Mitwirkende