Cara menggunakan Manticore untuk menemukan bug dalam kontrak pintar

Solidity

kontrak pintar

keamanan

pengujian

verifikasi formal

Lanjutan

Trailofbits

Building secure contracts

13 Januari 2020

11 menit baca

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":/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 dalam Docker

Di dalam Docker, jalankan:

solc-select 0.5.11
cd /home/trufflecon/

Manticore melalui pip

pip3 install --user manticore

solc 0.5.11 direkomendasikan.

Menjalankan skrip

Untuk menjalankan skrip Python dengan Python 3:

python3 script.py

Pengantar eksekusi simbolik dinamis

Singkatnya tentang Eksekusi Simbolik Dinamis

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

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

Pendekatan ini tidak menghasilkan positif palsu dalam arti bahwa semua state program yang teridentifikasi dapat dipicu selama eksekusi konkret. Misalnya, jika analisis menemukan limpahan (overflow) bilangan bulat, hal itu dijamin dapat direproduksi.

Contoh Predikat Jalur

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

function f(uint a){

  if (a == 65) {
      // Terdapat bug
  }

}

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 pemecah SMT (opens in a new tab), yang akan mencoba memecahkan persamaan tersebut. Untuk Path 1, pemecah akan mengatakan bahwa jalur tersebut dapat dieksplorasi dengan a = 65. Untuk Path 2, pemecah 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:

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // tidak ada perlindungan limpahan
  return c;
}

Di sini hanya ada satu jalur untuk dieksplorasi dalam fungsi:

Jalur 1: c = a + b

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

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

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

Jika Anda mempertimbangkan versi yang diperbaiki:

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

Rumus terkait dengan pemeriksaan limpahan akan menjadi:

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

Rumus ini tidak dapat dipecahkan; 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):

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

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 kasus uji seperti ini (urutannya mungkin berubah):

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

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 mengembalikan (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 kasus uji
test_XXXXX.tx: daftar detail transaksi per kasus uji

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

	Transaksi 0	Transaksi 1	Transaksi 2	Hasil
test_00000000.tx	Pembuatan kontrak	f(!=65)	f(!=65)	STOP
test_00000001.tx	Pembuatan kontrak	fungsi fallback		REVERT
test_00000002.tx	Pembuatan kontrak			RETURN
test_00000003.tx	Pembuatan kontrak	f(65)		REVERT
test_00000004.tx	Pembuatan kontrak	f(!=65)		STOP
test_00000005.tx	Pembuatan kontrak	f(!=65)	f(65)	REVERT
test_00000006.tx	Pembuatan kontrak	f(!=65)	fungsi fallback	REVERT

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

Seperti yang dapat Anda perhatikan, Manticore menghasilkan kasus uji unik untuk setiap transaksi yang berhasil atau dikembalikan.

Gunakan tanda --quick-mode jika Anda menginginkan eksplorasi kode yang cepat (ini menonaktifkan pendeteksi 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 rantai blok baru dengan perintah berikut:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

Kontrak Solidity dapat diterapkan menggunakan m.solidity_create_contract (opens in a new tab):

source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}
'''
# Initiate the contract
contract_account = m.solidity_create_contract(source_code, owner=user_account)

Ringkasan

Anda dapat membuat akun pengguna dan akun 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):

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

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:

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

Jika datanya simbolik, Manticore akan mengeksplorasi semua fungsi kontrak selama eksekusi transaksi. Akan sangat membantu untuk melihat penjelasan Fungsi Fallback di artikel Praktik Langsung 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:

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

Jika value dari transaksi tidak ditentukan, secara default adalah 0.

Ringkasan

Argumen 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:

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

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 kasus uji untuk setiap jalur yang dieksplorasi.

Ringkasan: Menjalankan di bawah Manticore

Menggabungkan semua langkah sebelumnya, kita mendapatkan:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

print("Results are in {}".format(m.workspace))
m.finalize() # hentikan eksplorasi

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

Mendapatkan jalur pelemparan (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):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Menggunakan informasi state

Setiap jalur yang dieksekusi memiliki state rantai bloknya. Sebuah state bisa dalam keadaan siap (ready) atau dimatikan (killed), yang berarti ia mencapai instruksi THROW atau REVERT:

m.ready_states (opens in a new tab): daftar state yang 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

for state in m.all_states:
    # lakukan sesuatu dengan state

Anda dapat mengakses informasi state. 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:

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

Cara menghasilkan kasus uji

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

m.generate_testcase(state, 'BugFound')

Ringkasan

Anda dapat melakukan iterasi pada 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 Pelemparan

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

## Periksa apakah eksekusi berakhir dengan MENGEMBALIKAN atau TIDAK VALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        m.generate_testcase(state, 'ThrowFound')

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 state 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, sehingga bug apa pun dengan a == 65 bukanlah bug yang sebenarnya. Targetnya masih kontrak pintar berikut example.sol (opens in a new tab):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

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:

from manticore.core.smtlib import Operators

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

last_return = Operators.CONCAT(256, *last_return)

Batasan

Anda dapat menggunakan batasan secara global atau untuk state 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:

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

Batasan state

Gunakan state.constrain(constraint) (opens in a new tab) untuk menambahkan batasan ke state tertentu. Ini dapat digunakan untuk membatasi state 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 state tersebut masih layak:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # state memungkinkan

Ringkasan: Menambahkan Batasan

Menambahkan batasan pada kode sebelumnya, kita mendapatkan:

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

m = ManticoreEVM()

with open("example.sol") as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

no_bug_found = True

## Periksa apakah eksekusi berakhir dengan MENGEMBALIKAN atau TIDAK VALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # kami tidak mempertimbangkan jalur di mana a == 65
        condition = symbolic_var != 65
        if m.generate_testcase(state, name="BugFound", only_if=condition):
            print(f'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

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