Cara menggunakan Manticore untuk menemukan bug dalam kontrak pintar

Tujuan tutorial ini adalah menunjukkan cara menggunakan Manticore untuk menemukan bug dalam kontrak pintar secara otomatis.

Instalasi

Manticore memerlukan versi >= python 3.6. Itu bisa diinstal melalui pip atau docker.

Manticore 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/trufflecon/

Manticore melalui pip

pip3 install --user manticore

solc 0.5.11 disarankan untuk ini.

Menjalankan skrip

Untuk menjalankan skrip python dengan python 3:

python3 script.py

Pengantar eksekusi simbolis dinamis

Eksekusi Simbolis Dinamis Secara Singkat

Eksekusi simbolis dinamis (DSE) adalah teknik analisis program yang menjelajah ruang state dengan kesadaran semantik tingkat tinggi. Teknik ini didasarkan pada penemuan "jalur program", yang direpresentasikan sebagai formula matematika yang disebut predikat jalur. Secara konsep, teknik ini beroperasi pada predikat jalur dalam dua langkah:

1. Predikat dibuat menggunakan batasan pada input program.
2. Predikat dibuat untuk menghasilkan input program yang akan menyebabkan eksekusi jalur yang terkait.

Pendekatan ini tidak menghasilkan false positive, dalam arti semua state program teridentifikasi bisa dipicu saat eksekusi konkretnya. Sebagai contoh, jika analisis menemukan sebuah integer overflow, ini dipastikan dapat dibuat kembali.

Contoh Predikat Jalur

Untuk mendapatkan wawasan tentang cara kerja DSE, perhatikan contoh berikut:

1function f(uint a){
2
3  if (a == 65) {
4      // Satu bug ditemukan
5  }
6
7}
 Salin

Karena f() berisi dua jalur, DSE akan membangun dua predikat jalur berbeda:

• Jalur 1: a == 65
• Jalur 2: Not (a == 65)

Setiap predikat jalur adalah formula matematika yang bisa diberikan ke solver SMT(opens in a new tab), yang akan mencoba menyelesaikan persamaannya. Untuk Jalur 1, solver akan berkata bahwa jalurnya bisa dijelajahi dengan a = 65. Untuk Jalur 2, solver bisa memberi a nilai apa saja selain dari 65, contohnya a = 0.

Memverifikasi properti

Manticore memungkinkan kontrol penuh atas semua eksekusi masing-masing jalur. Sebagai hasilnya, memungkinkan Anda menambahkan batasan arbitrari ke hampir semua hal. Kontrol ini memungkinkan pembuatan properti pada kontrak.

Perhatikan contoh berikut:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // tidak ada perlindungan terhadap overflow
3  return c;
4}
 Salin

Di sini hanya ada satu jalur untuk dijelajahi dalam fungsi:

• Jalur 1: c = a + b

Dengan menggunakan Manticore, Anda bisa memeriksa overflow, dan menambahkan batasan ke predikat jalur:

• c = a + b AND (c < a OR c < b)

Jika memungkinkan untuk menemukan valuasi dari a dan b di mana predikat jalur bisa dilakukan, itu berarti Anda telah menemukan overflow. Sebagai contoh solver bisa menghasilkan input a = 10, b = MAXUINT256.

Jika Anda mempertimbangkan versi tetapnya:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
 Salin

Formula yang terkait dengan pemeriksaan overflow akan menjadi:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Formula ini tidak bisa diselesaikan; dengan kata lain ini adalah bukti bahwa dalam safe_add, c akan selalu bertambah.

Dengan demikian, DSE adalah peralatan yang efektif yang bisa memverifikasi batasan arbitrari pada kode Anda.

Menjalankan dengan Manticore

Kita akan melihat cara menjelajahi kontrak pintar dengan API Manticore. Targetnya adalah kontrak pintar example.sol(opens in a new tab) berikut ini:

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Tampilkan semua
 Salin

Menjalankan penjelajahan mandiri

Anda bisa menjalankan Manticore secara langsung pada kontrak pintar dengan mengikuti perintah berikut (proyek bisa berupa File Solidity, atau direktori proyek):

manticore project

Anda akan mendapatkan output kasus percobaan seperti yang satu ini (urutannya bisa berubah):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Tampilkan semua

Tanpa infromasi tambahan, Manticore akan menjelajahi kontrak dengan transaksi simbolis baru sampai tidak lagi menjelajahi jalur baru pada kontrak. Manticore tidak menjalankan transaksi baru setelah satu transaksi gagal (contohnya: setelah pembalikan).

Manticore akan menghasilkan output informasi dalam direktori mcore_*. Di antaranya, Anda akan menemukan ini dalam direktori:

• global.summary: peringatan cakupan dan pengompilasi
• test_XXXXX.summary: cakupan, instruksi terakhir, saldo akun per kasus percobaan
• test_XXXXX.tx: daftar mendetail transaksi per kasus percobaan

Di sini Manticore menemukan 7 kasus percobaan, yang sesuai dengan (urutan nama filenya mungkin berubah):

Ringkasan penjelejahan f(!=65) berarti f dipanggil dengan nilai apa saja yang berbeda dari 65.

Seperti yang Anda lihat, Manticore menghasilkan kasus percobaan yang unik untuk setiap transaksi yang berhasil atau dibalikkan.

Gunakan bendera --quick-mode jika Anda mau penjelajahan kode yang cepat (ini mematikan detektor bug, komputasi gas, ...)

Memanipulasi kontrak pintar lewat API

Bagian ini menjelaskan detail cara memanipulasi kontrak pintar lewat API Python Manticore. Anda bisa membuat file baru dengan ekstensi python *.py dan menulis kode yang diperlukan dengan menambahkan perintah API (dasar-dasarnya akan dijelaskan di bawah) ke dalam file lalu menjalankannya dengan perintah python3 *.py. Anda juga bisa mengeksekui perintah di bawah ini, langsung ke dalam konsol python; untuk menjalankan konsol gunakan perintah python3.

Membuat Akun

Langkah pertama yang harus Anda lakukan adalah memulai blockchain baru dengan perintah berikut:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
 Salin

Akun non-kontrak dibuat menggunakan m.create_account(opens in a new tab):

1user_account = m.create_account(balance=1000)
 Salin

Kontrak Solidity bisa digunakan menggunakan m.solidity_create_contract(opens in a new tab):

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Tampilkan semua
 Salin

Ringkasan

• You can create user and contract accounts with m.create_account(opens in a new tab) and m.solidity_create_contract(opens in a new tab).

Mengeksekusi transaksi

Manticore mendukung dua jenis transaksi:

• Transaksi mentah: semua fungsi dijelajahi
• Transaksi bernama: hanya satu fungsi dijelajahi

Transaksi mentah

Satu transaksi mentah dieksekusi menggunakan m.transaction(opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
 Salin

Pemanggil, alamat, data, atau nilai transaksi bisa berbentuk baik konkret atau simbolis:

• m.make_symbolic_value(opens in a new tab) membuat nilai simbolis.
• m.make_symbolic_buffer(size)(opens in a new tab) membuat array bita simbolis.

Sebagai contoh:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
 Salin

Jika datanya simbolis, Manticore akan menjelajahi semua fungsi kontrak saat eksekusi transaksi. Akan membantu membaca penjelasan Fungsi Fallback dalam artikel Praktik langsung dengan Ethernaut CTF(opens in a new tab) untuk memahami cara kerja pemilihan fungsi.

Transaksi bernama

Fungsi bisa dieksekusi melalui namanya. Untuk mengeksekusi f(uint var) dengan nilai simbolis, dari user_account, dan dengan 0 ether, gunakan:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
 Salin

Jika nilai transaksi tidak ditentukan, nilainya 0 secara default.

Ringkasan

• Argumen transaksi bisa berbentuk konkret atau simbolis
• Sebuah transaksi mentah akan menjelajahi semua fungsi
• Fungsi bisa dipanggil berdasarkan namanya

Ruang Kerja

m.workspace adalah direktori yang digunakan sebagai direktori output untuk semua file yang dihasilkan:

1print("Results are in {}".format(m.workspace))
 Salin

Akhiri Penjelajahan

Untuk menghentikan penjelajahan gunakan m.finalize()(opens in a new tab). Tidak ada transaksi berikutnya yang harus dikirimkan setelah metode ini dipanggil dan Manticore menghasilkan kasus percobaan untuk setiap jalur yang dijelajahi.

Ringkasan: Menjalankan dengan Manticore

Dengan menggabungkan semua langkah sebelumnya, kita mendapatkan:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
Tampilkan semua
 Salin

Semua kode di atas bisa Anda temukan di example_run.py(opens in a new tab)

Mendapatkan jalur throwing

Sekarang kita akan membuat input spesifik untuk jalur yang memunculkan pengecualian dalam f(). Targetnya masih kontrak pintar example.sol(opens in a new tab) berikut:

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 Salin

Menggunakan informasi state

Tiap jalur yang dieksekusi memiliki state blockchainnya. Sebuah state bisa berstatus siap atau dimatikan, artinya bahwa state menjangkau instruksi THROW atau REVERT:

• m.ready_states(opens in a new tab): daftar state yang berstatus siap (mereka tidak mengeksekusi REVERT/INVALID)
• m.killed_states(opens in a new tab): daftar state yang dimatikan
• m.all_states(opens in a new tab): semua state

1for state in m.all_states:
2    # do something with state
 Salin

Anda bisa mengakses informasi state. Sebagai contoh:

• state.platform.get_balance(account.address): saldo akun
• state.platform.transactions: daftar traksaksi
• state.platform.transactions[-1].return_data: data yang dikembalikan oleh transaksi terakhir

Data yang dikembalikan oleh transaksi terakhir adalah sebuah array, yang bisa diubah ke nilai dengan ABI.deserialize, contohnya:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
 Salin

Cara menghasilkan kasus percobaan

Gunakan m.generate_testcase(state, name)(opens in a new tab) untuk menghasilkan kasus percobaan:

1m.generate_testcase(state, 'BugFound')
 Salin

Ringkasan

• Anda bisa mengulangi state dengan m.all_states
• state.platform.get_balance(account.address) mengembalikan saldo akun
• state.platform.transactions mengembalikan daftar transaksi
• transaction.return_data adalah data yang dikembalikan
• m.generate_testcase(state, name) menghasilkan input untuk state

Ringkasan: Mendapatkan Jalur Throwing

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Check if an execution ends with a REVERT or INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
Tampilkan semua
 Salin

Semua kode di atas bisa ditemukan dalam example_run.py(opens in a new tab)

Ingatlah kita telah menghasilkan skrip yang jauh lebih sederhana, karena semua state yang dikembalikan oleh terminated_state memiliki REVERT atau INVALID di dalam hasilnya: contoh ini hanya untuk menunjukkan cara memanipulasi API.

Menambahkan batasan

Kita akan melihat cara membatasi penjelajahan. Kita akan membuat asumsi bahwa dokumentasi state f() yang fungsinya tidak pernah dipanggil dengan a == 65, sehingga bug mana pun dengan a == 65 bukan bug sebenarnya. Targetnya masih kontrak pintar example.sol(opens in a new tab) berikut:

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 Salin

Operator

Modul Operator(opens in a new tab) mendukung manipulasi batasan, antara lain menyediakan:

• Operators.AND,
• Operators.OR,
• Operators.UGT (unsigned greater than),
• Operators.UGE (unsigned greater than or equal to),
• Operators.ULT (unsigned lower than),
• Operators.ULE (unsigned lower than or equal to).

Untuk mengimpor modul gunakan fungsi berikut:

1dari Operator impor manticore.core.smtlib
 Salin

Operators.CONCAT digunakan untuk menghubungkan array dengan nilai. Contohnya, transaksi return_data perlu diubah ke nilai untuk diperiksa terhadap nilai lainnya:

1last_return = Operators.CONCAT(256, *last_return)
 Salin

Batasan

Anda bisa menggunakan batasan secara global atau untuk state tertentu.

Batasan global

Use m.constrain(constraint) to add a global constraint. Contohnya, Anda bisa memanggil kontrak dari alamat simbolis, dan membatasi alamat ini menjadi nilai spesifik:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
 Salin

Batasan state

Gunakan state.constrain(constraint)(opens in a new tab) untuk menambahkan batasan ke state tertentu. Ini bisa digunakan untuk membatasi state setelah penjelajahannya untuk memeriksa beberapa properti di dalamnya.

Memeriksa Batasan

Gunakan solver.check(state.constraints) untuk mengetahui apakah batasan masih memungkinkan. Contohnya, fungsi berikut akan membatasi symbolic_value agar berbeda dari 65 dan memeriksa apakah state masih memungkinkan:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # state is feasible
 Salin

Ringkasan: Menambahkan batasan

Dengan menambahkan batasan ke kode sebelumnya, kita mendapatkan:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Check if an execution ends with a REVERT or INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
Tampilkan semua
 Salin

Semua kode di atas bisa ditemukan dalam example_run.py(opens in a new tab)