Artikel ini merupakan kiriman dari komunitas. Penulisnya adalah David Tarditi, VP of Engineering di CertiK, yaitu sebuah firma audit smart contract Web3.
Ringkasan
Verifikasi formal memastikan bahwa smart contract bebas dari bug, kerentanan, dan perilaku lainnya yang tidak diinginkan. Dalam prosesnya, seorang ahli menyajikan logika smart contract dalam pernyataan matematis, lalu menjalankannya melalui proses otomatis yang membandingkan logika sebenarnya dengan model perilaku kontrak yang diharapkan. Kombinasi verifikasi formal dan audit manual memberikan evaluasi yang komprehensif terhadap keamanan smart contract.
Pendahuluan
Smart contract adalah program komputer yang diterapkan pada sebuah blockchain yang berjalan secara otomatis ketika kondisi tertentu terpenuhi. Smart contract dapat berkisar dari sederhana hingga sangat kompleks, serta dapat menyimpan aset bernilai jutaan atau bahkan miliaran dolar.
Kerentanan keamanan dalam kode smart contract dapat memiliki konsekuensi yang merugikan, termasuk pencurian semua aset yang disimpan oleh smart contract. Pada tahun 2021, dana milik automated market maker (AMM) Uranium Finance sebesar $50 juta dicuri karena satu saltik dalam sebuah smart contract.
Pada tahun 2021 juga, Compound Finance mengeluarkan $80 juta sebagai reward yang tidak diterima karena kesalahan satu karakter. Pada tahun 2022, $320 juta dicuri dari Wormhole Bridge karena sebuah bug dalam salah satu smart contract.
Penting untuk membuat program smart contract dengan benar di awal. Smart contract memiliki sumber terbuka, artinya kode tersedia secara publik setelah kontrak diterapkan. Jika seorang peretas menemukan bug, dia bisa segera memanfaatkannya. Selain itu, memperbaiki kerentanan keamanan seiring waktu bukan merupakan pilihan yang baik, karena kode smart contract biasanya tidak dapat dimodifikasi setelah diterapkan.
Bagaimana Cara Kerja Verifikasi Smart Contract?
Cara kerja verifikasi formal smart contract adalah dengan menyajikan logika dan perilaku yang diinginkan dari smart contract dalam bentuk pernyataan matematis. Kemudian, auditor menggunakan alat otomatis untuk memastikan bahwa pernyataan tersebut benar.
Prosesnya meliputi:
Menentukan spesifikasi dan karakteristik yang diinginkan dari sebuah kontrak dalam bahasa formal.
Menerjemahkan kode kontrak menjadi representasi formal, seperti model matematis atau logika.
Menggunakan pembukti teorema atau pemeriksa model otomatis untuk memvalidasi spesifikasi dan karakteristik kontrak.
Mengulangi proses verifikasi untuk menemukan dan memperbaiki kesalahan atau penyimpangan dari karakteristik yang diinginkan.
Alasan Pentingnya Verifikasi Smart Contract
Penggunaan penalaran matematis membantu memastikan bahwa smart contract yang telah melalui verifikasi formal bebas dari bug, kerentanan, dan perilaku lainnya yang tidak diinginkan. Hal ini juga membantu meningkatkan kepercayaan dan keyakinan dalam kontrak tersebut, karena karakteristiknya terbukti kuat benar.
Berikut adalah beberapa contoh yang menunjukkan bahwa verifikasi smart contract telah membantu mencegah kerugian finansial yang besar dan dampak merugikan lainnya.
Uniswap
Uniswap merupakan AMM yang ternama. Ketika diterapkan, smart contract Uniswap V1 telah melalui verifikasi formal. Sebelum dirilis, verifikasi formal ini menemukan dan memperbaiki kesalahan pembulatan yang dapat menyebabkan dana Uniswap V1 terkuras.
Balancer
Balancer V2 juga merupakan AMM yang telah melalui verifikasi formal. Verifikasi formal menemukan dan memperbaiki perhitungan biaya yang salah terkait fungsionalitas pinjaman kilat yang dapat membuat bursa rentan terhadap pencurian.
SafeMoon
SafeMoon V1 mengandung bug tak kentara yang ditemukan oleh verifikasi formal setelah diterapkan. Pemilik dapat melepaskan kepemilikan kontrak lalu mendapatkannya kembali jika operasi tertentu dilakukan sebelum melepaskan kepemilikan.
Bug ini terlewatkan dalam sebagian besar audit manual dari fork SafeMoon V1 karena diperlukan analisis kombinasi tertentu dari nilai variabel program untuk menemukannya. Bug ini mudah terlewatkan oleh manusia dan mudah dilacak oleh mesin.
Manfaat Menggabungkan Verifikasi Formal dan Audit Manual
Verifikasi formal menyediakan cara yang sistematis dan otomatis untuk membandingkan logika dan perilaku kontrak dengan karakteristik yang diinginkan darinya. Hal ini memudahkan dalam mengidentifikasi dan memperbaiki kesalahan atau bug potensial. Proses ini sangat berguna untuk menemukan masalah yang kompleks dan tak kentara yang mungkin sulit terdeteksi melalui inspeksi manual.
Dalam audit manual, seorang ahli meninjau kode, desain, dan penerapan sebuah kontrak. Auditor menggunakan pengalaman dan keahliannya untuk mengidentifikasi risiko keamanan dan mengevaluasi keseluruhan kondisi keamanan kontrak. Mereka juga dapat memastikan bahwa proses verifikasi formal telah dilakukan dengan benar dan mencari masalah yang mungkin tidak terdeteksi oleh alat otomatis.
Dengan menggabungkan verifikasi formal dan audit manual, Anda mendapatkan evaluasi yang komprehensif dan menyeluruh terhadap keamanan smart contract. Hal ini meningkatkan peluang untuk menemukan dan memperbaiki kerentanan. Hasilnya adalah pendekatan pertahanan yang mendalam terhadap keamanan yang memanfaatkan kemampuan unik dari manusia dan mesin.
Penutup
Demi memastikan keamanan smart contract, penting untuk menggunakan verifikasi formal dan audit manual guna memastikan evaluasi yang komprehensif dan menyeluruh dari kondisi keamanan smart contract.
Meskipun memerlukan sumber daya yang banyak, verifikasi formal adalah investasi yang sepadan untuk kontrak dengan faktor bernilai tinggi atau berisiko tinggi. Pada akhirnya, memprioritaskan keamanan serta memastikan smart contract bebas dari bug, kerentanan, dan perilaku yang tidak diinginkan adalah hal yang penting.
Bacaan Lebih Lanjut
Penafian dan Peringatan Risiko: Konten ini disajikan kepada Anda dengan dasar “sebagaimana adanya” untuk informasi umum dan tujuan edukasional saja tanpa pernyataan atau jaminan dalam bentuk apa pun. Konten ini tidak boleh dianggap sebagai nasihat keuangan ataupun dimaksudkan untuk menyarankan pembelian produk atau jasa tertentu. Harga aset digital dapat menjadi volatil. Nilai investasi Anda mungkin turun atau naik. Anda mungkin tidak mendapatkan kembali jumlah yang sudah diinvestasikan. Anda bertanggung jawab sepenuhnya terhadap keputusan investasi Anda. Binance Academy tidak bertanggung jawab terhadap kerugian yang mungkin Anda alami. Materi ini tidak boleh ditafsirkan sebagai nasihat keuangan.