Cara menggunakan Manticore untuk menemukan bug dalam kontrak pintar

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

Instalasi

Manticore membutuhkan >= python 3.6. Ini dapat diinstal melalui pip atau menggunakan docker.

Manticore melalui docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/share 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 /share

Manticore melalui pip

pip3 install --user "manticore[native]"

solc 0.5.11 direkomendasikan.

Menjalankan skrip

Untuk menjalankan skrip python dengan python 3:

python3 script.py

Pengantar eksekusi simbolik dinamis

Singkatnya Eksekusi Simbolik Dinamis

Eksekusi simbolik dinamis (DSE) adalah teknik analisis program yang mengeksplorasi ruang status dengan tingkat kesadaran semantik yang tinggi. Teknik ini didasarkan pada penemuan "jalur program", yang direpresentasikan sebagai rumus matematika yang disebut path predicates (predikat jalur). Secara konseptual, teknik ini beroperasi pada predikat jalur dalam dua langkah:

1. Mereka dibangun menggunakan batasan pada input program.
2. Mereka digunakan untuk menghasilkan input program yang akan menyebabkan jalur terkait dieksekusi.

Pendekatan ini tidak menghasilkan positif palsu dalam arti bahwa semua status program yang teridentifikasi dapat dipicu selama eksekusi konkret. Misalnya, jika analisis menemukan integer overflow, hal itu dijamin dapat direproduksi.

Contoh Predikat Jalur

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

1function f(uint a){
2  if (a == 65) {
3      // A bug is present
4  }
5}
Salin

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

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

Setiap predikat jalur adalah rumus matematika yang dapat diberikan kepada apa yang disebut SMT solver (opens in a new tab), yang akan mencoba menyelesaikan persamaan tersebut. Untuk Jalur 1, solver akan mengatakan bahwa jalur tersebut dapat dieksplorasi dengan a = 65. Untuk Jalur 2, solver dapat memberikan a nilai apa pun selain 65, misalnya a = 0.

Memverifikasi properti

Manticore memungkinkan kontrol penuh atas semua eksekusi dari setiap jalur. Akibatnya, ini memungkinkan Anda untuk menambahkan batasan arbitrer ke hampir semua hal. Kontrol ini memungkinkan pembuatan properti pada kontrak.

Pertimbangkan contoh berikut:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  return c;
4}
Salin

Di sini hanya ada satu jalur untuk dieksplorasi dalam fungsi:

• Jalur 1: c = a + b

Menggunakan Manticore, Anda dapat memeriksa overflow, dan menambahkan batasan ke predikat jalur:

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

Jika memungkinkan untuk menemukan penilaian a dan b di mana predikat jalur di atas layak, itu berarti Anda telah menemukan overflow. Misalnya solver dapat menghasilkan input a = 10 , b = MAXUINT256.

Jika Anda mempertimbangkan versi yang diperbaiki:

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

Rumus terkait dengan pemeriksaan overflow akan menjadi:

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

Rumus ini tidak dapat diselesaikan; dengan kata lain ini adalah bukti bahwa dalam safe_add, c akan selalu meningkat.

Oleh karena itu, DSE adalah alat yang ampuh, yang dapat memverifikasi batasan arbitrer pada kode Anda.

Menjalankan di bawah Manticore

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

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 eksplorasi mandiri

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

manticore project

Anda akan mendapatkan output dari testcase seperti ini (urutannya mungkin berubah):

...
...
manticore.core.manticore:INFO: Generated testcase No. 0 - STOP
manticore.core.manticore:INFO: Generated testcase No. 1 - REVERT
manticore.core.manticore:INFO: Generated testcase No. 2 - RETURN
manticore.core.manticore:INFO: Generated testcase No. 3 - REVERT
manticore.core.manticore:INFO: Generated testcase No. 4 - STOP
manticore.core.manticore:INFO: Generated testcase No. 5 - REVERT
manticore.core.manticore:INFO: Generated testcase No. 6 - REVERT
...
Tampilkan semua

Tanpa informasi tambahan, Manticore akan mengeksplorasi kontrak dengan transaksi simbolik baru hingga tidak mengeksplorasi jalur baru pada kontrak. Manticore tidak menjalankan transaksi baru setelah transaksi yang gagal (misalnya: setelah revert).

Manticore akan mengeluarkan informasi dalam direktori mcore_*. Di antaranya, Anda akan menemukan di direktori ini:

• global.summary: cakupan dan peringatan kompiler
• test_XXXXX.summary: cakupan, instruksi terakhir, saldo akun per test case
• test_XXXXX.tx: daftar detail transaksi per test case

Di sini Manticore menemukan 7 test case, yang sesuai dengan (urutan nama file mungkin berubah):

Ringkasan eksplorasi f(!=65) menunjukkan f dipanggil dengan nilai apa pun yang berbeda dari 65.

Seperti yang dapat Anda perhatikan, Manticore menghasilkan test case unik untuk setiap transaksi yang berhasil atau di-revert.

Gunakan tanda --quick-mode jika Anda menginginkan eksplorasi kode yang cepat (ini menonaktifkan detektor bug, komputasi gas, ...)

Memanipulasi kontrak pintar melalui API

Bagian ini menjelaskan detail cara memanipulasi kontrak pintar melalui API Python Manticore. Anda dapat 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 ini dan kemudian menjalankannya dengan perintah $ python3 *.py. Anda juga dapat mengeksekusi perintah di bawah ini secara langsung ke dalam konsol python, untuk menjalankan konsol gunakan perintah $ python3.

Membuat Akun

Hal pertama yang harus Anda lakukan adalah menginisiasi 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 dapat diterapkan 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'''
11contract_account = m.solidity_create_contract(source_code, owner=user_account)
Tampilkan semua
Salin

Ringkasan

• Anda dapat membuat akun pengguna dan kontrak dengan m.create_account (opens in a new tab) dan m.solidity_create_contract (opens in a new tab).

Mengeksekusi transaksi

Manticore mendukung dua jenis transaksi:

• Transaksi mentah: semua fungsi dieksplorasi
• Transaksi bernama: hanya satu fungsi yang dieksplorasi

Transaksi mentah

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 dapat berupa konkret atau simbolik:

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

Misalnya:

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

Jika datanya simbolik, Manticore akan mengeksplorasi semua fungsi kontrak selama eksekusi transaksi. Akan sangat membantu untuk melihat penjelasan Fungsi Fallback di artikel Hands on the Ethernaut CTF (opens in a new tab) untuk memahami cara kerja pemilihan fungsi.

Transaksi bernama

Fungsi dapat dieksekusi melalui namanya. Untuk mengeksekusi f(uint var) dengan nilai simbolik, 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 value dari transaksi tidak ditentukan, secara default adalah 0.

Ringkasan

• Argumen dari sebuah transaksi dapat berupa konkret atau simbolik
• Transaksi mentah akan mengeksplorasi semua fungsi
• Fungsi dapat dipanggil dengan 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

Mengakhiri Eksplorasi

Untuk menghentikan eksplorasi gunakan m.finalize() (opens in a new tab). Tidak ada transaksi lebih lanjut yang boleh dikirim setelah metode ini dipanggil dan Manticore menghasilkan test case untuk setiap jalur yang dieksplorasi.

Ringkasan: Menjalankan di bawah Manticore

Menyatukan 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 # hentikan eksplorasi
Tampilkan semua
Salin

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

Mendapatkan jalur yang melempar (throwing paths)

Kita sekarang akan menghasilkan input spesifik untuk jalur yang memunculkan pengecualian di f(). Targetnya masih kontrak pintar berikut example.sol (opens in a new tab):

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 status

Setiap jalur yang dieksekusi memiliki status blockchain-nya. Sebuah status bisa siap (ready) atau dimatikan (killed), yang berarti ia mencapai instruksi THROW atau REVERT:

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

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

Anda dapat mengakses informasi status. Misalnya:

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

Data yang dikembalikan oleh transaksi terakhir adalah sebuah array, yang dapat dikonversi menjadi nilai dengan ABI.deserialize, misalnya:

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

Cara menghasilkan testcase

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

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

Ringkasan

• Anda dapat melakukan iterasi pada status 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 status tersebut

Ringkasan: Mendapatkan Jalur yang Melempar

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 # # Periksa apakah eksekusi berakhir dengan REVERT atau 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 dapat Anda temukan di example_run.py (opens in a new tab)

Catatan kita bisa saja menghasilkan skrip yang jauh lebih sederhana, karena semua status yang dikembalikan oleh terminated_state memiliki REVERT atau INVALID dalam hasilnya: contoh ini hanya dimaksudkan untuk mendemonstrasikan cara memanipulasi API.

Menambahkan batasan

Kita akan melihat cara membatasi eksplorasi. Kita akan membuat asumsi bahwa dokumentasi f() menyatakan bahwa fungsi tersebut tidak pernah dipanggil dengan a == 65, jadi bug apa pun dengan a == 65 bukanlah bug yang sebenarnya. Targetnya masih kontrak pintar berikut example.sol (opens in a new tab):

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 Operators (opens in a new tab) memfasilitasi manipulasi batasan, di antaranya 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 yang berikut ini:

1from manticore.core.smtlib import Operators
Salin

Operators.CONCAT digunakan untuk menggabungkan array ke sebuah nilai. Misalnya, return_data dari sebuah transaksi perlu diubah menjadi nilai untuk diperiksa terhadap nilai lain:

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

Batasan

Anda dapat menggunakan batasan secara global atau untuk status tertentu.

Batasan global

Gunakan m.constrain(constraint) untuk menambahkan batasan global. Misalnya, Anda dapat memanggil kontrak dari alamat simbolik, dan membatasi alamat ini menjadi nilai tertentu:

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

Batasan status

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

Memeriksa Batasan

Gunakan solver.check(state.constraints) untuk mengetahui apakah suatu batasan masih layak. Misalnya, berikut ini akan membatasi symbolic_value agar berbeda dari 65 dan memeriksa apakah status tersebut masih layak:

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

Ringkasan: Menambahkan Batasan

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 dapat Anda temukan di example_run.py (opens in a new tab)

Pembaruan terakhir halaman: 26 April 2024

n (opens in a new tab)

r (opens in a new tab)

h (opens in a new tab)

+6

Lihat kontributor