Artikel ini adalah kiriman komunitas. Penulisnya adalah David Tarditi, VP of Engineering di CertiK, sebuah firma audit kontrak pintar Web3.
Pandangan dalam artikel ini adalah milik kontributor/penulis dan tidak mencerminkan pandangan Binance Academy.
TL;DR
Verifikasi formal atas kontrak pintar memastikan kontrak tersebut bebas dari bug, kerentanan, dan perilaku tidak diinginkan lainnya. Hal ini melibatkan pakar manusia yang menyajikan logika kontrak cerdas sebagai pernyataan matematis, kemudian menjalankannya melalui proses otomatis yang memeriksa logika aktual terhadap model perilaku kontrak yang diharapkan. Kombinasi verifikasi formal dan audit manual memberikan evaluasi komprehensif terhadap keamanan kontrak pintar.
Perkenalan
Kontrak pintar adalah program komputer yang diterapkan pada blockchain yang berjalan secara otomatis ketika kondisi tertentu terpenuhi. Mulai dari yang sederhana hingga yang sangat kompleks, dan dapat memiliki aset bernilai jutaan atau bahkan miliaran dolar.
Kerentanan keamanan dalam kode kontrak pintar dapat menimbulkan konsekuensi yang menghancurkan, termasuk pencurian semua aset yang dimiliki oleh kontrak pintar. Pada tahun 2021, pembuat pasar otomatis (AMM) Uranium Finance telah mencuri $50 juta karena satu kesalahan ketik dalam kontrak pintar.
Juga pada tahun 2021, Compound Finance memberikan $80 juta hadiah yang belum diterima karena satu kesalahan karakter. Pada tahun 2022, $320 juta dicuri dari Wormhole Bridge karena bug di salah satu kontrak pintarnya.
Penting untuk menjalankan program kontrak pintar dengan benar pada kali pertama. Kontrak pintar bersifat sumber terbuka, artinya kode tersedia untuk umum setelah kontrak diterapkan. Jika seorang hacker menemukan bug, mereka dapat langsung memanfaatkannya. Selain itu, menambal kerentanan keamanan dari waktu ke waktu bukanlah suatu pilihan, karena kode kontrak pintar biasanya tidak dapat diubah setelah penerapan.
Bagaimana Cara Kerja Verifikasi Kontrak Cerdas?
Verifikasi formal kontrak pintar bekerja dengan menyajikan logika dan perilaku kontrak pintar yang diinginkan sebagai pernyataan matematis. Auditor kemudian menggunakan alat otomatis untuk memeriksa apakah pernyataan ini benar.
Prosesnya melibatkan:
Mendefinisikan spesifikasi dan properti yang diinginkan dari suatu kontrak dalam bahasa formal.
Menerjemahkan kode kontrak ke dalam representasi formal, seperti model matematika atau logika.
Menggunakan pembukti teorema otomatis atau pemeriksa model untuk memvalidasi spesifikasi dan properti kontrak.
Mengulangi proses verifikasi untuk menemukan dan memperbaiki kesalahan atau penyimpangan dari properti yang diinginkan.
Mengapa Verifikasi Kontrak Cerdas Itu Penting
Penggunaan penalaran matematis membantu memastikan bahwa kontrak pintar yang diverifikasi secara formal bebas dari bug, kerentanan, dan perilaku tidak diinginkan lainnya. Hal ini juga membantu meningkatkan kepercayaan dan keyakinan terhadap kontrak, karena propertinya telah terbukti benar secara ketat.
Di bawah ini adalah beberapa contoh bagaimana verifikasi kontrak pintar telah membantu mencegah kerugian finansial yang signifikan dan akibat buruk lainnya.
Tidak bertukar tempat
Uniswap adalah AMM yang terkenal. Ketika kontrak pintar Uniswap V1 dikembangkan, kontrak tersebut diverifikasi secara resmi. Sebelum dirilis, verifikasi formal ini menemukan dan memperbaiki kesalahan pembulatan yang dapat menyebabkan Uniswap V1 terkuras dana.
Pengimbang
Balancer V2 juga merupakan AMM yang telah diverifikasi secara resmi. Verifikasi formal menemukan dan memperbaiki kesalahan penghitungan biaya yang melibatkan fungsi pinjaman kilat dalam kontrak pintar, yang dapat membuat bursa rentan terhadap pencurian.
Bulan Aman
SafeMoon V1 berisi bug halus yang ditemukan melalui verifikasi formal setelah diterapkan. Pemilik dapat melepaskan kepemilikan atas kontrak dan kemudian memperolehnya kembali, jika operasi tertentu dilakukan sebelum melepaskan kepemilikan.
Bug ini terlewatkan di sebagian besar audit manual fork SafeMoon V1 karena untuk menemukannya diperlukan analisis kombinasi spesifik dari nilai variabel program. Ini adalah sesuatu yang mudah dilewatkan oleh manusia, dan mudah dipahami oleh mesin.
Bagaimana Verifikasi Formal dan Audit Manual Bekerja Sama
Verifikasi formal menyediakan cara sistematis dan otomatis untuk memeriksa logika dan perilaku kontrak terhadap properti yang diinginkan. Hal ini memudahkan untuk mengidentifikasi dan memperbaiki potensi kesalahan atau bug. Hal ini sangat berguna untuk menemukan masalah rumit dan tidak kentara yang mungkin sulit dideteksi melalui inspeksi manual.
Audit manual melibatkan tinjauan ahli atas kode kontrak, desain, dan penerapan. Auditor menggunakan pengalaman dan keahlian mereka untuk mengidentifikasi risiko keamanan dan mengevaluasi keseluruhan postur keamanan kontrak. Mereka juga dapat mengonfirmasi bahwa proses verifikasi formal telah dilakukan dengan benar, dan memeriksa masalah apa pun yang mungkin tidak dapat dideteksi oleh alat otomatis.
Menggabungkan verifikasi formal dan audit manual memberikan evaluasi yang komprehensif dan menyeluruh terhadap keamanan kontrak pintar. Hal ini meningkatkan kemungkinan menemukan dan memperbaiki kerentanan apa pun. Hasilnya adalah pendekatan pertahanan mendalam terhadap keamanan yang memanfaatkan kemampuan unik manusia dan mesin.
Menutup Pikiran
Untuk memastikan keamanan kontrak pintar, penting untuk menggunakan verifikasi formal dan audit manual untuk memastikan evaluasi yang komprehensif dan menyeluruh terhadap postur keamanan kontrak pintar.
Meskipun verifikasi formal membutuhkan banyak sumber daya, verifikasi ini merupakan investasi yang bermanfaat untuk kontrak dengan nilai tinggi atau faktor risiko tinggi. Pada akhirnya, memprioritaskan keamanan dan memastikan kontrak pintar bebas dari bug, kerentanan, dan perilaku yang tidak diinginkan sangatlah penting.
Bacaan lebih lanjut
Apa itu Kontrak Cerdas?
Apa Itu Audit Keamanan Kontrak Cerdas?
Penafian dan Peringatan Risiko: Konten ini disajikan kepada Anda “sebagaimana adanya” hanya untuk informasi umum dan tujuan pendidikan, tanpa representasi atau jaminan apa pun. Hal ini tidak boleh ditafsirkan sebagai nasihat keuangan, hukum, atau profesional lainnya, juga tidak dimaksudkan untuk merekomendasikan pembelian produk atau layanan tertentu. Anda harus mencari nasihat Anda sendiri dari penasihat profesional yang tepat. Apabila artikel tersebut dikontribusikan oleh kontributor pihak ketiga, harap dicatat bahwa pandangan yang diungkapkan adalah milik kontributor pihak ketiga, dan tidak mencerminkan pandangan Binance Academy. Silakan baca penafian lengkap kami di sini untuk rincian lebih lanjut. Harga aset digital bisa berfluktuasi. Nilai investasi Anda mungkin turun atau naik dan Anda mungkin tidak mendapatkan kembali jumlah yang diinvestasikan. Anda sepenuhnya bertanggung jawab atas keputusan investasi Anda dan Binance Academy tidak bertanggung jawab atas kerugian apa pun yang mungkin Anda alami. Materi ini tidak boleh ditafsirkan sebagai nasihat keuangan, hukum, atau nasihat profesional lainnya. Untuk informasi lebih lanjut, lihat Ketentuan Penggunaan dan Peringatan Risiko kami.
