Jak używać Echidny do testowania inteligentnych kontraktów

Instalacja

Echidnę można zainstalować za pomocą platformy Docker lub używając wstępnie skompilowanego pliku binarnego.

Echidna przez platformę Docker

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

Ostatnie polecenie uruchamia eth-security-toolbox w dockerze, który ma dostęp do bieżącego katalogu. Możesz zmienić pliki z hosta i uruchomić narzędzia na plikach z dockera

Wewnątrz Dockera uruchom:

solc-select 0.5.11
cd /home/training

Plik binarny

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

Wprowadzenie do testowania opartego na właściwościach (fuzzing)

Echidna to fuzzer oparty na właściwościach, co opisaliśmy w naszych poprzednich wpisach na blogu (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) to dobrze znana technika w społeczności zajmującej się bezpieczeństwem. Polega ona na generowaniu danych wejściowych, które są mniej lub bardziej losowe, w celu znalezienia błędów w programie. Fuzzery dla tradycyjnego oprogramowania (takie jak AFL (opens in a new tab) lub LibFuzzer (opens in a new tab)) są znane jako wydajne narzędzia do znajdowania błędów.

Oprócz czysto losowego generowania danych wejściowych istnieje wiele technik i strategii generowania dobrych danych wejściowych, w tym:

• Uzyskiwanie informacji zwrotnej z każdego wykonania i wykorzystywanie jej do kierowania generowaniem. Na przykład, jeśli nowo wygenerowane dane wejściowe prowadzą do odkrycia nowej ścieżki, sensowne może być wygenerowanie nowych danych wejściowych zbliżonych do nich.
• Generowanie danych wejściowych z poszanowaniem ograniczeń strukturalnych. Na przykład, jeśli dane wejściowe zawierają nagłówek z sumą kontrolną, sensowne będzie pozwolić fuzzerowi na wygenerowanie danych wejściowych weryfikujących sumę kontrolną.
• Używanie znanych danych wejściowych do generowania nowych danych wejściowych: jeśli masz dostęp do dużego zbioru prawidłowych danych wejściowych, fuzzer może generować nowe dane wejściowe na ich podstawie, zamiast rozpoczynać generowanie od zera. Są one zwykle nazywane ziarnami (seeds).

Fuzzing oparty na właściwościach

Echidna należy do specyficznej rodziny fuzzerów: fuzzingu opartego na właściwościach, mocno inspirowanego QuickCheck (opens in a new tab). W przeciwieństwie do klasycznego fuzzera, który próbuje znaleźć awarie, Echidna próbuje złamać niezmienniki zdefiniowane przez użytkownika.

W inteligentnych kontraktach niezmienniki to funkcje Solidity, które mogą reprezentować dowolny nieprawidłowy lub nieważny stan, jaki kontrakt może osiągnąć, w tym:

• Nieprawidłowa kontrola dostępu: atakujący stał się właścicielem kontraktu.
• Nieprawidłowa maszyna stanu: tokeny mogą być transferowane, gdy kontrakt jest wstrzymany.
• Nieprawidłowa arytmetyka: użytkownik może spowodować niedomiar swojego salda i uzyskać nieograniczoną liczbę darmowych tokenów.

Testowanie właściwości za pomocą Echidny

Zobaczymy, jak testować inteligentny kontrakt za pomocą Echidny. Celem jest następujący inteligentny kontrakt 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}
Pokaż wszystko
Kopiuj

Przyjmiemy założenie, że ten token musi mieć następujące właściwości:

• Każdy może mieć maksymalnie 1000 tokenów
• Token nie może być transferowany (nie jest to token ERC20)

Napisz właściwość

Właściwości Echidny to funkcje Solidity. Właściwość musi:

• Nie mieć argumentów
• Zwracać true w przypadku powodzenia
• Mieć nazwę zaczynającą się od echidna

Echidna:

• Automatycznie generuje dowolne transakcje w celu przetestowania właściwości.
• Zgłaszać wszelkie transakcje, które powodują, że właściwość zwraca false lub zgłasza błąd.
• Odrzucać efekty uboczne podczas wywoływania właściwości (tzn. jeśli właściwość zmienia zmienną stanu, jest to odrzucane po teście)

Poniższa właściwość sprawdza, czy dzwoniący nie ma więcej niż 1000 tokenów:

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

Użyj dziedziczenia, aby oddzielić swój kontrakt od właściwości:

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

token.sol (opens in a new tab) implementuje właściwość i dziedziczy po tokenie.

Inicjowanie kontraktu

Echidna potrzebuje konstruktora bez argumentów. Jeśli Twój kontrakt wymaga określonej inicjalizacji, musisz to zrobić w konstruktorze.

W Echidnie istnieją pewne specyficzne adresy:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72, który wywołuje konstruktor.
• 0x10000, 0x20000 i 0x00a329C0648769a73afAC7F9381e08fb43DBEA70, które losowo wywołują inne funkcje.

W naszym obecnym przykładzie nie potrzebujemy żadnej szczególnej inicjalizacji, w rezultacie nasz konstruktor jest pusty.

Uruchom Echidnę

Echidnę uruchamia się za pomocą:

echidna-test contract.sol

Jeśli contract.sol zawiera wiele kontraktów, możesz określić cel:

echidna-test contract.sol --contract MyContract

Podsumowanie: Testowanie właściwości

Poniżej podsumowano uruchomienie Echidny na naszym przykładzie:

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

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

Echidna odkryła, że właściwość jest naruszana, jeśli wywołana zostanie funkcja backdoor.

Filtrowanie funkcji do wywołania podczas kampanii fuzzingu

Zobaczymy, jak filtrować funkcje, które mają być poddane fuzzingowi. Celem jest następujący inteligentny kontrakt:

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}
Pokaż wszystko
Kopiuj

Ten mały przykład zmusza Echidnę do znalezienia określonej sekwencji transakcji w celu zmiany zmiennej stanu. Jest to trudne dla fuzzera (zaleca się użycie narzędzia do wykonywania symbolicznego, takiego jak Manticore (opens in a new tab)). Możemy uruchomić Echidnę, aby to zweryfikować:

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

Filtrowanie funkcji

Echidna ma problemy ze znalezieniem prawidłowej sekwencji do przetestowania tego kontraktu, ponieważ dwie funkcje resetowania (reset1 i reset2) ustawią wszystkie zmienne stanu na false. Możemy jednak użyć specjalnej funkcji Echidny, aby dodać funkcje resetowania do czarnej listy lub dodać do białej listy tylko funkcje f, g, h i i.

Aby dodać funkcje do czarnej listy, możemy użyć tego pliku konfiguracyjnego:

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

Innym podejściem do filtrowania funkcji jest utworzenie listy dozwolonych funkcji (biała lista). Aby to zrobić, możemy użyć tego pliku konfiguracyjnego:

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

• filterBlacklist jest domyślnie ustawiony na true.
• Filtrowanie odbywa się tylko po nazwie (bez parametrów). Jeśli masz f() i f(uint256), filtr "f" będzie pasował do obu funkcji.

Uruchom Echidnę

Aby uruchomić Echidnę z plikiem konfiguracyjnym blacklist.yaml:

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

Echidna niemal natychmiast znajdzie sekwencję transakcji falsyfikujących właściwość.

Podsumowanie: Filtrowanie funkcji

Echidna może dodawać funkcje do czarnej lub białej listy, które mają być wywoływane podczas kampanii fuzzingu, używając:

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

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

Echidna rozpoczyna kampanię fuzzingu, dodając f1, f2 i f3 do czarnej listy lub wywołując tylko te funkcje, w zależności od wartości logicznej filterBlacklist.

Jak testować asercję Solidity za pomocą Echidny

W tym krótkim samouczku pokażemy, jak używać Echidny do testowania sprawdzania asercji w kontraktach. Załóżmy, że mamy taki kontrakt:

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}
Pokaż wszystko
Kopiuj

Napisz asercję

Chcemy się upewnić, że tmp jest mniejsze lub równe counter po zwróceniu ich różnicy. Moglibyśmy napisać właściwość Echidny, ale musielibyśmy gdzieś przechowywać wartość tmp. Zamiast tego moglibyśmy użyć takiej asercji:

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}
Pokaż wszystko
Kopiuj

Uruchom Echidnę

Aby włączyć testowanie niepowodzenia asercji, utwórz plik konfiguracyjny Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

Gdy uruchomimy ten kontrakt w Echidnie, uzyskamy oczekiwane wyniki:

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
Pokaż wszystko

Jak widać, Echidna zgłasza błąd asercji w funkcji inc. Możliwe jest dodanie więcej niż jednej asercji na funkcję, ale Echidna nie jest w stanie stwierdzić, która asercja zawiodła.

Kiedy i jak używać asercji

Asercje mogą być używane jako alternatywa dla jawnych właściwości, zwłaszcza jeśli warunki do sprawdzenia są bezpośrednio związane z prawidłowym użyciem jakiejś operacji f. Dodanie asercji po jakimś kodzie wymusi, że sprawdzenie nastąpi natychmiast po jego wykonaniu:

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

W przeciwieństwie do tego, użycie jawnej właściwości echidna będzie losowo wykonywać transakcje i nie ma łatwego sposobu, aby wymusić, kiedy dokładnie zostanie ona sprawdzona. Nadal można zastosować to obejście:

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

Istnieją jednak pewne problemy:

• Kończy się niepowodzeniem, jeśli f jest zadeklarowane jako internal lub external.
• Nie jest jasne, jakich argumentów należy użyć do wywołania f.
• Jeśli f zostanie wycofane (revert), właściwość zakończy się niepowodzeniem.

Ogólnie rzecz biorąc, zalecamy stosowanie się do zaleceń Johna Regehra (opens in a new tab) dotyczących używania asercji:

• Nie wymuszaj żadnych efektów ubocznych podczas sprawdzania asercji. Na przykład: assert(ChangeStateAndReturn() == 1)
• Nie należy sprawdzać oczywistych stwierdzeń. Na przykład assert(var >= 0), gdzie var jest zadeklarowane jako uint.

Na koniec, proszę, nie używaj require zamiast assert, ponieważ Echidna nie będzie w stanie tego wykryć (ale kontrakt i tak zostanie wycofany).

Podsumowanie: Sprawdzanie asercji

Poniżej podsumowano uruchomienie Echidny na naszym przykładzie:

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}
Pokaż wszystko
Kopiuj

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
Pokaż wszystko

Echidna odkryła, że asercja w inc może zakończyć się niepowodzeniem, jeśli ta funkcja zostanie wywołana wielokrotnie z dużymi argumentami.

Zbieranie i modyfikowanie korpusu Echidna

Zobaczymy, jak zbierać i wykorzystywać korpus transakcji za pomocą Echidny. Celem jest następujący inteligentny kontrakt 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}
Pokaż wszystko
Kopiuj

Ten mały przykład zmusza Echidnę do znalezienia określonych wartości w celu zmiany zmiennej stanu. Jest to trudne dla fuzzera (zaleca się użycie narzędzia do wykonywania symbolicznego, takiego jak Manticore (opens in a new tab)). Możemy uruchomić Echidnę, aby to zweryfikować:

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

Możemy jednak nadal używać Echidny do zbierania korpusu podczas prowadzenia tej kampanii fuzzingu.

Zbieranie korpusu

Aby włączyć zbieranie korpusu, utwórz katalog korpusu:

mkdir corpus-magic

Oraz plik konfiguracyjny Echidna (opens in a new tab) config.yaml:

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

Teraz możemy uruchomić nasze narzędzie i sprawdzić zebrany korpus:

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

Echidna nadal nie może znaleźć prawidłowych magicznych wartości, ale możemy spojrzeć na zebrany korpus. Na przykład, jeden z tych plików to:

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]
Pokaż wszystko
Kopiuj

Oczywiście, te dane wejściowe nie spowodują niepowodzenia naszej właściwości. Jednak w następnym kroku zobaczymy, jak to zmodyfikować.

Zasilanie korpusu

Echidna potrzebuje pomocy, aby poradzić sobie z funkcją magic. Skopiujemy i zmodyfikujemy dane wejściowe, aby użyć odpowiednich parametrów:

cp corpus/2712688662897926208.txt corpus/new.txt

Zmodyfikujemy plik new.txt, aby wywołać magic(42,129,333,0). Teraz możemy ponownie uruchomić Echidnę:

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
Pokaż wszystko

Tym razem natychmiast wykryła, że właściwość jest naruszona.

Znajdowanie transakcji o wysokim zużyciu gazu

Zobaczymy, jak za pomocą Echidny znaleźć transakcje o wysokim zużyciu gazu. Celem jest następujący inteligentny kontrakt:

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}
Pokaż wszystko
Kopiuj

Tutaj expensive może mieć duże zużycie gazu.

Obecnie Echidna zawsze potrzebuje właściwości do testowania: tutaj echidna_test zawsze zwraca true. Możemy uruchomić Echidnę, aby to zweryfikować:

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

Pomiar zużycia gazu

Aby włączyć pomiar zużycia gazu za pomocą Echidny, utwórz plik konfiguracyjny config.yaml:

1estimateGas: true

W tym przykładzie zmniejszymy również rozmiar sekwencji transakcji, aby wyniki były łatwiejsze do zrozumienia:

1seqLen: 2
2estimateGas: true

Uruchom Echidnę

Po utworzeniu pliku konfiguracyjnego możemy uruchomić Echidnę w następujący sposób:

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
Pokaż wszystko

• Pokazany gaz jest szacunkiem dostarczonym przez HEVM (opens in a new tab).

Odsiewanie wywołań redukujących gaz

Powyższy samouczek na temat filtrowania funkcji do wywołania podczas kampanii fuzzingu pokazuje, jak usunąć niektóre funkcje z testowania.
Może to mieć kluczowe znaczenie dla uzyskania dokładnego oszacowania gazu. Rozważmy następujący przykład:

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}
Pokaż wszystko
Kopiuj

Jeśli Echidna może wywołać wszystkie funkcje, nie znajdzie łatwo transakcji o wysokim koszcie gazu:

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
Pokaż wszystko

Dzieje się tak, ponieważ koszt zależy od rozmiaru addrs, a losowe wywołania mają tendencję do pozostawiania tablicy prawie pustej. Jednak umieszczenie na czarnej liście pop i clear daje nam znacznie lepsze wyniki:

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

Podsumowanie: Znajdowanie transakcji o wysokim zużyciu gazu

Echidna może znaleźć transakcje o wysokim zużyciu gazu, używając opcji konfiguracji estimateGas:

1estimateGas: true

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

Po zakończeniu kampanii fuzzingu Echidna zgłosi sekwencję z maksymalnym zużyciem gazu dla każdej funkcji.

Strona ostatnio zaktualizowana: 21 października 2025

p (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+8

Zobacz współtwórców