Artikel ini merupakan kontribusi komunitas. Penulis: Dimitris Tsabis, Wakil Presiden Teknik di CertiK, perusahaan audit kontrak pintar Web3.
Singkatnya
Verifikasi formal kontrak pintar memastikan bahwa kontrak tersebut bebas dari bug, kerentanan, dan perilaku tidak diinginkan lainnya. Proses ini melibatkan seorang pakar manusia yang merepresentasikan logika kontrak pintar dalam bentuk matematika, kemudian menjalankannya melalui proses otomatis untuk memverifikasi logika aktual terhadap model perilaku kontrak yang diharapkan. Kombinasi verifikasi formal dan audit manual memberikan penilaian komprehensif terhadap keamanan kontrak pintar.
pengantar
Kontrak pintar adalah program komputer yang diterapkan pada blockchain yang secara otomatis dijalankan ketika kondisi tertentu terpenuhi. Kontrak pintar berkisar dari yang sederhana hingga yang kompleks dan dapat menyimpan aset senilai miliaran dolar.
Kerentanan keamanan dalam kode kontrak pintar dapat menimbulkan konsekuensi yang menghancurkan, termasuk pencurian semua aset yang dimiliki oleh kontrak pintar tersebut. Pada tahun 2021, perusahaan pembuat pasar otomatis Uranium Finance mengalami pencurian senilai $50 juta karena satu kesalahan ketik dalam sebuah kontrak pintar.
Pada tahun 2021, protokol Compound Finance juga mengeluarkan $80 juta dalam bentuk imbalan yang tidak diperoleh karena satu bug kode. Pada tahun 2022, $320 juta dicuri dari Wormhole Bridge karena kesalahan pemrograman di salah satu kontrak pintarnya.
Sangat penting untuk mendapatkan perangkat lunak kontrak pintar yang tepat sejak awal. Kontrak pintar bersifat sumber terbuka, artinya kodenya tersedia untuk umum segera setelah kontrak dipublikasikan. Jika peretas menemukan bug, mereka dapat langsung mengeksploitasinya. Selain itu, mengatasi kerentanan keamanan secara berkala bukanlah suatu pilihan, karena kode kontrak pintar biasanya tidak dapat dimodifikasi setelah dipublikasikan.
Bagaimana cara kerja verifikasi kontrak pintar?
Verifikasi formal kontrak pintar bekerja dengan merepresentasikan logika dan perilaku yang diinginkan dari kontrak pintar dalam bentuk data matematika. Auditor dapat menggunakan alat otomatis untuk memverifikasi validitas data.
Prosesnya meliputi hal berikut:
Tentukan spesifikasi dan karakteristik kontrak yang diinginkan dalam bahasa formal.
Menerjemahkan kode kontrak ke dalam presentasi formal, seperti model atau kerangka logika matematika.
Menggunakan alat pembuktian teorema atau pemeriksaan model untuk memverifikasi spesifikasi dan properti kontrak.
Ulangi proses verifikasi untuk menemukan dan memperbaiki kesalahan atau penyimpangan dari karakteristik yang diperlukan.
Mengapa verifikasi kontrak pintar penting?
Penggunaan penalaran matematika membantu memastikan bahwa kontrak pintar yang diverifikasi secara formal bebas dari bug, kerentanan, dan perilaku tidak diinginkan lainnya. Hal ini juga membantu meningkatkan kepercayaan terhadap kontrak, karena propertinya telah diverifikasi secara akurat.
Berikut adalah beberapa contoh bagaimana verifikasi kontrak pintar dapat membantu mencegah kerugian finansial yang besar dan hasil buruk lainnya.
Uniswap
Uniswap adalah pembuat pasar otomatis yang terkenal. Saat kontrak pintar Uniswap V1 dikembangkan, kontrak tersebut menjalani verifikasi formal. Sebelum diluncurkan, proses verifikasi formal ini mengidentifikasi dan mengoreksi kesalahan pembulatan yang dapat menyebabkan pencurian dana Uniswap V1.
Pengimbang
Balancer V2 juga merupakan pembuat pasar otomatis yang terverifikasi secara formal. Proses verifikasi formal mengidentifikasi dan memperbaiki perhitungan biaya yang salah, serta menyertakan fungsi pinjaman kilat dalam kontrak pintar, yang berpotensi membuat platform perdagangan rentan terhadap risiko pencurian.
SafeMoon
SafeMoon V1 mengandung bug kecil yang ditemukan melalui verifikasi formal setelah dirilis. Pemilik dapat saja melepaskan kepemilikan kontrak dan mengklaimnya kembali jika tindakan tertentu dilakukan sebelum melepaskan kepemilikan.
Bug ini tidak terdeteksi selama sebagian besar audit manual fork SafeMoon V1 karena untuk menemukannya diperlukan analisis terhadap serangkaian variabel program tertentu. Hal ini mudah terlewatkan oleh manusia, tetapi mudah ditemukan oleh mesin.
Bagaimana verifikasi formal dan audit manual bekerja bersama
Verifikasi formal menyediakan cara sistematis dan otomatis untuk memeriksa logika dan perilaku kontrak terhadap properti yang diinginkan. Hal ini memudahkan identifikasi dan perbaikan potensi kesalahan atau bug. Verifikasi formal sangat berguna untuk menemukan masalah kompleks dan tersembunyi yang mungkin sulit dideteksi selama inspeksi manual.
Proses audit manual melibatkan peninjauan oleh para ahli atas kode kontrak, desain, dan penerapannya. Auditor menggunakan keahlian mereka untuk mengidentifikasi risiko keamanan dan menilai postur keamanan kontrak secara keseluruhan. Mereka juga memastikan bahwa proses verifikasi formal diselesaikan dengan benar dan memeriksa masalah apa pun yang mungkin tidak terdeteksi oleh alat otomatis.
Menggabungkan verifikasi formal dengan audit manual menghasilkan penilaian keamanan kontrak pintar yang komprehensif. Hal ini meningkatkan kemungkinan menemukan dan mengatasi kerentanan apa pun. Hasilnya adalah pendekatan pertahanan keamanan berlapis yang memanfaatkan kemampuan unik manusia dan mesin.
Pikiran penutup
Untuk memastikan keamanan kontrak pintar, perlu menggunakan verifikasi formal dan audit manual untuk memastikan penilaian yang komprehensif dan akurat terhadap status keamanan kontrak pintar.
Meskipun verifikasi formal mungkin membutuhkan banyak sumber daya, hal ini merupakan investasi yang berharga untuk kontrak pintar bernilai tinggi atau berisiko tinggi. Terakhir, memprioritaskan keamanan dan memastikan kontrak pintar bebas dari bug, kerentanan, dan perilaku tidak diinginkan lainnya sangatlah penting.
Artikel terkait
Apa itu kontrak pintar?
Apa itu audit keamanan kontrak pintar?
Penafian dan Peringatan Risiko: Konten ini disediakan "sebagaimana adanya" hanya untuk informasi umum dan tujuan edukasi, tanpa pernyataan atau jaminan apa pun. Konten ini tidak boleh ditafsirkan sebagai nasihat keuangan dan tidak dimaksudkan sebagai rekomendasi untuk membeli produk atau layanan tertentu. Harga aset digital dapat berfluktuasi. Nilai investasi Anda dapat naik atau turun, dan Anda mungkin tidak mendapatkan kembali jumlah yang Anda investasikan. Anda sendiri yang bertanggung jawab atas keputusan investasi Anda, dan Binance Academy tidak bertanggung jawab atas kerugian apa pun yang mungkin Anda alami. Ini bukan nasihat keuangan.