Cum se folosește Echidna pentru a testa contracte inteligente

Instalare

Echidna poate fi instalat prin docker sau utilizând pachetul binar pre-compilat.

Echidna prin docker

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

Ultima comandă rulează „eth-security-toolbox” într-un docker care are acces la directorul dvs. curent. Puteți modifica fișierele de pe gazda dvs. și puteți rula instrumentele pe fișierele din docker

În interiorul docker-ului, executați:

solc-select 0.5.11
cd /home/training

Sursa binară

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

Introducere despre fuzzing-ul bazat pe proprietăți

Echidna este un fuzzer bazat pe proprietăți, așa cum am descris în articolele noastre anterioare de pe blog (1(opens in a new tab), 2(opens in a new tab), 3(opens in a new tab)).

Fuzzing

Fuzzing-ul(opens in a new tab) este o tehnică binecunoscută în comunitatea de securitate. Aceasta constă în generarea de date de intrare mai mult sau mai puțin aleatorii pentru a găsi bug-uri în program. Se știe că fuzzer-ii pentru software-uri tradiționale (cum ar fi AFL(opens in a new tab) sau LibFuzzer(opens in a new tab)) sunt instrumente eficiente pentru a găsi bug-uri.

În afară de generarea pur aleatorie a datelor de intrare, există numeroase tehnici și strategii pentru a genera date bune de intrare, printre care se numără:

• Obținerea feedback-ului de la fiecare execuție și orientarea generării cu ajutorul acestuia. De exemplu, dacă datele de intrare nou generate conduc la descoperirea unei noi căi, pare normal să fie generate noi date de intrare apropiate de acestea.
• Generarea datelor de intrare respectând o obligație structurală. De exemplu, dacă datele dvs. de intrare conțin un antet cu o sumă de control, va fi logic să lăsați fuzzer-ul să genereze date de intrare care validează suma de control.
• Utilizarea datelor de intrare cunoscute pentru a genera noi date de intrare: dacă aveți acces la un set mare de date de intrare valide, fuzzer-ul dvs. poate genera noi date de intrare din acestea, în loc să înceapă generarea acestora de la zero. Acestea se numesc de regulă seeds.

Fuzzing-ul bazat pe proprietăți

Echidna aparține unei familii specifice de fuzzer-i: fuzzing-ul bazat pe proprietăți inspirat puternic de QuickCheck(opens in a new tab). Spre deosebire de fuzzer-ii clasici, care încearcă să găsească erori, Echidna încearcă să spargă invarianții definiți de utilizator.

În contractele inteligente, invarianții sunt funcții Solidity care pot reprezenta orice stare incorectă sau nevalidă pe care o poate atinge un contract, inclusiv:

• Controlul incorect al accesului: atacatorul a devenit proprietarul contractului.
• Mașină de stare incorectă: tokenurile pot fi transferate în timp ce contractul este în pauză.
• Aritmetică incorectă: utilizatorul, printr-un „underflow” al soldului său, poate obține un număr nelimitat de tokenuri gratuite.

Testarea unei proprietăți cu Echidna

Vom vedea cum să testăm un contract inteligent cu Echidna. Obiectivul este următorul contract inteligent 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}
Afișează tot
 Copiați

Vom presupune că acest token trebuie să aibă următoarele proprietăți:

• Oricine poate avea cel mult 1000 de tokenuri
• Tokenul nu poate fi transferat (nu este un token ERC20)

Scrieți o proprietate

Proprietățile Echidna sunt funcții Solidity. O proprietate trebuie să:

• nu aibă niciun argument
• răspundă prin true dacă are succes
• aibă un nume care să înceapă cu echidna

Echidna va face următoarele:

• va genera automat tranzacții arbitrare pentru a testa proprietatea.
• va raporta orice tranzacție care face ca o proprietate să răspundă prin false sau să genereze o eroare.
• va elimina efectul secundar atunci când apelează o proprietate (adică, dacă proprietatea modifică o variabilă de stare, aceasta este eliminată după test)

Următoarea proprietate verifică dacă apelantul nu are mai mult de 1000 de tokenuri:

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

Utilizați moștenirea („inheritance”) pentru a vă separa contractul de proprietăți:

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

token.sol(opens in a new tab) implementează proprietatea și moștenește de la token.

Inițiați un contract

Echidna are nevoie de un constructor fără argument. În cazul în care contractul dvs. are nevoie de o inițializare anume, trebuie să o faceți în cadrul constructorului.

Există câteva adrese specifice în Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 care apelează constructorul.
• 0x10000, 0x20000 și 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 care apelează aleatoriu celelalte funcții.

Nu avem nevoie de nicio inițializare specială în exemplul nostru actual, de aceea constructorul nostru este gol.

Executați Echidna

Echidna se lansează cu:

$ echidna-test contract.sol

În cazul în care „contract.sol” conține mai multe contracte, puteți specifica ținta:

$ echidna-test contract.sol --contract MyContract

Rezumat: testarea unei proprietăți

Ceea ce urmează sintetizează cum se execută Echidna în exemplul nostru:

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  }
 Copiați

$ echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Afișează tot

Echidna a constatat că proprietatea este încălcată dacă se apelează funcția backdoor.

Filtrarea funcțiilor care trebuie apelate în timpul unei campanii de fuzzing

Vom vedea cum să filtrăm funcțiile care urmează să fie fuzzate. Obiectivul este următorul contract inteligent:

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}
Afișează tot
 Copiați

Acest mic exemplu forțează Echidna să găsească o anumită secvență de tranzacții pentru a modifica o variabilă de stare. Acest lucru este dificil pentru un fuzzer (se recomandă utilizarea unui instrument simbolic de execuție precum Manticore(opens in a new tab)). Pentru a verifica aceasta, putem executa Echidna:

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

Funcții de filtrare

Este dificil pentru Echidna să găsească secvența corectă pentru a testa acest contract, pentru că cele două funcții de resetare (reset1 și reset2) vor configura toate variabilele de stare ca false. Totuși, putem utiliza o funcție specială Echidna fie pentru a pune pe lista neagră funcția de resetare, fie pentru a pune pe lista albă doar funcțiile f, g, h și i.

Pentru a pune funcțiile pe lista neagră, putem folosi acest fișier de configurare:

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

O altă abordare pentru filtrarea funcțiilor este să listăm funcțiile de pe lista albă. Pentru a face aceasta, putem utiliza acest fișier de configurare:

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

• filterBlacklist este true în mod implicit.
• Filtrarea va fi efectuată numai după nume (fără parametri). Dacă aveți f() și f(uint256), filtrul ”f” va marca ambele funcții ca fiind corespunzătoare.

Executați Echidna

Pentru a executa Echidna cu un fișier de configurare blacklist.yaml:

$ echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!
  Secvența de apelare:
    f(12)
    g(8)
    h(42)
    i()

Echidna va găsi secvența de tranzacții de falsificare a proprietății aproape imediat.

Rezumat: Funcții de filtrare

Echidna poate pune pe lista neagră sau pe lista albă funcțiile care trebuie apelate în timpul unei campanii de fuzzing folosind:

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

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

Echidna pornește o campanie de fuzzing fie punând pe lista neagră f1, f2 și f3, fie apelându-le numai pe acestea, în funcție de valoarea booleanului filterBlacklist.

Cum să testați aserțiunea Solidity cu Echidna

În acest scurt tutorial vom arăta cum se utilizează Echidna pentru a testa verificarea aserțiunilor în contracte. Să presupunem că avem un contract ca acesta:

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}
Afișează tot
 Copiați

Scrieți o aserțiune

Vrem să ne asigurăm că tmp este mai mic sau egal cu counter după ce a răspuns prin diferența acestora. Am putea scrie o proprietate Echidna, dar va trebui să stocăm undeva această valoare tmp. În schimb, am putea folosi o afirmație ca aceasta:

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}
Afișează tot
 Copiați

Executați Echidna

To enable the assertion failure testing, create an Echidna configuration file(opens in a new tab) config.yaml:

1checkAsserts: true

Când executăm acest contract în Echidna, obținem rezultatele așteptate:

$ echidna-test assert.sol --config config.yaml
Analizarea contractului: assert.sol:Incrementor
assertion in inc: failed!
  Secvență de apeluri, micșorarea (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Afișează tot

După cum puteți vedea, Echidna raportează unele eșecuri de aserțiune în funcția inc. Este posibilă adăugarea mai multor aserțiuni pe funcție, dar Echidna nu poate determina care aserțiune a eșuat.

Când și cum se utilizează aserțiunile

Aserțiunile pot fi utilizate ca alternative la proprietățile explicite, mai ales atunci când condițiile de verificat sunt direct legate de utilizarea corectă a unei operații f. Adding assertions after some code will enforce that the check will happen immediately after it was executed:

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

Dimpotrivă, dacă se utilizează o proprietate Echidna explicită, tranzacțiile se vor executa aleatoriu și nu este ușor de a stabili momentul când se va efectua obligatoriu verificarea. Puteți totusi utiliza această soluție:

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

Cu toate acestea, există unele probleme:

• Eșuează dacă f este declarat ca fiind internal sau external.
• Nu este prea clar ce argumente ar trebui utilizate pentru a apela f.
• Dacă se inversează f, proprietatea va eșua.

În general, vă recomandăm să urmați recomandarea lui John Regehr(opens in a new tab) despre modul cum să utilizați aserțiunile:

• Nu impuneți niciun efect secundar în timpul verificării aserțiunilor. De exemplu: assert(ChangeStateAndReturn() == 1)
• Nu faceți aserțiuni evidente. De exemplu, assert(var >= 0) în cazul în care var este declarat ca uint.

În cele din urmă, vă rugăm să nu utilizați require în loc de assert, deoarece Echidna nu va putea detecta acest lucru (dar contractul se va inversa oricum).

Rezumat: verificarea aserțiunilor

Ceea ce urmează sintetizează cum se execută Echidna în exemplul nostru:

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}
Afișează tot
 Copiați

$ 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
Afișează tot

Echidna a constatat că aserțiunea din inc poate eșua dacă această funcție este apelată de mai multe ori cu argumente mari.

Colectarea și modificarea unui corpus Echidna

Vom vedea cum putem colecta și utiliza un corpus de tranzacții cu Echidna. Obiectivul este următorul contract inteligent 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}
Afișează tot
 Copiați

Acest mic exemplu forțează Echidna să găsească anumite valori pentru a modifica o variabilă de stare. Acest lucru este dificil pentru un fuzzer (se recomandă utilizarea unui instrument simbolic de execuție precum Manticore(opens in a new tab)). Pentru a verifica aceasta, putem executa Echidna:

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

Cu toate acestea, putem folosi în continuare Echidna pentru a colecta corpus atunci când executăm această campanie de fuzzing.

Colectarea unui corpus

Pentru a activa colectarea unui corpus, creați un director corpus:

$ mkdir corpus-magic

Și un fișier de configurare Echidna(opens in a new tab) config.yaml:

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

Acum putem să rulăm instrumentul nostru și să verificăm corpusul colectat:

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

Echidna tot nu poate găsi valorile „magic” corecte, dar ne putem uita la corpusul pe care l-a colectat. De pildă, unul dintre aceste fișiere era:

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]
Afișează tot
 Copiați

Este evident că aceste date de intrare nu vor declanșa eșecul în proprietatea noastră. Totuși, vom vedea în etapa următoare cum putem să o modificăm în acest sens.

Adăugarea de surse la un corpus

Echidna are nevoie de puțin ajutor pentru a se ocupa de funcția magic. Vom copia și vom modifica datele de intrare ca să utilizăm parametri adecvați pentru aceasta:

$ cp corpus/2712688662897926208.txt corpus/new.txt

Vom modifica new.txt pentru a apela magic(42,129,333,0). Acum putem executa din nou Echidna:

$ 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
Afișează tot

This time, it found that the property is violated immediately.

Găsirea tranzacțiilor cu un consum ridicat de gaz

We will see how to find the transactions with high gas consumption with Echidna. Obiectivul este următorul contract inteligent:

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}
Afișează tot
 Copiați

Aici expensive poate avea un consum mare de gaz.

Actualmente Echidna are totdeauna nevoie să testeze o proprietate: aici echidna_test răspunde întotdeauna prin true. Pentru a verifica aceasta, putem executa Echidna:

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

Măsurarea consumului de gaz

To enable the gas consumption with Echidna, create a configuration file config.yaml:

1estimateGas: true

În acest exemplu vom și reduce dimensiunea secvenței de tranzacții pentru a facilita înțelegerea rezultatelor:

1seqLen: 2
2estimateGas: true

Run Echidna

După ce am creat fișierul de configurare, putem rula Echidna în felul următor:

$ 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
Afișează tot

• Gazul afișat este o estimare furnizată de HEVM(opens in a new tab).

Filtrarea apelurilor de reducere a gazului

Tutorialul privind funcțiile de filtrare care trebuie apelate în timpul unei campanii de fuzzing de mai sus arată cum să eliminați unele funcții din testele dvs.
Acest lucru poate fi esențial pentru a obține o estimare precisă a gazului. Să considerăm următorul exemplu:

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}
Afișează tot
 Copiați

Dacă Echidna poate apela toate funcțiile, nu va găsi cu ușurință tranzacțiile cu un cost ridicat al gazului:

1$ echidna-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
Afișează tot

Aceasta deoarece costul depinde de mărimea addrs și apelurile aleatorii tind să lase matricea aproape goală. Cu toate acestea, dacă punem pe lista neagră funcțiile pop și clear, obținem rezultate mult mai bune:

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

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

Rezumat: găsirea tranzacțiilor cu un consum ridicat de gaz

Echidna poate găsi tranzacțiile cu un consum ridicat de gaz prin utilizarea opțiunii de configurare estimateGas:

1estimateGas: true

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

Echidna va raporta o secvență cu consumul maxim de gaz pentru fiecare funcție odată ce s-a încheiat campania de fuzzing.