kontrak pintarmembuatnya memungkinkan untuk membuat aplikasi terdesentralisasi, tanpa kepercayaan, dan tangguh yang memperkenalkan kasus penggunaan baru dan membuka nilai bagi pengguna. Karena kontrak pintar menangani jumlah nilai yang besar, keamanan adalah pertimbangan kritis bagi pengembang.

Verifikasi formal adalah salah satu teknik yang direkomendasikan untuk meningkatkan keamanan kontrak cerdas. Verifikasi formal, yang menggunakan metode formal

(buka di tab baru)

untuk menentukan, merancang, dan memverifikasi program, telah digunakan selama bertahun-tahun untuk memastikan kebenaran sistem perangkat keras dan lunak yang kritis.

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

APA ITU VERIFIKASI FORMAL?

Verifikasi formal merujuk pada proses mengevaluasi kebenaran suatu sistem dengan spesifikasi formal. Dengan kata lain, verifikasi formal memungkinkan kita untuk memeriksa apakah perilaku suatu sistem memenuhi beberapa persyaratan (yaitu, melakukan apa yang kita inginkan).

Perilaku yang diharapkan dari sistem (kontrak pintar dalam hal ini) dijelaskan menggunakan pemodelan formal, sementara bahasa spesifikasi memungkinkan penciptaan properti formal. Teknik verifikasi formal kemudian dapat memverifikasi bahwa implementasi kontrak sesuai dengan spesifikasinya dan menurunkan bukti matematika dari kebenaran yang terdahulunya. Ketika kontrak memenuhi spesifikasinya, itu dijelaskan sebagai “benar secara fungsional”, “benar secara desain”, atau “benar secara konstruksi”.

Apa itu model formal?

Dalam ilmu komputer, model formal

(buka di tab baru)

adalah deskripsi matematis dari proses komputasi. Program-program diabstraksikan menjadi fungsi matematis (persamaan), dengan model tersebut menjelaskan bagaimana output dari fungsi-fungsi dihitung dengan memberikan suatu input.

Model-model formal memberikan tingkat abstraksi di atasnya analisis perilaku program dapat dievaluasi. Keberadaan model formal memungkinkan penciptaan spesifikasi formal, yang menggambarkan properti yang diinginkan dari model yang bersangkutan.

Berbagai teknik digunakan untuk memodelkan kontrak pintar untuk verifikasi formal. Misalnya, beberapa model digunakan untuk merenungkan tentang perilaku tingkat tinggi dari kontrak pintar. Teknik pemodelan ini menerapkan pandangan kotak hitam terhadap kontrak pintar, memandangnya sebagai sistem yang menerima input dan menjalankan komputasi berdasarkan input tersebut.

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

Sebaliknya, model formal lainnya fokus pada perilaku tingkat rendah dari kontrak cerdas. Sementara model tingkat tinggi dapat membantu dalam penalaran tentang fungsionalitas kontrak, mereka mungkin gagal menangkap detail tentang cara kerja internal implementasinya. Model tingkat rendah menerapkan pandangan kotak putih untuk analisis program dan mengandalkan representasi tingkat rendah dari aplikasi kontrak cerdas, seperti jejak program dan grafik alur kontrol

(buka di tab baru)

, untuk merenungkan tentang properti yang relevan dengan pelaksanaan kontrak.

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

Apa spesifikasi formal?

Sebuah spesifikasi hanyalah kebutuhan teknis yang harus dipenuhi oleh sistem tertentu. Dalam pemrograman, spesifikasi mewakili gagasan umum tentang eksekusi program (yaitu, apa yang seharusnya dilakukan program).

Dalam konteks kontrak pintar, spesifikasi formal mengacu pada properti—deskripsi formal dari persyaratan yang harus dipenuhi oleh sebuah kontrak. Properti tersebut dijelaskan sebagai "invarian" dan mewakili pernyataan logis tentang eksekusi kontrak yang harus tetap benar dalam setiap keadaan mungkin, tanpa pengecualian apapun.

Oleh karena itu, kita dapat menganggap spesifikasi formal sebagai kumpulan pernyataan yang ditulis dalam bahasa formal yang menggambarkan pelaksanaan yang dimaksud dari kontrak pintar. Spesifikasi mencakup properti kontrak dan mendefinisikan bagaimana kontrak seharusnya berperilaku dalam berbagai keadaan. Tujuan verifikasi formal adalah untuk menentukan apakah kontrak pintar memiliki properti (invarian) ini dan bahwa properti ini tidak dilanggar selama pelaksanaan.

Spesifikasi formal sangat penting dalam mengembangkan implementasi yang aman dari kontrak pintar. Kontrak yang gagal menerapkan invarian atau melanggar propertinya selama eksekusi rentan terhadap kerentanan yang dapat merusak fungsionalitas atau menyebabkan eksploitasi jahat.

JENIS-JENIS SPESIFIKASI FORMAL UNTUK KONTRAK CERDAS

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 dibuat dengan menggunakan elemen-elemen dari logika program

(dibuka di tab baru)

, yang memungkinkan penalaran formal tentang sifat-sifat dari sebuah program. Logika program memiliki aturan formal yang menyatakan (dalam bahasa matematika) perilaku yang diharapkan dari sebuah program. Berbagai logika program digunakan dalam menciptakan spesifikasi formal, termasuk logika keterjangkauan

(terbuka di tab baru)

logika temporal

(opens in a new tab)

danlogika Hoare

(buka di tab baru)

Spesifikasi formal untuk kontrak pintar dapat diklasifikasikan secara luas sebagai spesifikasi tingkat tinggi atau tingkat rendah. Terlepas dari kategori spesifikasi mana yang termasuk, itu harus memadai dan dengan jelas menjelaskan properti sistem yang sedang dianalisis.

Spesifikasi tingkat tinggi

Sesuai dengan namanya, spesifikasi tingkat tinggi (juga disebut sebagai “spesifikasi berorientasi model”) menggambarkan perilaku tingkat tinggi dari sebuah program. Spesifikasi tingkat tinggi memodelkan kontrak pintar sebagai sebuah mesin keadaan terbatas

(buka di tab baru)

(FSM), yang dapat bertransisi antara keadaan dengan melakukan operasi, dengan logika temporal digunakan untuk mendefinisikan properti formal untuk model FSM.

logika temporal

(buka di tab baru)

adalah "aturan untuk penalaran tentang proposisi yang memenuhi syarat dalam hal waktu (misalnya, "Saya selalu lapar" atau "Saya akhirnya akan lapar")." Ketika diterapkan pada verifikasi formal, logika temporal digunakan untuk menyatakan pernyataan tentang perilaku yang benar dari sistem yang dimodelkan sebagai mesin negara. Secara khusus, logika temporal menggambarkan keadaan masa depan kontrak pintar dan bagaimana transisi antar negara.

Spesifikasi tingkat tinggi umumnya menangkap dua properti temporal kritis untuk kontrak pintar: keselamatan dan kelangsungan hidup. Properti keselamatan mewakili gagasan bahwa "tidak ada yang buruk pernah terjadi" dan biasanya menyatakan invariansi. Sebuah properti keselamatan mungkin mendefinisikan persyaratan perangkat lunak umum, seperti bebas dari kebuntuan

(opens in a a new tab)

, atau mengekspresikan properti domain khusus untuk kontrak (misalnya, invarian pada kontrol akses untuk fungsi, nilai-nilai yang diizinkan dari variabel status, atau kondisi untuk transfer token).

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

Properti kehidupan menegaskan bahwa “akhirnya sesuatu yang baik terjadi” dan berkaitan dengan kemampuan kontrak untuk berkembang melalui berbagai keadaan. Contoh dari properti kehidupan adalah “likuiditas”, yang mengacu pada kemampuan kontrak untuk mentransfer saldo kepada pengguna atas permintaan. Jika properti ini dilanggar, pengguna tidak akan dapat menarik aset yang disimpan di kontrak, seperti yang terjadi dengan Insiden dompet Parity

(buka di tab baru)

.

Spesifikasi tingkat rendah

Spesifikasi tingkat tinggi dimulai dari model keadaan terbatas dari kontrak dan mendefinisikan properti yang diinginkan dari model ini. Sebaliknya, spesifikasi tingkat rendah (juga disebut sebagai 'spesifikasi berorientasi properti') sering kali 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 berusaha mendefinisikan properti dari kontrak pintar di atas jejak tersebut. Jejak merujuk pada urutan eksekusi fungsi yang mengubah status kontrak pintar; oleh karena itu, spesifikasi tingkat rendah membantu menentukan persyaratan untuk eksekusi internal kontrak.

Spesifikasi formal tingkat rendah dapat diberikan sebagai properti gaya Hoare atau invarian pada lintasan eksekusi.

properti gaya Hoare

Logika Hoare

(buka di tab baru)

memberikan seperangkat aturan formal untuk penalaran tentang kebenaran program, termasuk kontrak pintar. Sebuah properti gaya Hoare direpresentasikan oleh triplet Hoare {P}c{Q}, di mana c adalah sebuah program dan P dan Q adalah predikat pada keadaan c (yaitu, program), secara formal dijelaskan sebagai prasyarat dan pascasyarat, masing-masing.

Sebuah prasyarat adalah predikat yang menggambarkan kondisi yang diperlukan untuk eksekusi yang benar dari sebuah fungsi; pengguna yang memanggil kontrak harus memenuhi persyaratan ini. Sebuah postkondisi adalah predikat yang menggambarkan kondisi yang sebuah fungsi tetapkan 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 gaya Hoare dapat menjamin kebenaran parsial atau kebenaran total. Implementasi fungsi kontrak adalah "sebagian benar" jika prasyarat berlaku sebelum fungsi dijalankan, dan jika eksekusi berakhir, postcondition juga benar. Bukti kebenaran total diperoleh jika prasyarat benar sebelum fungsi dijalankan, eksekusi dijamin untuk berakhir dan ketika itu terjadi, postcondition berlaku.

Mendapatkan bukti kebenaran total sulit karena beberapa eksekusi mungkin mengalami penundaan sebelum berakhir, atau bahkan tidak pernah berakhir sama sekali. Namun, pertanyaan apakah eksekusi berakhir secara argumen adalah sebuah titik yang tidak penting karena mekanisme gas Ethereum mencegah perulangan program tak terbatas (eksekusi berakhir dengan sukses atau berakhir karena kesalahan 'kehabisan gas').

Spesifikasi kontrak pintar yang dibuat menggunakan logika Hoare akan memiliki pra kondisi, pasca kondisi, dan invarian yang ditentukan untuk eksekusi fungsi dan perulangan dalam kontrak. Pra kondisi sering kali mencakup kemungkinan input yang salah ke fungsi, dengan pasca kondisi yang menggambarkan respons yang diharapkan terhadap input tersebut (misalnya, melempar pengecualian tertentu). Dengan cara ini, properti gaya Hoare efektif untuk menjamin kebenaran implementasi kontrak.

Banyak kerangka verifikasi formal menggunakan spesifikasi gaya Hoare untuk membuktikan kebenaran semantik dari fungsi. Juga memungkinkan untuk menambahkan properti gaya Hoare (sebagai asersi) langsung ke kode kontrak dengan menggunakan pernyataan require dan assert dalam Solidity.

pernyataan require menyatakan sebuah prasyarat atau invarian dan sering digunakan untuk memvalidasi input pengguna, sementara assert menangkap sebuah posyondisi yang diperlukan untuk keamanan. Misalnya, kontrol akses yang tepat untuk fungsi (sebagai contoh dari properti keamanan) dapat dicapai dengan menggunakan require sebagai pemeriksaan prasyarat pada identitas akun yang memanggil. Demikian pula, sebuah invarian pada nilai-nilai yang diizinkan dari variabel-variabel keadaan dalam kontrak (misalnya, jumlah total token yang beredar) dapat dilindungi dari pelanggaran dengan menggunakan assert untuk mengkonfirmasi keadaan kontrak setelah eksekusi fungsi.

Properti tingkat jejak

Spesifikasi berbasis jejak menggambarkan operasi yang mengalihkan kontrak antara berbagai keadaan dan hubungan antara operasi-operasi tersebut. Seperti yang dijelaskan sebelumnya, jejak adalah urutan operasi yang mengubah keadaan kontrak dengan cara tertentu.

Pendekatan ini bergantung pada model kontrak pintar sebagai sistem transisi status dengan beberapa status yang telah ditentukan (dijelaskan oleh variabel status) bersama dengan serangkaian transisi yang telah ditentukan (dijelaskan oleh fungsi kontrak). Selain itu, grafik aliran kontrol

(buka di tab baru)

(CFG), yang merupakan representasi grafis dari alur eksekusi program, sering digunakan untuk menjelaskan semantik operasional dari kontrak. Di sini, setiap jejak direpresentasikan sebagai jalur pada graf alur kontrol.

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

Mari kita gunakan contoh dari sebuahDAOkontrak yang memiliki beberapa fungsi yang dapat diakses secara publik untuk menggambarkan properti tingkat jejak. Di sini, kita mengasumsikan kontrak DAO memungkinkan pengguna untuk melakukan operasi berikut:

• Menyetor dana
• Memilih suara pada proposal setelah mendepositkan dana
• Klaim pengembalian dana jika mereka tidak memberikan suara pada proposal

Properti tingkat jejak contoh bisa menjadi "pengguna yang tidak melakukan deposit tidak dapat memberikan suara pada proposal" atau "pengguna yang tidak memberikan suara pada proposal seharusnya selalu dapat melakukan klaim pengembalian dana". Kedua properti menegaskan urutan eksekusi yang diinginkan (pengambilan suara tidak dapat terjadi sebelum melakukan deposit dan klaim pengembalian dana tidak dapat terjadi setelah memberikan suara pada proposal).

TEKNIK VERIFIKASI FORMAL KONTRAK PINTAR

Pemeriksaan model

Model checking adalah teknik verifikasi formal di mana sebuah algoritma memeriksa model formal dari kontrak pintar terhadap spesifikasinya. Dalam model checking, kontrak pintar sering kali direpresentasikan sebagai sistem transisi keadaan, sementara properti pada keadaan kontrak yang diperbolehkan didefinisikan menggunakan logika temporal.

Model checking memerlukan membuat representasi matematis abstrak dari sebuah sistem (yaitu, sebuah kontrak) dan mengekspresikan properti dari sistem ini menggunakan rumus yang berakar dalam logika proposisional

(buka di tab baru)

. Hal ini menyederhanakan tugas algoritma pemeriksaan model, yaitu membuktikan bahwa sebuah model matematika memenuhi formula logis 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 meliputi keselamatan dan keberlangsungan hidup, yang telah kami jelaskan sebelumnya.

Sebagai contoh, 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.

Model checking menggunakan eksplorasi ruang keadaan, yang melibatkan konstruksi semua kemungkinan keadaan dari sebuah kontrak pintar dan berupaya untuk menemukan keadaan yang dapat dicapai yang mengakibatkan pelanggaran properti. Namun, hal ini dapat menyebabkan jumlah keadaan yang tak terbatas (dikenal sebagai "masalah ledakan keadaan"), oleh karena itu pengecek model mengandalkan teknik abstraksi untuk membuat analisis kontrak pintar menjadi mungkin secara efisien.

Pembuktian teorema

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

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

Hubungan yang diperlukan (ekivalensi logis) antara pernyataan tentang model kontrak dan propertinya diformulasikan sebagai pernyataan yang dapat dibuktikan (disebut teorema). Dengan menggunakan sistem formal inferensi, pembuktian teorema otomatis dapat memverifikasi validitas teorema. Dengan kata lain, pembuktian teorema dapat membuktikan dengan pasti bahwa model kontrak pintar sesuai dengan spesifikasinya.

Saat memeriksa model kontrak sebagai sistem transisi dengan keadaan terbatas, pembuktian teorema dapat menangani analisis sistem berkeadaan tak terbatas. Namun, hal ini berarti pembuktian teorema otomatis tidak selalu tahu apakah masalah logika tersebut "dapat diputuskan" atau tidak.

Sebagai hasilnya, bantuan manusia sering diperlukan untuk memandu pengoreksi teorema dalam menurunkan bukti kebenaran. Penggunaan upaya manusia dalam pembuktian teorema membuatnya lebih mahal untuk digunakan daripada pemeriksaan model, yang sepenuhnya otomatis.

Eksekusi simbolis

Simulasi simbolik adalah metode menganalisis kontrak pintar dengan menjalankan fungsi menggunakan nilai simbolik (misalnya, x > 5) daripada nilai konkret (misalnya, x == 5). Sebagai teknik verifikasi formal, simulasi simbolik digunakan untuk meresahkan secara formal tentang properti tingkat jejak dalam kode kontrak.

Eksekusi simbolis mewakili jejak eksekusi sebagai formula matematika atas nilai input simbolis, juga disebut predikat jalur. Sebuahsolver SMT

(opens in a new tab)

digunakan untuk memeriksa apakah predikat jalur “memuaskan” (yaitu, ada nilai yang dapat memenuhi rumus). Jika jalur yang rentan memuaskan, solver SMT akan menghasilkan nilai konkret yang memicu eksekusi menuju jalur tersebut.

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

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

Karena eksekusi simbolis bergantung pada input ke program, dan himpunan input untuk menjelajahi semua keadaan yang dapat dicapai secara potensial tak terbatas, ini masih merupakan bentuk pengujian. Namun, seperti yang ditunjukkan dalam contoh, eksekusi simbolis lebih efisien daripada pengujian reguler untuk menemukan input yang memicu pelanggaran properti.

Selain itu, eksekusi simbolis menghasilkan lebih sedikit positif palsu daripada teknik berbasis properti lainnya (mis., fuzzing) yang secara acak menghasilkan input ke fungsi. Jika keadaan kesalahan dipicu selama eksekusi simbolis, maka mungkin untuk menghasilkan nilai konkret yang memicu kesalahan dan mereproduksi isu tersebut.

Eksekusi simbolis juga dapat memberikan sejumlah derajat bukti matematis tentang kebenaran. Pertimbangkan contoh berikut dari fungsi kontrak dengan perlindungan overflow:

Jejak eksekusi yang menghasilkan integer overflow perlu memenuhi rumus: z = x + y DAN (z >= x) DAN (z=>y) DAN (z < x ATAU z < y) Sebuah rumus seperti itu kemungkinan kecil untuk dipecahkan, oleh karena itu ini merupakan bukti matematis bahwa fungsi safe_add tidak pernah overflow.

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 keuangan. Kontrak pintar adalah aplikasi bernilai tinggi yang mengendalikan jumlah nilai yang sangat besar, dan kesalahan sederhana dalam desain dapat menyebabkan kerugian yang tidak dapat dipulihkan bagi pengguna

(buka di tab baru)

Secara formal memverifikasi kontrak sebelum dideploy, namun, dapat meningkatkan jaminan bahwa kontrak akan berjalan sesuai yang diharapkan di blockchain.

Keandalan adalah kualitas yang sangat diinginkan dalam kontrak pintar manapun, terutama karena kode yang diterapkan dalam Mesin Virtual Ethereum (EVM) umumnya tidak berubah. Dengan upgrade setelah peluncuran tidak mudah diakses, kebutuhan untuk menjamin keandalan kontrak membuat verifikasi formal diperlukan. Verifikasi formal mampu mendeteksi isu-isu rumit, seperti underflows dan overflow bilangan bulat, re-entrancy, dan optimasi gas yang buruk, yang mungkin lolos dari pemeriksa dan pengujian.

Buktikan kebenaran fungsionalitas

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

Namun, pendekatan ini tidak bisa membuktikan eksekusi yang benar untuk nilai input yang tidak termasuk dalam sampel. Oleh karena itu, pengujian kontrak dapat membantu mendeteksi bug (yaitu, jika beberapa jalur kode gagal mengembalikan hasil yang diinginkan selama eksekusi), tetapi tidak dapat membuktikan secara konklusif ketiadaan 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 pengembangan model formal (matematis) dari sistem kontrak. Kemudian kita dapat mengikuti prosedur bukti formal untuk memeriksa konsistensi antara model kontrak dan spesifikasinya.

Dengan verifikasi formal, pertanyaan tentang memverifikasi apakah logika bisnis kontrak memenuhi persyaratan adalah proposisi matematis yang dapat dibuktikan atau dibantah. 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 sebuah kontrak secara fungsional benar dengan spesifikasi yang ada.

Target verifikasi ideal

Sebuah target verifikasi menggambarkan sistem yang akan diverifikasi secara formal. Verifikasi formal paling baik digunakan dalam “sistem tertanam” (potongan perangkat lunak kecil dan sederhana yang merupakan bagian dari sistem yang lebih besar). Mereka juga ideal untuk domain khusus yang memiliki sedikit aturan, karena ini memudahkan untuk memodifikasi alat verifikasi properti domain-spesifik.

Kontrak pintar — setidaknya, sampai batas tertentu — memenuhi kedua persyaratan tersebut. Misalnya, ukuran kecil kontrak Ethereum membuat mereka setuju untuk verifikasi formal. Demikian pula, EVM mengikuti aturan sederhana, yang membuat menentukan dan memverifikasi properti semantik untuk program yang berjalan di EVM 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-nilai simbolis untuk menguji asersi ("bagaimana jika pengguna mencoba menarik n ether?") berbeda dengan pengujian yang menggunakan nilai konkret ("bagaimana jika pengguna mencoba menarik 5 ether?").

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

Verifikasi formal juga meningkatkan proses pembangunan aplikasi terdesentralisasi (dapps) dengan mengurangi kesalahan desain yang mahal. Memperbarui kontrak (jika memungkinkan) untuk memperbaiki kerentanan memerlukan penulisan ulang kode yang luas dan lebih banyak usaha yang dihabiskan pada pengembangan. Verifikasi formal dapat mendeteksi banyak kesalahan dalam implementasi kontrak yang mungkin lolos dari pengujian dan pemeriksaan dan memberikan kesempatan yang cukup untuk memperbaiki masalah tersebut sebelum menerapkan kontrak.

KEKURANGAN VERIFIKASI FORMAL

Biaya tenaga kerja manual

Verifikasi formal, khususnya verifikasi semi-otomatis di mana seorang manusia memandu pemberi bukti untuk menurunkan bukti kebenaran, memerlukan tenaga kerja manual yang cukup banyak. Selain itu, menciptakan spesifikasi formal adalah aktivitas yang kompleks yang menuntut tingkat keterampilan yang tinggi.

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

Negatif palsu

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

Jika spesifikasi ditulis dengan buruk, pelanggaran properti—yang menunjukkan eksekusi yang rentan—tidak dapat dideteksi oleh audit verifikasi formal. Dalam kasus ini, seorang pengembang mungkin dengan keliru menganggap bahwa kontrak tersebut bebas dari bug.

Masalah kinerja

Verifikasi formal menghadapi sejumlah masalah kinerja. Sebagai contoh, masalah ledakan status dan jalur yang dihadapi saat pemeriksaan model dan pemeriksaan simbolis, masing-masing, dapat memengaruhi prosedur verifikasi. Selain itu, alat verifikasi formal sering menggunakan pemecah SMT dan pemecah kendala lainnya dalam lapisan dasarnya, dan pemecah-pemecah ini bergantung pada prosedur yang intensif secara komputasi.

Selain itu, tidak selalu mungkin bagi verifikasi program untuk menentukan apakah properti (yang dijelaskan sebagai formula logis) dapat dipenuhi atau tidak (yang masalah keputusan

(buka di tab baru)

Karena sebuah program mungkin tidak pernah berakhir. Dengan demikian, mungkin tidak mungkin untuk membuktikan beberapa properti untuk sebuah kontrak bahkan jika itu sudah dijelaskan dengan baik.

ALAT VERIFIKASI FORMAL UNTUK KONTRAK PINTAR ETHEREUM

Bahasa spesifikasi untuk membuat spesifikasi formal

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

• GitHub
• (buka di tab baru)
• Dokumentasi
• (opens in a new tab)

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

• Dokumentasi
• (buka di tab baru)

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

• GitHub
• (buka di tab baru)

Program verifiers for checking correctness

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

• Website
• (buka di tab baru)
• Dokumentasi
• (buka di tab baru)

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

• GitHub
• (buka di tab baru)

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

• GitHub
• (opens in a new tab)

KEVM - KEVM adalah semantik formal dari Mesin Virtual Ethereum (EVM) yang ditulis dalam kerangka K. KEVM dapat dieksekusi dan dapat membuktikan beberapa pernyataan terkait properti menggunakan logika jangkauan.

• GitHub
• (opens in a new tab)
• Dokumentasi
• (buka di tab baru)

Kerangka kerja logis untuk pembuktian teorema

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

• GitHub
• (buka di tab baru)
• Dokumentasi
• (opens in a new tab)

Coq - Coq adalah pembuktian teorema interaktif yang memungkinkan Anda mendefinisikan program menggunakan teorema dan menghasilkan bukti kebenaran yang diperiksa mesin secara interaktif.

• GitHub
• (buka di tab baru)
• Dokumentasi
• (buka di tab baru)

Alat berbasis eksekusi simbolik untuk mendeteksi pola rentan dalam kontrak pintar

Manticore - Sebuah alat untuk menganalisis alat analisis bytecode EVM berdasarkan eksekusi simbolik.

• GitHub
• (buka di tab baru)
• Dokumentasi
• (buka di tab baru)

hevm - hevm adalah mesin eksekusi simbolik dan pemeriksa kesetaraan untuk bytecode EVM.

• GitHub
• (buka di tab baru)

Mythril - Sebuah alat eksekusi simbolik untuk mendeteksi kerentanan dalam kontrak pintar Ethereum

• GitHub
• (buka di tab baru)
• Dokumentasi
• (buka di tab baru)

Disclaimer：

1. Artikel ini dicetak ulang dari [ ]. Semua hak cipta dimiliki oleh penulis asli [**]. Jika ada keberatan terhadap cetakan ulang ini, silakan hubungi Gate Belajartim, dan mereka akan menanganinya dengan segera.
2. Penolakan Tanggung Jawab Kewajiban: Pandangan dan opini yang terdapat dalam artikel ini semata-mata milik penulis dan tidak merupakan saran investasi apa pun.
3. Terjemahan artikel ke dalam bahasa lain dilakukan oleh tim Gate Learn. Kecuali disebutkan, menyalin, mendistribusikan, atau menjiplak artikel yang diterjemahkan dilarang.