Jak používat Echidnu k testování chytrých kontraktů

Instalace

Echidnu lze nainstalovat prostřednictvím dockeru nebo pomocí předkompilovaného binárního souboru.

Echidna prostřednictvím dockeru

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

Poslední příkaz spustí eth-security-toolbox v dockeru, který má přístup k vašemu aktuálnímu adresáři. Můžete měnit soubory z vašeho hostitele a spouštět nástroje na souborech z dockeru

Uvnitř dockeru spusťte:

solc-select 0.5.11
cd /home/training

Binární soubor

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

Úvod do fuzzingu založeného na vlastnostech

Echidna je fuzzer založený na vlastnostech, který jsme popsali v našich předchozích příspěvcích 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) je dobře známá technika v bezpečnostní komunitě. Spočívá v generování více či méně náhodných vstupů pro nalezení chyb v programu. Fuzzery pro tradiční software (jako je AFL (opens in a new tab) nebo LibFuzzer (opens in a new tab)) jsou známé jako účinné nástroje pro hledání chyb.

Kromě čistě náhodného generování vstupů existuje mnoho technik a strategií pro generování dobrých vstupů, včetně:

• Získávání zpětné vazby z každého spuštění a její použití k řízení generování. Například, pokud nově vygenerovaný vstup vede k objevení nové cesty, může mít smysl generovat nové vstupy, které jsou mu blízké.
• Generování vstupu respektujícího strukturální omezení. Například, pokud váš vstup obsahuje hlavičku s kontrolním součtem, bude mít smysl nechat fuzzer generovat vstup ověřující kontrolní součet.
• Použití známých vstupů pro generování nových vstupů: pokud máte přístup k velkému souboru dat platných vstupů, váš fuzzer může z nich generovat nové vstupy, místo aby začínal generování od nuly. Ty se obvykle nazývají seeds.

Fuzzing založený na vlastnostech

Echidna patří do specifické rodiny fuzzerů: fuzzing založený na vlastnostech, silně inspirovaný QuickCheck (opens in a new tab). Na rozdíl od klasického fuzzeru, který se snaží najít pády, se Echidna snaží narušit uživatelem definované invarianty.

V chytrých kontraktech jsou invarianty funkce v Solidity, které mohou představovat jakýkoli nesprávný nebo neplatný stav, kterého může kontrakt dosáhnout, včetně:

• Nesprávná kontrola přístupu: útočník se stal vlastníkem kontraktu.
• Nesprávný stavový automat: tokeny mohou být převáděny, i když je kontrakt pozastaven.
• Nesprávná aritmetika: uživatel může způsobit podtečení svého zůstatku a získat neomezené množství tokenů zdarma.

Testování vlastnosti s Echidnou

Podíváme se, jak testovat chytrý kontrakt s Echidnou. Cílem je následující chytrý 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}
Zobrazit vše
Kopírovat

Budeme předpokládat, že tento token musí mít následující vlastnosti:

• Každý může mít maximálně 1000 tokenů
• Token nelze převést (nejedná se o token ERC20)

Napsání vlastnosti

Vlastnosti Echidny jsou funkce v Solidity. Vlastnost musí:

• Nemít žádný argument
• Vrátit true, pokud je úspěšná
• Mít jméno začínající na echidna

Echidna bude:

• Automaticky generovat libovolné transakce pro testování vlastnosti.
• Hlásit jakékoli transakce, které vedou k tomu, že vlastnost vrátí false nebo vyhodí chybu.
• Zahodit vedlejší účinky při volání vlastnosti (tzn. pokud vlastnost změní stavovou proměnnou, je to po testu zahozeno)

Následující vlastnost kontroluje, že volající nemá více než 1000 tokenů:

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

Použijte dědičnost k oddělení vašeho kontraktu od vašich vlastností:

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

token.sol (opens in a new tab) implementuje vlastnost a dědí z tokenu.

Inicializace kontraktu

Echidna potřebuje konstruktor bez argumentu. Pokud váš kontrakt potřebuje specifickou inicializaci, musíte ji provést v konstruktoru.

V Echidně existují některé specifické adresy:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72, která volá konstruktor.
• 0x10000, 0x20000 a 0x00a329C0648769a73afAC7F9381e08fb43DBEA70, které náhodně volají ostatní funkce.

V našem aktuálním příkladu nepotřebujeme žádnou zvláštní inicializaci, proto je náš konstruktor prázdný.

Spuštění Echidny

Echidna se spouští pomocí:

echidna-test contract.sol

Pokud contract.sol obsahuje více kontraktů, můžete specifikovat cíl:

echidna-test contract.sol --contract MyContract

Shrnutí: Testování vlastnosti

Následující text shrnuje spuštění Echidny na našem příkladu:

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  }
Kopírovat

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

Echidna zjistila, že vlastnost je narušena, pokud je volána funkce backdoor.

Filtrování funkcí pro volání během fuzzingové kampaně

Ukážeme si, jak filtrovat funkce, které mají být fuzzovány. Cílem je následující chytrý 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}
Zobrazit vše
Kopírovat

Tento malý příklad nutí Echidnu najít určitou sekvenci transakcí ke změně stavové proměnné. Pro fuzzer je to obtížné (doporučuje se použít nástroj pro symbolické provádění, jako je Manticore (opens in a new tab)). Můžeme spustit Echidnu, abychom to ověřili:

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

Filtrování funkcí

Echidna má potíže s nalezením správné sekvence pro testování tohoto kontraktu, protože dvě resetovací funkce (reset1 a reset2) nastaví všechny stavové proměnné na false. Můžeme však použít speciální funkci Echidny a buď dát resetovací funkce na černou listinu, nebo na bílou listinu pouze funkce f, g, h a i.

Chcete-li dát funkce na černou listinu, můžeme použít tento konfigurační soubor:

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

Dalším přístupem k filtrování funkcí je vypsání funkcí na bílé listině. K tomu můžeme použít tento konfigurační soubor:

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

• filterBlacklist je ve výchozím nastavení true.
• Filtrování bude provedeno pouze podle jména (bez parametrů). Pokud máte f() a f(uint256), filtr "f" bude odpovídat oběma funkcím.

Spuštění Echidny

Chcete-li spustit Echidnu s konfiguračním souborem blacklist.yaml:

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

Echidna téměř okamžitě najde sekvenci transakcí, která vlastnost zneplatní.

Shrnutí: Filtrování funkcí

Echidna může během fuzzingové kampaně buď dát funkce na černou listinu, nebo na bílou listinu pomocí:

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

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

Echidna spustí fuzzingovou kampaň buď s funkcemi f1, f2 a f3 na černé listině, nebo voláním pouze těchto funkcí, podle hodnoty booleovské proměnné filterBlacklist.

Jak testovat assert v Solidity pomocí Echidny

V tomto krátkém návodu si ukážeme, jak používat Echidnu k testování kontroly tvrzení (assertions) v kontraktech. Předpokládejme, že máme kontrakt jako je tento:

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}
Zobrazit vše
Kopírovat

Napsání tvrzení (assertion)

Chceme se ujistit, že tmp je menší nebo rovno counter po vrácení jejich rozdílu. Mohli bychom napsat vlastnost pro Echidnu, ale museli bychom hodnotu tmp někam uložit. Místo toho bychom mohli použít tvrzení (assertion) jako je toto:

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}
Zobrazit vše
Kopírovat

Spuštění Echidny

Chcete-li povolit testování selhání tvrzení (assertion), vytvořte konfigurační soubor Echidny (opens in a new tab) config.yaml:

1checkAsserts: true

Když spustíme tento kontrakt v Echidně, získáme očekávané výsledky:

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
Zobrazit vše

Jak můžete vidět, Echidna hlásí selhání tvrzení (assertion) ve funkci inc. Přidání více než jednoho tvrzení (assertion) na funkci je možné, ale Echidna nedokáže říct, které tvrzení selhalo.

Kdy a jak používat tvrzení (assertions)

Tvrzení (assertions) lze použít jako alternativu k explicitním vlastnostem, zejména pokud jsou podmínky ke kontrole přímo spojeny se správným použitím nějaké operace f. Přidání tvrzení (assertions) za nějaký kód vynutí, že kontrola proběhne okamžitě po jeho vykonání:

1function f(..) public {
2    // nějaký složitý kód
3    ...
4    assert (condition);
5    ...
6}
7
Kopírovat

Naopak, použití explicitní vlastnosti echidna bude náhodně provádět transakce a neexistuje snadný způsob, jak vynutit, kdy přesně bude zkontrolována. Stále je možné použít toto řešení:

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

Existují však některé problémy:

• Selže, pokud je f deklarováno jako internal nebo external.
• Není jasné, které argumenty by se měly použít k volání f.
• Pokud se f vrátí, vlastnost selže.

Obecně doporučujeme řídit se doporučením Johna Regehra (opens in a new tab) o tom, jak používat tvrzení (assertions):

• Nevynucujte žádný vedlejší účinek během kontroly tvrzení. Například: assert(ChangeStateAndReturn() == 1)
• Netvrďte zjevné výroky. Například assert(var >= 0), kde var je deklarováno jako uint.

Nakonec, prosím, nepoužívejte require místo assert, protože Echidna to nebude schopna detekovat (ale kontrakt se stejně vrátí).

Shrnutí: Kontrola tvrzení (Assertion Checking)

Následující text shrnuje spuštění Echidny na našem příkladu:

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}
Zobrazit vše
Kopírovat

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
Zobrazit vše

Echidna zjistila, že tvrzení v inc může selhat, pokud je tato funkce volána vícekrát s velkými argumenty.

Sběr a úprava korpusu Echidna

Ukážeme si, jak sbírat a používat korpus transakcí s Echidnou. Cílem je následující chytrý 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}
Zobrazit vše
Kopírovat

Tento malý příklad nutí Echidnu najít určité hodnoty pro změnu stavové proměnné. Pro fuzzer je to obtížné (doporučuje se použít nástroj pro symbolické provádění, jako je Manticore (opens in a new tab)). Můžeme spustit Echidnu, abychom to ověřili:

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

Můžeme však stále používat Echidnu ke sběru korpusu při spouštění této fuzzingové kampaně.

Sběr korpusu

Chcete-li povolit sběr korpusu, vytvořte adresář korpusu:

mkdir corpus-magic

A konfigurační soubor Echidny (opens in a new tab) config.yaml:

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

Nyní můžeme spustit náš nástroj a zkontrolovat shromážděný korpus:

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

Echidna stále nemůže najít správné magické hodnoty, ale můžeme se podívat na korpus, který shromáždila. Například jeden z těchto souborů byl:

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]
Zobrazit vše
Kopírovat

Je zřejmé, že tento vstup nespustí selhání v naší vlastnosti. V dalším kroku si však ukážeme, jak jej pro tento účel upravit.

Nasazení korpusu

Echidna potřebuje pomoc, aby si poradila s funkcí magic. Zkopírujeme a upravíme vstup tak, aby používal vhodné parametry:

cp corpus/2712688662897926208.txt corpus/new.txt

Upravíme new.txt tak, aby volal magic(42,129,333,0). Nyní můžeme Echidnu znovu spustit:

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
Zobrazit vše

Tentokrát zjistila, že vlastnost je okamžitě narušena.

Hledání transakcí s vysokou spotřebou paliva

Ukážeme si, jak s Echidnou najít transakce s vysokou spotřebou paliva. Cílem je následující chytrý 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}
Zobrazit vše
Kopírovat

Zde může mít expensive velkou spotřebu paliva.

V současné době Echidna vždy potřebuje vlastnost k testování: zde echidna_test vždy vrací true. Můžeme spustit Echidnu, abychom to ověřili:

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

Měření spotřeby paliva

Chcete-li s Echidnou povolit spotřebu paliva, vytvořte konfigurační soubor config.yaml:

1estimateGas: true

V tomto příkladu také zmenšíme velikost sekvence transakcí, aby byly výsledky snáze pochopitelné:

1seqLen: 2
2estimateGas: true

Spuštění Echidny

Jakmile máme vytvořený konfigurační soubor, můžeme Echidnu spustit takto:

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
Zobrazit vše

• Zobrazené palivo je odhad poskytnutý HEVM (opens in a new tab).

Odfiltrování volání snižujících spotřebu paliva

Výše uvedený návod Filtrování funkcí pro volání během fuzzingové kampaně ukazuje, jak odebrat některé funkce z testování.
To může být zásadní pro získání přesného odhadu paliva. Zvažte následující příklad:

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}
Zobrazit vše
Kopírovat

Pokud může Echidna volat všechny funkce, nenajde snadno transakce s vysokými náklady na palivo:

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
Zobrazit vše

Je to proto, že náklady závisí na velikosti addrs a náhodná volání mají tendenci ponechat pole téměř prázdné. Vyloučení funkcí pop a clear nám však dává mnohem lepší výsledky:

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

Shrnutí: Hledání transakcí s vysokou spotřebou paliva

Echidna může najít transakce s vysokou spotřebou paliva pomocí konfigurační volby estimateGas:

1estimateGas: true

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

Jakmile bude fuzzingová kampaň ukončena, Echidna nahlásí sekvenci s maximální spotřebou paliva pro každou funkci.

Stránka naposledy aktualizována: 21. října 2025

p (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+8

Zobrazit přispěvatele