Cara menggunakan Echidna untuk menguji kontrak pintar

Instalasi

Echidna dapat diinstal melalui docker atau menggunakan biner 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 terakhir menjalankan eth-security-toolbox di dalam docker yang memiliki akses ke direktori Anda saat ini. Anda dapat mengubah file dari host Anda, dan menjalankan alat pada file dari docker

Di dalam docker, jalankan:

solc-select 0.5.11
cd /home/training

Biner

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

Pengantar fuzzing berbasis properti

Echidna adalah fuzzer berbasis properti, yang telah kami jelaskan di postingan blog kami sebelumnya (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) adalah teknik yang terkenal di komunitas keamanan. Teknik ini terdiri dari menghasilkan input yang kurang lebih acak untuk menemukan bug dalam program. Fuzzer untuk perangkat lunak tradisional (seperti AFL (opens in a new tab) atau LibFuzzer (opens in a new tab)) dikenal sebagai alat yang efisien untuk menemukan bug.

Selain pembuatan input yang murni acak, ada banyak teknik dan strategi untuk menghasilkan input yang baik, termasuk:

• Mendapatkan umpan balik dari setiap eksekusi dan memandu pembuatan menggunakan umpan balik tersebut. Misalnya, jika input yang baru dibuat mengarah pada penemuan jalur baru, masuk akal untuk membuat input baru yang dekat dengannya.
• Menghasilkan input dengan memperhatikan batasan struktural. Misalnya, jika input Anda berisi header dengan checksum, masuk akal untuk membiarkan fuzzer menghasilkan input yang memvalidasi checksum tersebut.
• Menggunakan input yang diketahui untuk menghasilkan input baru: jika Anda memiliki akses ke kumpulan data besar dari input yang valid, fuzzer Anda dapat menghasilkan input baru dari data tersebut, daripada memulai pembuatannya dari awal. Ini biasanya disebut seed.

Fuzzing berbasis properti

Echidna termasuk dalam keluarga fuzzer tertentu: fuzzing berbasis properti yang sangat terinspirasi oleh QuickCheck (opens in a new tab). Berbeda dengan fuzzer klasik yang akan mencoba menemukan kerusakan (crash), Echidna akan mencoba memecahkan invarian yang ditentukan pengguna.

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

• Kontrol akses yang salah: penyerang menjadi pemilik kontrak.
• Mesin status yang salah: token dapat ditransfer saat kontrak dijeda.
• Aritmatika yang salah: pengguna dapat melakukan underflow pada saldonya dan mendapatkan token gratis tanpa batas.

Menguji properti dengan Echidna

Kita akan melihat cara menguji kontrak pintar dengan Echidna. Targetnya adalah kontrak pintar berikut 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}
Tampilkan semua
Salin

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

• Siapa pun dapat memiliki maksimal 1000 token
• Token tidak dapat ditransfer (ini bukan token ERC-20)

Menulis properti

Properti Echidna adalah fungsi Solidity. Sebuah properti harus:

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

Echidna akan:

• Secara otomatis menghasilkan transaksi arbitrer untuk menguji properti.
• Melaporkan setiap transaksi yang menyebabkan properti mengembalikan false atau memunculkan kesalahan.
• Membuang efek samping saat memanggil properti (yaitu, jika properti mengubah variabel status, itu akan dibuang setelah pengujian)

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 pewarisan 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.sol (opens in a new tab) mengimplementasikan properti dan mewarisi dari token.

Memulai kontrak

Echidna membutuhkan konstruktor tanpa argumen. Jika kontrak Anda memerlukan inisialisasi tertentu, Anda harus melakukannya di konstruktor.

Ada beberapa alamat tertentu di Echidna:

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

Kita tidak memerlukan inisialisasi khusus dalam contoh kita saat ini, sebagai hasilnya konstruktor kita kosong.

Menjalankan Echidna

Echidna diluncurkan dengan:

echidna-test contract.sol

Jika contract.sol berisi beberapa kontrak, Anda dapat menentukan targetnya:

echidna-test contract.sol --contract MyContract

Ringkasan: Menguji properti

Berikut ini merangkum jalannya echidna pada 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.

Memfilter fungsi untuk dipanggil selama kampanye fuzzing

Kita akan melihat cara memfilter fungsi yang akan di-fuzz. Targetnya adalah kontrak pintar berikut:

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 untuk menemukan urutan transaksi tertentu untuk mengubah variabel status. Ini sulit bagi fuzzer (disarankan untuk menggunakan alat eksekusi simbolik seperti Manticore (opens in a new tab)). Kita dapat menjalankan Echidna untuk memverifikasi ini:

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

Memfilter fungsi

Echidna kesulitan menemukan urutan yang benar untuk menguji kontrak ini karena dua fungsi reset (reset1 dan reset2) akan mengatur semua variabel status menjadi false. Namun, kita dapat menggunakan fitur khusus Echidna untuk memasukkan fungsi reset ke daftar hitam (blacklist) atau hanya memasukkan fungsi f, g, h, dan i ke daftar putih (whitelist).

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

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

Pendekatan lain untuk memfilter fungsi adalah dengan membuat daftar fungsi yang masuk daftar putih. Untuk melakukannya, kita dapat menggunakan file konfigurasi ini:

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

• filterBlacklist bernilai true secara default.
• Pemfilteran akan dilakukan berdasarkan nama saja (tanpa parameter). Jika Anda memiliki f() dan f(uint256), filter "f" akan cocok dengan kedua fungsi tersebut.

Menjalankan Echidna

Untuk menjalankan Echidna dengan file konfigurasi blacklist.yaml:

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

Echidna akan menemukan urutan transaksi untuk memalsukan properti hampir seketika.

Ringkasan: Memfilter fungsi

Echidna dapat memasukkan fungsi ke daftar hitam atau daftar putih untuk dipanggil selama kampanye fuzzing menggunakan:

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

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

Echidna memulai kampanye fuzzing dengan memasukkan f1, f2, dan f3 ke daftar hitam atau hanya memanggil fungsi-fungsi ini, sesuai dengan nilai boolean filterBlacklist.

Cara menguji assert Solidity dengan Echidna

Dalam tutorial singkat ini, kita akan menunjukkan cara menggunakan Echidna untuk menguji pemeriksaan asersi dalam kontrak. Misalkan kita memiliki 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 // tmp <= counter
8    return (counter - tmp);
9  }
10}
Tampilkan semua
Salin

Menulis asersi

Kita ingin memastikan bahwa tmp kurang dari atau sama dengan counter setelah mengembalikan selisihnya. Kita bisa menulis properti Echidna, tetapi kita perlu menyimpan nilai tmp di suatu tempat. Sebagai gantinya, kita bisa menggunakan asersi 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    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Tampilkan semua
Salin

Menjalankan Echidna

Untuk mengaktifkan pengujian kegagalan asersi, buat file konfigurasi Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

Saat kita menjalankan kontrak ini di Echidna, kita mendapatkan hasil yang diharapkan:

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

Seperti yang Anda lihat, Echidna melaporkan beberapa kegagalan asersi dalam fungsi inc. Menambahkan lebih dari satu asersi per fungsi dimungkinkan, tetapi Echidna tidak dapat memberi tahu asersi mana yang gagal.

Kapan dan bagaimana menggunakan asersi

Asersi dapat digunakan sebagai alternatif untuk properti eksplisit, terutama jika kondisi yang akan diperiksa terkait langsung dengan penggunaan yang benar dari beberapa operasi f. Menambahkan asersi setelah beberapa kode akan memastikan bahwa pemeriksaan akan terjadi segera setelah dieksekusi:

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

Sebaliknya, menggunakan properti echidna eksplisit akan mengeksekusi transaksi secara acak dan tidak ada cara mudah untuk memastikan kapan tepatnya itu akan diperiksa. Masih mungkin untuk melakukan solusi ini:

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

Namun, ada beberapa masalah:

• Ini gagal jika f dideklarasikan sebagai internal atau external.
• Tidak jelas argumen mana yang harus digunakan untuk memanggil f.
• Jika f dikembalikan (revert), properti akan gagal.

Secara umum, kami menyarankan untuk mengikuti rekomendasi John Regehr (opens in a new tab) tentang cara menggunakan asersi:

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

Terakhir, tolong jangan gunakan require sebagai pengganti assert, karena Echidna tidak akan dapat mendeteksinya (tetapi kontrak akan tetap dikembalikan).

Ringkasan: Pemeriksaan Asersi

Berikut ini merangkum jalannya echidna pada 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 asersi dalam inc dapat gagal jika fungsi ini dipanggil beberapa kali dengan argumen yang besar.

Mengumpulkan dan memodifikasi korpus Echidna

Kita akan melihat cara mengumpulkan dan menggunakan korpus transaksi dengan Echidna. Targetnya adalah kontrak pintar berikut 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}
Tampilkan semua
Salin

Contoh kecil ini memaksa Echidna untuk menemukan nilai tertentu untuk mengubah variabel status. Ini sulit bagi fuzzer (disarankan untuk menggunakan alat eksekusi simbolik seperti Manticore (opens 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 saat menjalankan kampanye fuzzing ini.

Mengumpulkan korpus

Untuk mengaktifkan pengumpulan korpus, buat direktori korpus:

mkdir corpus-magic

Dan file konfigurasi Echidna (opens in a new tab) config.yaml:

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

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

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

Echidna masih tidak dapat menemukan nilai ajaib yang benar, tetapi kita dapat melihat korpus yang dikumpulkannya. Misalnya, salah satu 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 di properti kita. Namun, pada langkah berikutnya, kita akan melihat cara memodifikasinya untuk itu.

Menyemai korpus

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

cp corpus/2712688662897926208.txt corpus/new.txt

Kita akan memodifikasi new.txt untuk memanggil magic(42,129,333,0). Sekarang, kita dapat menjalankan ulang 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
Tampilkan semua

Kali ini, ia menemukan bahwa properti tersebut segera dilanggar.

Menemukan transaksi dengan konsumsi gas tinggi

Kita akan melihat cara menemukan transaksi dengan konsumsi gas tinggi dengan Echidna. Targetnya adalah kontrak pintar berikut:

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 konsumsi gas yang besar.

Saat ini, Echidna selalu membutuhkan properti untuk diuji: di sini echidna_test selalu mengembalikan true. Kita dapat menjalankan Echidna untuk memverifikasi ini:

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

Mengukur Konsumsi Gas

Untuk mengaktifkan konsumsi gas dengan Echidna, buat file konfigurasi config.yaml:

1estimateGas: true

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

1seqLen: 2
2estimateGas: true

Menjalankan Echidna

Setelah kita membuat file konfigurasi, 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 ditampilkan adalah estimasi yang diberikan oleh HEVM (opens in a new tab).

Memfilter Panggilan yang Mengurangi Gas

Tutorial tentang memfilter fungsi untuk dipanggil selama kampanye fuzzing di atas menunjukkan cara menghapus beberapa fungsi dari pengujian Anda.
Ini bisa sangat penting untuk mendapatkan estimasi gas yang akurat. Pertimbangkan 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, ia tidak akan mudah menemukan transaksi dengan biaya gas tinggi:

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

Itu karena biayanya bergantung pada ukuran addrs dan panggilan acak cenderung membuat array hampir kosong. Namun, memasukkan pop dan clear ke daftar hitam memberi kita hasil yang jauh lebih baik:

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

Ringkasan: Menemukan transaksi dengan konsumsi gas tinggi

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

1estimateGas: true

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

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

Pembaruan terakhir halaman: 3 Maret 2026

m (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+10

Lihat kontributor