Cara menggunakan Echidna untuk menguji kontrak pintar

Instalasi

Echidna dapat diinstal melalui docker atau dengan menggunakan binari yang telah dikompilasi sebelumnya.

Echidna melalui docker

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

Perintah terakhirnya menjalankan kotak peralatan keamanan eth di dalam docker yang memiliki akses ke direktori Anda saat ini. Anda bisa mengubah file dari host Anda, dan menjalankan peralatannya pada file dari docker

Dalam docker, jalankan :

solc-select 0.5.11
cd /home/training

Binari

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

Pengantar fuzzing berbasis properti

Echidna merupakan sebuah fuzzer berbasis properti, yang kami deskripsikan dalam postingan blog kami sebelumnya (1opens in a new tab, 2opens in a new tab, 3opens in a new tab).

Fuzzing

Fuzzingopens in a new tab adalah sebuah teknik yang terkenal dalam komunitas keamanan. Teknik ini berfungsi untuk membuat lebih banyak atau lebih sedikit input secara acak untuk menemukan bug dalam program. Fuzzer bagi perangkat lunak tradisional (seperti AFLopens in a new tab atau LibFuzzeropens in a new tab) dikenal sebagai peralatan efisien untuk menemukan bug.

Di luar dari pembentukan input acak secara murni, ada banyak teknik dan strategi untuk membuat input yang baik, termasuk:

• Memperoleh umpan balik dari setiap eksekusi dan generasi pemandu yang menggunakannya. Misalnya, jika sebuah input yang baru saja dibuat menghasilkan penemuan jalur baru, ini dapat menjelaskan cara membuat input baru yang dekat dengannya.
• Menghasilkan input yang sesuai dengan batasan struktural. Misalnya, jika input Anda berisi header dengan checksum, akan masuk akal untuk mengizinkan fuzzer membuat input yang memvalidasi checksum.
• Menggunakan input yang diketahui untuk membuat input baru: jika Anda memiliki akses ke kumpulan data besar input yang valid, fuzzer Anda dapat membuat input yang baru darinya, daripada memulai generasinya dari awal. Ini biasa disebut seed.

Fuzzing berbasis properti

Echidna termasuk pada keluarga fuzzer khusus: fuzzing berbasis properti yang sangat diinspirasikan oleh QuickCheckopens in a new tab. Berlawanan dengan fuzzer klasik yang akan mencoba menemukan kesalahan, Echidna akan mencoba memecah invarian yang ditentukan oleh pengguna.

Dalam kontrak pintar, invarian adalah fungsi Solidity, yang dapat mewakili state yang salah atau tidak valid yang dapat dicapai oleh kontrak, yang mencakup:

• Kontrol akses yang salah: penyerang menjadi pemilik kontrak.
• Mesin state yang salah: token dapat ditransfer sementara kontrak dijeda.
• Aritmatika yang salah: pengguna dapat melakukan underflow terhadap saldonya dan mendapatkan token gratis yang tak terbatas.

Menguji properti dengan Echidna

Kita akan melihat cara menguji kontrak pintar dengan Echidna. Targetnya adalah kontrak pintar token.solopens in a new tab berikut ini:

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}
Tampilkan semua
Salin

Kita akan membuat asumsi bahwa token ini harus memiliki properti berikut ini:

• Siapa pun dapat memiliki maksimum 1000 token
• Token tidak dapat ditransfer (ini bukan token ERC20)

Tulis sebuah properti

Properti Echidna merupakan fungsi Solidity. Sebuah properti harus:

• Tidak memiliki argumen
• Mengembalikan true jika berhasil
• Memiliki nama yang dimulai dengan echidna

Echidna akan:

• Secara otomatis membuat transaksi arbitrari untuk menguji properti.
• Melaporkan transaksi mana pun yang menyebabkan properti mengembalikan false atau yang menghasilkan kesalahan.
• Membuang efek samping saat memanggil properti (mis. jika properti mengubah variabel state, ini akan dibuang setelah tes selesai)

Properti berikut memeriksa bahwa pemanggil tidak memiliki lebih dari 1000 token:

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

Gunakan warisan untuk memisahkan kontrak Anda dari properti Anda:

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

token.solopens in a new tab mengimplementasikan properti dan mewariskannya dari token.

Mulai sebuah kontrak

Echidna memerlukan sebuah pembangun tanpa argumen. Jika kontrak Anda memerlukan inisialisasi khusus, Anda perlu melakukannya di pembangun.

Ada beberapa alamat khusus di Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 yang memanggil pembangun.
• 0x10000, 0x20000, dan 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 yang secara acak memanggil fungsi lainnya.

Kita tidak memiliki inisialisasi khusus mana pun dalam contoh kita saat ini, akibatnya pembangun kita kosong.

Jalankan Echidna

Echidna diluncurkan dengan:

$ echidna-test contract.sol

Jika contract.sol berisi berbagai kontrak, Anda dapat menentukan target:

$ echidna-test contract.sol --contract MyContract

Ringkasan: Menguji sebuah properti

Berikut ini merangkum operasi echidna dalam contoh kita:

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

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

Echidna menemukan bahwa properti dilanggar jika backdoor dipanggil.

Menyaring fungsi untuk memanggil saat kampanye fuzzing berlangsung

Kita akan melihat cara menyaring fungsi untuk di-fuzz. Targetnya adalah kontrak pintar berikut ini:

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}
Tampilkan semua
Salin

Contoh kecil ini memaksa Echidna menemukan urutan transaksi spesifik untuk mengubah variabel state. Ini sulit bagi sebuah fuzzer (direkomendasikan untuk menggunakan peralatan eksekusi simbolis seperti Manticoreopens in a new tab). Kita dapat menjalankan Echidna untuk memverifikasi ini:

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

Menyaring fungsi

Echidna memiliki masalah dalam menemukan urutan yang benar untuk menguji kontrak ini karena dua fungsi pengaturan ulang (reset1 dan reset2) akan menetapkan semua variabel state ke false. Namun, kita dapat menggunakan fitur spesial Echidna untuk membuat daftar hitam fungsi pengaturan ulang atau membuat daftar putih hanya untuk fungsi f, g, h dan i.

Untuk membuat daftar hitam fungsi, kita dapat menggunakan file konfigurasi ini:

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

Pendekatan lainnya untuk menyaring fungsi adalah mencantumkan fungsi yang dimasukkan ke dalam daftar putih. Untuk itu, kita dapat menggunakan file konfigurasi ini:

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

• filterBlacklist bersifat true secara default.
• Penyaringan akan dilakukan berdasarkan nama saja (tanpa parameter). Jika Anda memiliki f() dan f(uint256), "f" penyaring akan memasangkan kedua fungsi tersebut.

Jalankan Echidna

Untuk menjalankan Echidna dengan file konfigutasi blacklist.yaml:

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

Echidna akan segera menemukan urutan transaksi untuk memalsukan properti.

Ringkasan: Fungsi penyaringan

Echidna dapat membuat daftar hitam atau daftar putih fungsi yang dipanggil pada saat kampanye fuzzing dengan menggunakan:

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

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

Echidna memulai kampanye fuzzing dengan membuat daftar hitam f1, f2 dan f3 atau hanya memanggil ini, berdasarkan nilai dari boolean filterBlacklist.

Bagaimana cara menguji assert Solidity dengan Echidna

Dalam tutorial pendek ini, kami akan menunjukkan bagaimana cara menggunakan Echidna untuk menguji pemeriksaan fungsi penegasan dalam kontrak. Anggaplah kita memiliki sebuah kontrak seperti ini:

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}
Tampilkan semua
Salin

Tulis sebuah penegasan

Kita ingin memastikan bahwa tmp kurang dari atau sama dengan counter setelah mengembalikan perbedaannya. Kita dapat menulis sebuah properti Echidna, tetapi kita akan perlu menyimpan nilai tmp di suatu tempat. Sebagai gantinya, kita dapat menggunakan sebuah penegasan seperti yang ini:

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}
Tampilkan semua
Salin

Jalankan Echidna

To enable the assertion failure testing, create an Echidna configuration fileopens in a new tab config.yaml:

1checkAsserts: true

Ketika kita menjalankan kontrak di Echidna, kita mendapatkan hasil yang diharapkan:

$ echidna-test assert.sol --config config.yaml
Menganalisis kontrak: assert.sol:Incrementor
assertion in inc: failed!💥
  Urutan pemanggilan, menyusut (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Tampilkan semua

Seperti yang Anda dapat lihat, Echidna melaporkan beberapa kegagalan penegasan dalam fungsi inc. Dimungkinkan menambahkan lebih dari satu penegasan per fungsi, tetapi Echidna tidak dapat mengetahui penegasan mana yang gagal.

Kapan dan bagaimana cara menggunakan penegasan

Penegasan dapat digunakan sebagai alternatif untuk properti eksplisit, secara khusus jika kondisi untuk memeriksa terkait langsung dengan penggunaan beberapa operasi f yang benar. 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
Salin

Sebaliknya, menggunakan properti eksplisit echidna akan secara acak mengeksekusi transaksi dan tidak ada cara mudah untuk menerapkannya secara persis ketika akan diperiksa. Namun, masih mungkin untuk menyelesaikan ini:

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

Namun, ada beberapa masalah:

• Gagal jika f dideklarasikan sebagai internal atau external.
• Tidak jelas argumen mana yang harus digunakan untuk memanggil f.
• Jika f melakukan pembalikan, properti akan gagal.

Secara umum, kami menyarankan mengikuti rekomendasi John Regehropens in a new tab tentang bagaimana cara menggunakan penegasan:

• Jangan memaksakan efek samping apa pun pada saat pemeriksaan penegasan dilakukan. Misalnya: assert(ChangeStateAndReturn() == 1)
• Jangan menegaskan pernyataan yang jelas. Misalnya assert(var >= 0) di mana var dideklarasikan sebagai uint.

Akhirnya, harap tidak menggunakan require ketimbang assert, karena Echidna tidak akan dapat mendeteksinya (tetapi kontraknya bagaimana pun akan melakukan pembalikan).

Ringkasan: Pemeriksaan Penegasan

Berikut ini merangkum operasi echidna dalam contoh kita:

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}
Tampilkan semua
Salin

$ 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
Tampilkan semua

Echidna menemukan bahwa penegasan dalam inc dapat gagal jika fungsi ini dipanggil beberapa kali dengan argumen yang besar.

Mengumpulkan dan memodifikasi sebuah korpus Echidna

Kita akan melihat bagaimana cara mengumpulkan dan menggunakan sebuah korpus transaksi dengan Echidna. Targetnya adalah kontrak pintar magic.solopens in a new tab berikut ini:

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}
Tampilkan semua
Salin

Contoh kecil ini memaksa Echidna menemukan nilai tertentu untuk mengubah sebuah variabel state. Ini sulit bagi sebuah fuzzer (direkomendasikan untuk menggunakan peralatan eksekusi simbolis seperti Manticoreopens in a new tab). Kita dapat menjalankan Echidna untuk memverifikasi ini:

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

Namun, kita masih dapat menggunakan Echidna untuk mengumpulkan korpus ketika menjalankan kampanye fuzzing ini.

Mengumpulkan sebuah korpus

Untuk memungkinkan pengumpulan korpus, buat sebuah direktori korpus:

$ mkdir corpus-magic

Dan file konfigurasi Echidnaopens in a new tab config.yaml:

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

Sekarang kita dapat menjalankan peralatan kita dan memeriksa korpus yang dikumpulkan:

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

Echidna masih tidak dapat menemukan nilai magic yang benar, tetapi kita dapat melihat korpus yang dikumpulkannya. Sebagai contoh, salah satu dari file ini adalah:

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]
Tampilkan semua
Salin

Jelas, input ini tidak akan memicu kegagalan dalam properti kita. Namun, dalam tahap berikutnya, kita akan melihat bagaimana cara untuk memodifikasinya untuk tujuan itu.

Membuat seed dari sebuah korpus

Echidna membutuhkan beberapa bantuan untuk menangani fungsi magic. Kita akan menyalin dan memodifikasi input agar parameter yang sesuai digunakan untuknya:

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

Kita akan memodifikasi new.txt untuk memanggil magic(42,129,333,0). Sekarang, kita dapat menjalankan Echidna kembali:

$ 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
Tampilkan semua

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

Menemukan transaksi dengan pemakaiaan gas yang tinggi

We will see how to find the transactions with high gas consumption with Echidna. Targetnya adalah kontrak pintar berikut ini:

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}
Tampilkan semua
Salin

Di sini expensive dapat memiliki pemakaian gas yang besar.

Saat ini, Echidna selalu memerlukan sebuah properti untuk melakukan pengujian: di sini echidna_test selalu mengembalikan true. Kita dapat menjalankan Echidna untuk memverifikasi ini:

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

Mengukur Pemakaian Gas

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

1estimateGas: true

Dalam contoh ini, kita juga akan mengurangi ukuran urutan transaksi untuk membuat hasilnya lebih mudah dimengerti:

1seqLen: 2
2estimateGas: true

Run Echidna

Setelah kita memiliki file konfigurasi yang telah dibuat, kita dapat menjalankan Echidna seperti ini:

$ 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
Tampilkan semua

• Gas yang diperlihatkan adalah sebuah perkiraan yang disediakan oleh HEVMopens in a new tab.

Menyaring Pemanggilan Pengurangan Gas

Tutorial tentang menyaring fungsi untuk melakukan pemanggilan pada saat kampanye fuzzing di atas menunjukkan cara menghilangkan beberapa fungsi dari pengujian Anda.
Langkah ini dapat menjadi sangat penting untuk mendapatkan sebuah perkiraan gas yang akurat. Perhatikan contoh berikut:

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}
Tampilkan semua
Salin

Jika Echidna dapat memanggil semua fungsi, fungsi ini tidak akan dengan mudah menemukan transaksi dengan harga has yang tinggi:

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
Tampilkan semua

Itu karena harganya bergantung pada ukuran addrs dan pemanggilan acak cenderung membuat array hampir kosong. Namun, memasukkan pop dan clear ke dalam daftar hitam memberikan kita hasil yang lebih baik:

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

Ringkasan: Menemukan transaksi dengan pemakaian gas yang tinggi

Echidna dapat menemukan transaksi dengan pemakaian gas yang tinggi dengan menggunakan opsi konfigurasi estimateGas:

1estimateGas: true

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

Echidna akan melaporkan urutan dengan pemakaian gas maksimum untuk setiap fungsi, setelah kampanye fuzzing selesai.

Page last update: 4 Desember 2023

popens in a new tab

nopens in a new tab

Mopens in a new tab

+7

Lihat kontributor