Artikel ini diposting oleh anggota komunitas. Penulisnya adalah David Tarditi, Wakil Presiden Teknik di CertiK, sebuah perusahaan audit kontrak pintar Web3.
Ringkasan
Verifikasi formal atas kontrak pintar melindunginya dari kesalahan, kerentanan, dan kondisi buruk lainnya. Dalam proses ini, pakar manusia mengubah logika kontrak pintar menjadi pernyataan matematika, dan kemudian menggunakan proses otomatis untuk memeriksa logika aktual terhadap model perilaku kontrak yang diharapkan. Dengan menggabungkan verifikasi formal dan audit manual, kami dapat melakukan penilaian komprehensif terhadap keamanan kontrak pintar.
Perkenalan
Kontrak pintar adalah program komputer yang diterapkan pada blockchain yang secara otomatis berjalan ketika kondisi tertentu terpenuhi. Kontrak pintar bisa sangat sederhana atau sangat kompleks dan dapat menampung aset bernilai jutaan atau bahkan miliaran dolar.
Jika ada celah keamanan dalam kode kontrak pintar, hal ini dapat menimbulkan konsekuensi buruk, seperti pencurian semua aset yang dimiliki oleh penjahat. Pada tahun 2021, $50 juta dicuri dari pembuat pasar otomatis (AMM) Uranium Finance karena kesalahan ketik dalam kontrak pintar.
Juga pada tahun 2021, Compound Finance secara keliru memberikan hadiah $80 juta karena satu kesalahan pengkodean. Pada tahun 2022, $320 juta dicuri dari Wormhole Bridge karena kesalahan dalam kontrak pintar.
Oleh karena itu, penting untuk menjalankan program kontrak pintar Anda sejak awal. Kontrak pintar mengadopsi model sumber terbuka, yang berarti bahwa setelah kontrak diterapkan, kodenya akan dipublikasikan. Jika seorang hacker menemukan bug, mereka dapat langsung mengeksploitasinya. Selain itu, praktik normal menambal kerentanan keamanan dari waktu ke waktu tidak efektif karena kode kontrak pintar sering kali tidak dapat dimodifikasi setelah penerapan.
Bagaimana cara kerja verifikasi kontrak pintar?
Verifikasi formal kontrak pintar dicapai dengan menyajikan logika dan perilaku yang diharapkan dari kontrak pintar sebagai pernyataan matematis. Auditor kemudian menggunakan alat otomatis untuk memeriksa apakah pernyataan ini benar.
Prosesnya melibatkan:
Tentukan spesifikasi dan karakteristik yang diharapkan dari kontrak dalam bahasa formal.
Ubah kode kontrak menjadi pernyataan formal, seperti model matematika atau logika.
Verifikasi spesifikasi dan properti kontrak menggunakan pembuktian teorema otomatis atau pemeriksaan model.
Ulangi proses validasi untuk menemukan dan memperbaiki kesalahan atau penyimpangan dari karakteristik yang diharapkan.
Mengapa verifikasi kontrak pintar itu penting
Dengan menerapkan penalaran matematis, hal ini membantu memastikan bahwa kontrak pintar yang diverifikasi secara formal bebas dari kesalahan, kerentanan, dan situasi merugikan lainnya. Verifikasi juga membantu meningkatkan kepercayaan dan keyakinan terhadap kontrak karena propertinya telah diuji secara ketat dan benar serta dapat diandalkan.
Contoh di bawah ini menguraikan bagaimana verifikasi kontrak pintar dapat membantu mencegah kerugian finansial yang signifikan dan konsekuensi bencana lainnya.
Tidak bertukar tempat
Uniswap adalah AMM yang terkenal. Kontrak pintar Uniswap V1 menjalani verifikasi formal selama proses pengembangan. Sebelum dirilis, verifikasi formal ini menemukan dan memperbaiki beberapa kesalahan pembulatan, sehingga mencegah terkurasnya dana Uniswap V1.
Pengimbang
Balancer V2 juga merupakan AMM yang terbukti. Verifikasi formal menemukan dan memperbaiki kesalahan penghitungan biaya pada fitur pinjaman kilat di kontrak pintar yang membuat platform perdagangan rentan terhadap pencurian.
Bulan Aman
Setelah penerapan SafeMoon V1, kesalahan yang sangat kecil ditemukan melalui verifikasi formal. Jika kesalahan tidak ditemukan, jika pemilik kontrak melakukan operasi tertentu sebelum menyerahkan kepemilikan, pemilik kontrak mungkin memperolehnya kembali setelah melepaskan kontrak.
Sebagian besar audit manual pada fork SafeMoon V1 melewatkan bug ini karena kombinasi tertentu dari nilai variabel program perlu dianalisis untuk menemukannya. Manusia dapat dengan mudah melewatkan masalah ini, namun mesin dapat menangkapnya tepat pada waktunya.
Bagaimana verifikasi formal dan audit manual bekerja sama
Verifikasi formal menyediakan cara sistematis dan otomatis untuk memeriksa logika dan perilaku suatu kontrak terhadap karakteristik yang diharapkan. Hal ini mempermudah untuk mengidentifikasi dan memperbaiki potensi bug atau kerentanan. Hal ini sangat berguna untuk masalah yang kompleks dan tidak kentara yang sulit dideteksi melalui pemeriksaan manual.
Audit manual melibatkan para ahli yang meninjau kode, desain, dan penerapan kontrak. Auditor menggunakan pengalaman dan keahlian mereka untuk mengidentifikasi risiko keamanan dan menilai keseluruhan postur keamanan kontrak. Mereka juga dapat mengonfirmasi bahwa proses verifikasi formal telah dilakukan dengan benar dan memeriksa masalah apa pun yang mungkin tidak terdeteksi oleh alat otomatis.
Dengan menggabungkan verifikasi formal dan audit manual, kami dapat melakukan penilaian komprehensif terhadap keamanan kontrak pintar. Hal ini meningkatkan peluang menemukan dan memperbaiki kerentanan apa pun. Dalam melakukan hal ini, kami mengadopsi pendekatan pertahanan keamanan mendalam yang menggabungkan keahlian manusia dan mesin.
Kesimpulan
Untuk memastikan keamanan kontrak pintar, verifikasi formal dan audit manual harus digabungkan untuk memastikan penilaian yang komprehensif dan menyeluruh terhadap postur keamanan kontrak pintar.
Meskipun verifikasi formal membutuhkan lebih banyak sumber daya, ini merupakan investasi yang bermanfaat untuk kontrak dengan nilai tinggi atau faktor risiko tinggi. Bagaimanapun, pada akhirnya, keamanan adalah yang terpenting, jadi pastikan untuk memprioritaskan keamanan dan memastikan bahwa kontrak pintar bebas dari bug, kerentanan, dan perilaku merugikan yang tidak terduga.
Bacaan lebih lanjut
Apa itu kontrak pintar?
Apa itu audit keamanan kontrak pintar?
Penafian dan peringatan risiko: Isi artikel ini adalah fakta dan hanya untuk informasi umum dan tujuan pendidikan dan bukan merupakan representasi atau jaminan apa pun. Artikel ini tidak boleh ditafsirkan sebagai nasihat keuangan dan tidak menyarankan Anda membeli produk atau layanan tertentu. Harga aset digital mungkin berfluktuasi. Nilai investasi Anda mungkin turun atau naik dan Anda mungkin tidak mendapatkan kembali pokok investasi Anda. Anda sepenuhnya bertanggung jawab atas keputusan investasi Anda sendiri dan Binance Academy tidak bertanggung jawab atas kerugian apa pun yang mungkin Anda derita. Materi ini bukan merupakan nasihat keuangan.
