Lompat ke konten utama
Change page

Verifikasi formal kontrak pintar

Edit halaman (opens in a new tab)

Kontrak pintar memungkinkan pembuatan aplikasi yang terdesentralisasi, tanpa kepercayaan, dan tangguh yang memperkenalkan kasus penggunaan baru dan membuka nilai bagi pengguna. Karena kontrak pintar menangani nilai dalam jumlah besar, keamanan menjadi pertimbangan penting bagi pengembang.

Verifikasi formal adalah salah satu teknik yang direkomendasikan untuk meningkatkan keamanan kontrak pintar. Verifikasi formal, yang menggunakan metode formal (opens in a new tab) untuk menentukan, merancang, dan memverifikasi program, telah digunakan selama bertahun-tahun untuk memastikan kebenaran sistem perangkat keras dan perangkat lunak yang kritis.

Ketika diimplementasikan dalam kontrak pintar, verifikasi formal dapat membuktikan bahwa logika bisnis kontrak memenuhi spesifikasi yang telah ditentukan sebelumnya. Dibandingkan dengan metode lain untuk menilai kebenaran kode kontrak, seperti pengujian, verifikasi formal memberikan jaminan yang lebih kuat bahwa kontrak pintar secara fungsional benar.

Apa itu verifikasi formal?

Verifikasi formal mengacu pada proses mengevaluasi kebenaran suatu sistem sehubungan dengan spesifikasi formal. Secara lebih sederhana, verifikasi formal memungkinkan kita untuk memeriksa apakah perilaku suatu sistem memenuhi beberapa persyaratan (yaitu, sistem tersebut melakukan apa yang kita inginkan).

Perilaku yang diharapkan dari sistem (kontrak pintar dalam hal ini) dijelaskan menggunakan pemodelan formal, sementara bahasa spesifikasi memungkinkan pembuatan properti formal. Teknik verifikasi formal kemudian dapat memverifikasi bahwa implementasi kontrak mematuhi spesifikasinya dan memperoleh bukti matematis dari kebenaran implementasi tersebut. Ketika sebuah kontrak memenuhi spesifikasinya, kontrak tersebut digambarkan sebagai "benar secara fungsional", "benar berdasarkan desain", atau "benar berdasarkan konstruksi".

Apa itu model formal?

Dalam ilmu komputer, model formal (opens in a new tab) adalah deskripsi matematis dari proses komputasi. Program diabstraksikan menjadi fungsi matematika (persamaan), dengan model yang menjelaskan bagaimana keluaran ke fungsi dihitung berdasarkan suatu masukan.

Model formal memberikan tingkat abstraksi di mana analisis perilaku program dapat dievaluasi. Keberadaan model formal memungkinkan pembuatan spesifikasi formal, yang menjelaskan properti yang diinginkan dari model yang bersangkutan.

Berbagai teknik digunakan untuk memodelkan kontrak pintar untuk verifikasi formal. Misalnya, beberapa model digunakan untuk menalar perilaku tingkat tinggi dari kontrak pintar. Teknik pemodelan ini menerapkan pandangan kotak hitam (black-box) pada kontrak pintar, memandangnya sebagai sistem yang menerima masukan dan mengeksekusi komputasi berdasarkan masukan tersebut.

Model tingkat tinggi berfokus pada hubungan antara kontrak pintar dan agen eksternal, seperti akun yang dimiliki secara eksternal (EOA), akun kontrak, dan lingkungan rantai blok. Model semacam itu berguna untuk mendefinisikan properti yang menentukan bagaimana kontrak harus berperilaku sebagai respons terhadap interaksi pengguna tertentu.

Sebaliknya, model formal lainnya berfokus pada perilaku tingkat rendah dari kontrak pintar. Meskipun model tingkat tinggi dapat membantu menalar fungsionalitas kontrak, model tersebut mungkin gagal menangkap detail tentang cara kerja internal dari implementasinya. Model tingkat rendah menerapkan pandangan kotak putih (white-box) pada analisis program dan mengandalkan representasi tingkat rendah dari aplikasi kontrak pintar, seperti jejak program dan grafik aliran kontrol (opens in a new tab), untuk menalar properti yang relevan dengan eksekusi kontrak.

Model tingkat rendah dianggap ideal karena mewakili eksekusi aktual dari kontrak pintar di lingkungan eksekusi Ethereum (yaitu, EVM). Teknik pemodelan tingkat rendah sangat berguna dalam menetapkan properti keamanan kritis dalam kontrak pintar dan mendeteksi potensi kerentanan.

Apa itu spesifikasi formal?

Spesifikasi pada dasarnya adalah persyaratan teknis yang harus dipenuhi oleh sistem tertentu. Dalam pemrograman, spesifikasi mewakili gagasan umum tentang eksekusi program (yaitu, apa yang seharusnya dilakukan oleh program).

Dalam konteks kontrak pintar, spesifikasi formal mengacu pada properti—deskripsi formal dari persyaratan yang harus dipenuhi oleh kontrak. Properti semacam itu digambarkan sebagai "invarian" dan mewakili asersi logis tentang eksekusi kontrak yang harus tetap benar dalam setiap keadaan yang memungkinkan, tanpa pengecualian apa pun.

Dengan demikian, kita dapat menganggap spesifikasi formal sebagai kumpulan pernyataan yang ditulis dalam bahasa formal yang menjelaskan eksekusi yang dimaksudkan dari kontrak pintar. Spesifikasi mencakup properti kontrak dan menentukan bagaimana kontrak harus berperilaku dalam keadaan yang berbeda. Tujuan verifikasi formal adalah untuk menentukan apakah kontrak pintar memiliki properti ini (invarian) dan bahwa properti ini tidak dilanggar selama eksekusi.

Spesifikasi formal sangat penting dalam mengembangkan implementasi kontrak pintar yang aman. Kontrak yang gagal mengimplementasikan invarian atau propertinya dilanggar selama eksekusi rentan terhadap kerentanan yang dapat merusak fungsionalitas atau menyebabkan eksploitasi berbahaya.

Jenis spesifikasi formal untuk kontrak pintar

Spesifikasi formal memungkinkan penalaran matematis tentang kebenaran eksekusi program. Seperti halnya model formal, spesifikasi formal dapat menangkap properti tingkat tinggi atau perilaku tingkat rendah dari implementasi kontrak.

Spesifikasi formal diturunkan menggunakan elemen logika program (opens in a new tab), yang memungkinkan penalaran formal tentang properti suatu program. Logika program memiliki aturan formal yang mengekspresikan (dalam bahasa matematika) perilaku yang diharapkan dari suatu program. Berbagai logika program digunakan dalam membuat spesifikasi formal, termasuk logika keterjangkauan (reachability logic) (opens in a new tab), logika temporal (opens in a new tab), dan logika Hoare (opens in a new tab).

Spesifikasi formal untuk kontrak pintar dapat diklasifikasikan secara luas sebagai spesifikasi tingkat tinggi atau tingkat rendah. Terlepas dari kategori mana spesifikasi tersebut berada, spesifikasi tersebut harus secara memadai dan tidak ambigu menggambarkan properti sistem yang sedang dianalisis.

Spesifikasi tingkat tinggi

Sesuai dengan namanya, spesifikasi tingkat tinggi (juga disebut "spesifikasi berorientasi model") menjelaskan perilaku tingkat tinggi dari suatu program. Spesifikasi tingkat tinggi memodelkan kontrak pintar sebagai mesin state terbatas (finite state machine/FSM) (opens in a new tab), yang dapat bertransisi antar state dengan melakukan operasi, dengan logika temporal yang digunakan untuk mendefinisikan properti formal untuk model FSM.

Logika temporal (opens in a new tab) adalah "aturan untuk menalar proposisi yang dikualifikasikan dalam hal waktu (misalnya, "Saya selalu lapar" atau "Saya pada akhirnya akan lapar")." Ketika diterapkan pada verifikasi formal, logika temporal digunakan untuk menyatakan asersi tentang perilaku yang benar dari sistem yang dimodelkan sebagai mesin state. Secara khusus, logika temporal menjelaskan state masa depan yang dapat dialami oleh kontrak pintar dan bagaimana kontrak tersebut bertransisi antar state.

Spesifikasi tingkat tinggi umumnya menangkap dua properti temporal kritis untuk kontrak pintar: keamanan (safety) dan kehidupan (liveness). Properti keamanan mewakili gagasan bahwa "tidak ada hal buruk yang pernah terjadi" dan biasanya mengekspresikan invariansi. Properti keamanan dapat mendefinisikan persyaratan perangkat lunak umum, seperti kebebasan dari kebuntuan (deadlock) (opens in a new tab), atau mengekspresikan properti spesifik domain untuk kontrak (misalnya, invarian pada kontrol akses untuk fungsi, nilai variabel state yang dapat diterima, atau kondisi untuk transfer token).

Ambil contoh persyaratan keamanan ini yang mencakup kondisi untuk menggunakan transfer() atau transferFrom() dalam kontrak token ERC-20: "Saldo pengirim tidak pernah lebih rendah dari jumlah token yang diminta untuk dikirim.". Deskripsi bahasa alami dari invarian kontrak ini dapat diterjemahkan ke dalam spesifikasi formal (matematis), yang kemudian dapat diperiksa validitasnya secara ketat.

Properti kehidupan (liveness) menegaskan bahwa "sesuatu yang baik pada akhirnya terjadi" dan berkaitan dengan kemampuan kontrak untuk maju melalui state yang berbeda. Contoh properti kehidupan adalah "likuiditas", yang mengacu pada kemampuan kontrak untuk mentransfer saldonya kepada pengguna berdasarkan permintaan. Jika properti ini dilanggar, pengguna tidak akan dapat menarik aset yang disimpan dalam kontrak, seperti yang terjadi pada insiden dompet Parity (opens in a new tab).

Spesifikasi tingkat rendah

Spesifikasi tingkat tinggi mengambil model state terbatas dari suatu kontrak sebagai titik awal dan mendefinisikan properti yang diinginkan dari model ini. Sebaliknya, spesifikasi tingkat rendah (juga disebut "spesifikasi berorientasi properti") sering memodelkan program (kontrak pintar) sebagai sistem yang terdiri dari kumpulan fungsi matematika dan menjelaskan perilaku yang benar dari sistem tersebut.

Secara lebih sederhana, spesifikasi tingkat rendah menganalisis jejak program dan mencoba mendefinisikan properti kontrak pintar atas jejak ini. Jejak mengacu pada urutan eksekusi fungsi yang mengubah state kontrak pintar; oleh karena itu, spesifikasi tingkat rendah membantu menentukan persyaratan untuk eksekusi internal kontrak.

Spesifikasi formal tingkat rendah dapat diberikan sebagai properti bergaya Hoare atau invarian pada jalur eksekusi.

Properti bergaya Hoare

Logika Hoare (opens in a new tab) menyediakan serangkaian aturan formal untuk menalar kebenaran program, termasuk kontrak pintar. Properti bergaya Hoare diwakili oleh tripel Hoare {P}c{Q}, di mana c adalah program dan P serta Q adalah predikat pada state c (yaitu, program), yang secara formal digambarkan masing-masing sebagai prakondisi dan pascakondisi.

Prakondisi adalah predikat yang menjelaskan kondisi yang diperlukan untuk eksekusi fungsi yang benar; pengguna yang memanggil kontrak harus memenuhi persyaratan ini. Pascakondisi adalah predikat yang menjelaskan kondisi yang ditetapkan oleh fungsi jika dieksekusi dengan benar; pengguna dapat mengharapkan kondisi ini menjadi benar setelah memanggil fungsi tersebut. Sebuah invarian dalam logika Hoare adalah predikat yang dipertahankan oleh eksekusi suatu fungsi (yaitu, tidak berubah).

Spesifikasi bergaya Hoare dapat menjamin kebenaran parsial atau kebenaran total. Implementasi fungsi kontrak "benar secara parsial" jika prakondisi bernilai benar sebelum fungsi dieksekusi, dan jika eksekusi berakhir, pascakondisi juga benar. Bukti kebenaran total diperoleh jika prakondisi benar sebelum fungsi dieksekusi, eksekusi dijamin akan berakhir dan ketika itu terjadi, pascakondisi bernilai benar.

Mendapatkan bukti kebenaran total itu sulit karena beberapa eksekusi mungkin tertunda sebelum berakhir, atau tidak pernah berakhir sama sekali. Meskipun demikian, pertanyaan apakah eksekusi berakhir bisa dibilang tidak relevan karena mekanisme gas Ethereum mencegah perulangan program yang tak terbatas (eksekusi berakhir dengan sukses atau berakhir karena kesalahan 'kehabisan gas').

Spesifikasi kontrak pintar yang dibuat menggunakan logika Hoare akan memiliki prakondisi, pascakondisi, dan invarian yang ditentukan untuk eksekusi fungsi dan perulangan dalam kontrak. Prakondisi sering kali mencakup kemungkinan masukan yang salah ke suatu fungsi, dengan pascakondisi yang menjelaskan respons yang diharapkan terhadap masukan tersebut (misalnya, memunculkan pengecualian tertentu). Dengan cara ini, properti bergaya Hoare efektif untuk memastikan kebenaran implementasi kontrak.

Banyak kerangka kerja verifikasi formal menggunakan spesifikasi bergaya Hoare untuk membuktikan kebenaran semantik dari fungsi. Dimungkinkan juga untuk menambahkan properti bergaya Hoare (sebagai asersi) secara langsung ke kode kontrak dengan menggunakan pernyataan require dan assert di Solidity.

Pernyataan require mengekspresikan prakondisi atau invarian dan sering digunakan untuk memvalidasi masukan pengguna, sementara assert menangkap pascakondisi yang diperlukan untuk keamanan. Misalnya, kontrol akses yang tepat untuk fungsi (contoh properti keamanan) dapat dicapai menggunakan require sebagai pemeriksaan prakondisi pada identitas akun pemanggil. Demikian pula, invarian pada nilai variabel state yang diizinkan dalam kontrak (misalnya, jumlah total token yang beredar) dapat dilindungi dari pelanggaran dengan menggunakan assert untuk mengonfirmasi state kontrak setelah eksekusi fungsi.

Properti tingkat jejak

Spesifikasi berbasis jejak menjelaskan operasi yang mentransisikan kontrak di antara state yang berbeda dan hubungan antara operasi-operasi ini. Seperti yang dijelaskan sebelumnya, jejak adalah urutan operasi yang mengubah state kontrak dengan cara tertentu.

Pendekatan ini bergantung pada model kontrak pintar sebagai sistem transisi state dengan beberapa state yang telah ditentukan sebelumnya (dijelaskan oleh variabel state) bersama dengan serangkaian transisi yang telah ditentukan sebelumnya (dijelaskan oleh fungsi kontrak). Selanjutnya, grafik aliran kontrol (opens in a new tab) (CFG), yang merupakan representasi grafis dari aliran eksekusi program, sering digunakan untuk menjelaskan semantik operasional dari suatu kontrak. Di sini, setiap jejak direpresentasikan sebagai jalur pada grafik aliran kontrol.

Terutama, spesifikasi tingkat jejak digunakan untuk menalar pola eksekusi internal dalam kontrak pintar. Dengan membuat spesifikasi tingkat jejak, kita menegaskan jalur eksekusi yang dapat diterima (yaitu, transisi state) untuk kontrak pintar. Menggunakan teknik, seperti eksekusi simbolik, kita dapat memverifikasi secara formal bahwa eksekusi tidak pernah mengikuti jalur yang tidak didefinisikan dalam model formal.

Mari kita gunakan contoh kontrak DAO yang memiliki beberapa fungsi yang dapat diakses publik untuk menjelaskan properti tingkat jejak. Di sini, kita berasumsi bahwa kontrak DAO memungkinkan pengguna untuk melakukan operasi berikut:

  • Menyetor dana

  • Memberikan suara pada proposal setelah menyetor dana

  • Mengklaim pengembalian dana jika mereka tidak memberikan suara pada proposal

Contoh properti tingkat jejak bisa berupa "pengguna yang tidak menyetor dana tidak dapat memberikan suara pada proposal" atau "pengguna yang tidak memberikan suara pada proposal harus selalu dapat mengklaim pengembalian dana". Kedua properti tersebut menegaskan urutan eksekusi yang disukai (pemungutan suara tidak dapat terjadi sebelum menyetor dana dan mengklaim pengembalian dana tidak dapat terjadi setelah memberikan suara pada proposal).

Teknik untuk verifikasi formal kontrak pintar

Pemeriksaan model

Pemeriksaan model adalah teknik verifikasi formal di mana algoritma memeriksa model formal kontrak pintar terhadap spesifikasinya. Dalam pemeriksaan model, kontrak pintar sering direpresentasikan sebagai sistem transisi state, sementara properti pada state kontrak yang diizinkan didefinisikan menggunakan logika temporal.

Pemeriksaan model memerlukan pembuatan representasi matematis abstrak dari suatu sistem (yaitu, kontrak) dan mengekspresikan properti sistem ini menggunakan rumus yang berakar pada logika proposisional (opens in a new tab). Hal ini menyederhanakan tugas algoritma pemeriksaan model, yaitu untuk membuktikan bahwa model matematika memenuhi rumus logika yang diberikan.

Pemeriksaan model dalam verifikasi formal terutama digunakan untuk mengevaluasi properti temporal yang menggambarkan perilaku kontrak dari waktu ke waktu. Properti temporal untuk kontrak pintar mencakup keamanan dan kehidupan, yang telah kita jelaskan sebelumnya.

Misalnya, properti keamanan yang terkait dengan kontrol akses (misalnya, Hanya pemilik kontrak yang dapat memanggil selfdestruct) dapat ditulis dalam logika formal. Setelah itu, algoritma pemeriksaan model dapat memverifikasi apakah kontrak memenuhi spesifikasi formal ini.

Pemeriksaan model menggunakan eksplorasi ruang state, yang melibatkan konstruksi semua kemungkinan state dari kontrak pintar dan mencoba menemukan state yang dapat dijangkau yang mengakibatkan pelanggaran properti. Namun, hal ini dapat menyebabkan jumlah state yang tak terbatas (dikenal sebagai "masalah ledakan state"), oleh karena itu pemeriksa model mengandalkan teknik abstraksi untuk memungkinkan analisis kontrak pintar yang efisien.

Pembuktian teorema

Pembuktian teorema adalah metode penalaran matematis tentang kebenaran program, termasuk kontrak pintar. Ini melibatkan transformasi model sistem kontrak dan spesifikasinya menjadi rumus matematika (pernyataan logika).

Tujuan pembuktian teorema adalah untuk memverifikasi ekuivalensi logis antara pernyataan-pernyataan ini. "Ekuivalensi logis" (juga disebut "bi-implikasi logis") adalah jenis hubungan antara dua pernyataan sedemikian rupa sehingga pernyataan pertama benar jika dan hanya jika pernyataan kedua benar.

Hubungan yang diperlukan (ekuivalensi logis) antara pernyataan tentang model kontrak dan propertinya dirumuskan sebagai pernyataan yang dapat dibuktikan (disebut teorema). Menggunakan sistem inferensi formal, pembukti teorema otomatis dapat memverifikasi validitas teorema tersebut. Dengan kata lain, pembukti teorema dapat secara meyakinkan membuktikan bahwa model kontrak pintar sama persis dengan spesifikasinya.

Sementara pemeriksaan model memodelkan kontrak sebagai sistem transisi dengan state terbatas, pembuktian teorema dapat menangani analisis sistem state tak terbatas. Namun, ini berarti pembukti teorema otomatis tidak selalu dapat mengetahui apakah masalah logika "dapat diputuskan" atau tidak.

Akibatnya, bantuan manusia sering kali diperlukan untuk memandu pembukti teorema dalam memperoleh bukti kebenaran. Penggunaan upaya manusia dalam pembuktian teorema membuatnya lebih mahal untuk digunakan daripada pemeriksaan model, yang sepenuhnya otomatis.

Eksekusi simbolik

Eksekusi simbolik adalah metode menganalisis kontrak pintar dengan mengeksekusi fungsi menggunakan nilai simbolik (misalnya, x > 5) alih-alih nilai konkret (misalnya, x == 5). Sebagai teknik verifikasi formal, eksekusi simbolik digunakan untuk menalar secara formal tentang properti tingkat jejak dalam kode kontrak.

Eksekusi simbolik merepresentasikan jejak eksekusi sebagai rumus matematika atas nilai masukan simbolik, yang juga disebut predikat jalur. Pemecah SMT (opens in a new tab) digunakan untuk memeriksa apakah predikat jalur "dapat dipenuhi" (yaitu, ada nilai yang dapat memenuhi rumus tersebut). Jika jalur yang rentan dapat dipenuhi, pemecah SMT akan menghasilkan nilai konkret yang memicu dan mengarahkan eksekusi ke jalur tersebut.

Misalkan fungsi kontrak pintar mengambil nilai uint sebagai masukan (x) dan dikembalikan (revert) ketika x lebih besar dari 5 dan juga lebih rendah dari 10. Menemukan nilai untuk x yang memicu kesalahan menggunakan prosedur pengujian normal akan memerlukan penjalanan puluhan kasus uji (atau lebih) tanpa jaminan benar-benar menemukan masukan yang memicu kesalahan.

Sebaliknya, alat eksekusi simbolik akan mengeksekusi fungsi dengan nilai simbolik: X > 5 ∧ X < 10 (yaitu, x lebih besar dari 5 DAN x kurang dari 10). Predikat jalur terkait x = X > 5 ∧ X < 10 kemudian akan diberikan kepada pemecah SMT untuk dipecahkan. Jika nilai tertentu memenuhi rumus x = X > 5 ∧ X < 10, pemecah SMT akan menghitungnya—misalnya, pemecah mungkin menghasilkan 7 sebagai nilai untuk x.

Karena eksekusi simbolik bergantung pada masukan ke program, dan kumpulan masukan untuk mengeksplorasi semua state yang dapat dijangkau berpotensi tak terbatas, ini masih merupakan bentuk pengujian. Namun, seperti yang ditunjukkan dalam contoh, eksekusi simbolik lebih efisien daripada pengujian biasa untuk menemukan masukan yang memicu pelanggaran properti.

Selain itu, eksekusi simbolik menghasilkan lebih sedikit positif palsu daripada teknik berbasis properti lainnya (misalnya, fuzzing) yang secara acak menghasilkan masukan ke suatu fungsi. Jika state kesalahan dipicu selama eksekusi simbolik, maka dimungkinkan untuk menghasilkan nilai konkret yang memicu kesalahan dan mereproduksi masalah tersebut.

Eksekusi simbolik juga dapat memberikan beberapa tingkat bukti matematis tentang kebenaran. Pertimbangkan contoh berikut dari fungsi kontrak dengan perlindungan limpahan (overflow):

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

Jejak eksekusi yang menghasilkan limpahan bilangan bulat perlu memenuhi rumus: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) Rumus semacam itu tidak mungkin dipecahkan, oleh karena itu rumus ini berfungsi sebagai bukti matematis bahwa fungsi safe_add tidak pernah mengalami limpahan.

Mengapa menggunakan verifikasi formal untuk kontrak pintar?

Kebutuhan akan keandalan

Verifikasi formal digunakan untuk menilai kebenaran sistem kritis keselamatan yang kegagalannya dapat memiliki konsekuensi yang menghancurkan, seperti kematian, cedera, atau kehancuran finansial. Kontrak pintar adalah aplikasi bernilai tinggi yang mengendalikan nilai dalam jumlah besar, dan kesalahan sederhana dalam desain dapat menyebabkan kerugian yang tidak dapat dipulihkan bagi pengguna (opens in a new tab). Namun, memverifikasi kontrak secara formal sebelum penyebaran dapat meningkatkan jaminan bahwa kontrak tersebut akan berkinerja seperti yang diharapkan setelah berjalan di rantai blok.

Keandalan adalah kualitas yang sangat diinginkan dalam kontrak pintar apa pun, terutama karena kode yang disebarkan di Mesin Virtual Ethereum (EVM) biasanya tidak dapat diubah. Dengan peningkatan pasca-peluncuran yang tidak mudah diakses, kebutuhan untuk menjamin keandalan kontrak membuat verifikasi formal diperlukan. Verifikasi formal mampu mendeteksi masalah yang rumit, seperti underflow dan limpahan bilangan bulat, re-entrancy, dan pengoptimalan gas yang buruk, yang mungkin terlewatkan oleh auditor dan penguji.

Membuktikan kebenaran fungsional

Pengujian program adalah metode paling umum untuk membuktikan bahwa kontrak pintar memenuhi beberapa persyaratan. Ini melibatkan eksekusi kontrak dengan sampel data yang diharapkan untuk ditangani dan menganalisis perilakunya. Jika kontrak mengembalikan hasil yang diharapkan untuk data sampel, maka pengembang memiliki bukti objektif tentang kebenarannya.

Namun, pendekatan ini tidak dapat membuktikan eksekusi yang benar untuk nilai masukan yang bukan bagian dari sampel. Oleh karena itu, menguji kontrak dapat membantu mendeteksi bug (yaitu, jika beberapa jalur kode gagal mengembalikan hasil yang diinginkan selama eksekusi), tetapi hal ini tidak dapat secara meyakinkan membuktikan tidak adanya bug.

Sebaliknya, verifikasi formal dapat secara formal membuktikan bahwa kontrak pintar memenuhi persyaratan untuk rentang eksekusi yang tak terbatas tanpa menjalankan kontrak sama sekali. Ini memerlukan pembuatan spesifikasi formal yang secara tepat menggambarkan perilaku kontrak yang benar dan mengembangkan model formal (matematis) dari sistem kontrak. Kemudian kita dapat mengikuti prosedur pembuktian formal untuk memeriksa konsistensi antara model kontrak dan spesifikasinya.

Dengan verifikasi formal, pertanyaan untuk memverifikasi apakah logika bisnis kontrak memenuhi persyaratan adalah proposisi matematis yang dapat dibuktikan atau disangkal. Dengan membuktikan proposisi secara formal, kita dapat memverifikasi jumlah kasus uji yang tak terbatas dengan jumlah langkah yang terbatas. Dengan cara ini, verifikasi formal memiliki prospek yang lebih baik untuk membuktikan bahwa kontrak secara fungsional benar sehubungan dengan spesifikasi.

Target verifikasi yang ideal

Target verifikasi menjelaskan sistem yang akan diverifikasi secara formal. Verifikasi formal paling baik digunakan dalam "sistem tertanam" (perangkat lunak kecil dan sederhana yang membentuk bagian dari sistem yang lebih besar). Mereka juga ideal untuk domain khusus yang memiliki sedikit aturan, karena ini memudahkan modifikasi alat untuk memverifikasi properti spesifik domain.

Kontrak pintar—setidaknya, sampai batas tertentu—memenuhi kedua persyaratan tersebut. Misalnya, ukuran kontrak Ethereum yang kecil membuatnya dapat menerima verifikasi formal. Demikian pula, EVM mengikuti aturan sederhana, yang membuat penentuan dan verifikasi properti semantik untuk program yang berjalan di EVM menjadi lebih mudah.

Siklus pengembangan yang lebih cepat

Teknik verifikasi formal, seperti pemeriksaan model dan eksekusi simbolik, umumnya lebih efisien daripada analisis reguler kode kontrak pintar (dilakukan selama pengujian atau audit). Hal ini karena verifikasi formal mengandalkan nilai simbolik untuk menguji asersi ("bagaimana jika pengguna mencoba menarik n Ether?") tidak seperti pengujian yang menggunakan nilai konkret ("bagaimana jika pengguna mencoba menarik 5 Ether?").

Variabel masukan simbolik dapat mencakup beberapa kelas nilai konkret, sehingga pendekatan verifikasi formal menjanjikan cakupan kode yang lebih banyak dalam jangka waktu yang lebih singkat. Jika digunakan secara efektif, verifikasi formal dapat mempercepat siklus pengembangan bagi pengembang.

Verifikasi formal juga meningkatkan proses membangun aplikasi terdesentralisasi (dapp) dengan mengurangi kesalahan desain yang mahal. Meningkatkan kontrak (jika memungkinkan) untuk memperbaiki kerentanan memerlukan penulisan ulang basis kode yang ekstensif dan lebih banyak upaya yang dihabiskan untuk pengembangan. Verifikasi formal dapat mendeteksi banyak kesalahan dalam implementasi kontrak yang mungkin terlewatkan oleh penguji dan auditor serta memberikan banyak kesempatan untuk memperbaiki masalah tersebut sebelum menyebarkan kontrak.

Kekurangan verifikasi formal

Biaya tenaga kerja manual

Verifikasi formal, terutama verifikasi semi-otomatis di mana manusia memandu pembukti untuk memperoleh bukti kebenaran, membutuhkan tenaga kerja manual yang cukup besar. Selain itu, membuat spesifikasi formal adalah aktivitas kompleks yang menuntut tingkat keterampilan yang tinggi.

Faktor-faktor ini (upaya dan keterampilan) membuat verifikasi formal lebih menuntut dan mahal dibandingkan dengan metode biasa untuk menilai kebenaran dalam kontrak, seperti pengujian dan audit. Namun demikian, membayar biaya untuk audit verifikasi penuh adalah hal yang praktis, mengingat biaya kesalahan dalam implementasi kontrak pintar.

Negatif palsu

Verifikasi formal hanya dapat memeriksa apakah eksekusi kontrak pintar sesuai dengan spesifikasi formal. Oleh karena itu, penting untuk memastikan spesifikasi tersebut dengan tepat menggambarkan perilaku yang diharapkan dari kontrak pintar.

Jika spesifikasi ditulis dengan buruk, pelanggaran properti—yang mengarah pada eksekusi yang rentan—tidak dapat dideteksi oleh audit verifikasi formal. Dalam hal ini, pengembang mungkin secara keliru berasumsi bahwa kontrak tersebut bebas bug.

Masalah kinerja

Verifikasi formal menghadapi sejumlah masalah kinerja. Misalnya, masalah ledakan state dan jalur yang masing-masing ditemui selama pemeriksaan model dan pemeriksaan simbolik, dapat memengaruhi prosedur verifikasi. Selain itu, alat verifikasi formal sering menggunakan pemecah SMT dan pemecah kendala lainnya di lapisan dasarnya, dan pemecah ini mengandalkan prosedur komputasi yang intensif.

Selain itu, tidak selalu mungkin bagi pemverifikasi program untuk menentukan apakah suatu properti (dijelaskan sebagai rumus logika) dapat dipenuhi atau tidak ("masalah desidabilitas (opens in a new tab)") karena program mungkin tidak pernah berakhir. Oleh karena itu, mungkin tidak mungkin untuk membuktikan beberapa properti untuk suatu kontrak meskipun kontrak tersebut telah ditentukan dengan baik.

Alat verifikasi formal untuk kontrak pintar Ethereum

Bahasa spesifikasi untuk membuat spesifikasi formal

Act: Act memungkinkan spesifikasi pembaruan penyimpanan, pra/pascakondisi, dan invarian kontrak. Rangkaian alatnya juga memiliki backend bukti yang mampu membuktikan banyak properti melalui Coq, pemecah SMT, atau hevm.

Scribble - Scribble mengubah anotasi kode dalam bahasa spesifikasi Scribble menjadi asersi konkret yang memeriksa spesifikasi.

Dafny - Dafny adalah bahasa pemrograman siap verifikasi yang mengandalkan anotasi tingkat tinggi untuk menalar dan membuktikan kebenaran kode.

Pemverifikasi program untuk memeriksa kebenaran

Certora Prover - Certora Prover adalah alat verifikasi formal otomatis untuk memeriksa kebenaran kode dalam kontrak pintar. Spesifikasi ditulis dalam CVL (Certora Verification Language), dengan pelanggaran properti dideteksi menggunakan kombinasi analisis statis dan pemecahan kendala.

Solidity SMTChecker - SMTChecker Solidity adalah pemeriksa model bawaan berdasarkan SMT (Satisfiability Modulo Theories) dan pemecahan Horn. Ini mengonfirmasi apakah kode sumber kontrak cocok dengan spesifikasi selama kompilasi dan secara statis memeriksa pelanggaran properti keamanan.

solc-verify - solc-verify adalah versi lanjutan dari kompiler Solidity yang dapat melakukan verifikasi formal otomatis pada kode Solidity menggunakan anotasi dan verifikasi program modular.

KEVM - KEVM adalah semantik formal dari Mesin Virtual Ethereum (EVM) yang ditulis dalam kerangka kerja K. KEVM dapat dieksekusi dan dapat membuktikan asersi terkait properti tertentu menggunakan logika keterjangkauan.

Kerangka kerja logis untuk pembuktian teorema

Isabelle - Isabelle/HOL adalah asisten bukti yang memungkinkan rumus matematika diekspresikan dalam bahasa formal dan menyediakan alat untuk membuktikan rumus tersebut. Aplikasi utamanya adalah formalisasi bukti matematika dan khususnya verifikasi formal, yang mencakup pembuktian kebenaran perangkat keras atau perangkat lunak komputer dan pembuktian properti bahasa dan protokol komputer.

Rocq - Rocq adalah pembukti teorema interaktif yang memungkinkan Anda mendefinisikan program menggunakan teorema dan secara interaktif menghasilkan bukti kebenaran yang diperiksa oleh mesin.

Alat berbasis eksekusi simbolik untuk mendeteksi pola rentan dalam kontrak pintar

Manticore - Alat untuk menganalisis kode bita EVM berdasarkan eksekusi simbolik.

hevm - hevm adalah mesin eksekusi simbolik dan pemeriksa ekuivalensi untuk kode bita EVM.

Mythril - Alat eksekusi simbolik untuk mendeteksi kerentanan dalam kontrak pintar Ethereum

Bacaan lebih lanjut

Pembaruan terakhir halaman: 28 April 2026

shalom-ezekiels (opens in a new tab)
corwintinesc (opens in a new tab)
MOSHKA-GOTM (opens in a new tab)
+12