Apa itu verifikasi formal kontrak pintar?

Menguji formal dari kontrak pintar dapat menghindari kesalahan, celah keamanan, dan situasi merugikan lainnya. Dalam proses ini, para ahli manusia akan mengubah logika kontrak pintar menjadi pernyataan matematis, kemudian menggunakan proses otomatis untuk memeriksa logika aktual terhadap model yang sesuai dengan perilaku yang diharapkan dari kontrak tersebut. Dengan menggabungkan verifikasi formal dan audit manusia, kita dapat melakukan penilaian menyeluruh terhadap keamanan kontrak pintar.

Pendahuluan

Kontrak pintar adalah program komputer yang ditempatkan di blockchain dan akan berjalan secara otomatis saat memenuhi kondisi tertentu. Kontrak pintar bisa sangat sederhana atau sangat kompleks, dan dapat memegang aset bernilai jutaan bahkan miliaran dolar.

Jika kode kontrak pintar memiliki celah keamanan, hal ini dapat menyebabkan konsekuensi yang menghancurkan, seperti pencurian seluruh aset yang dimiliki oleh kontrak tersebut oleh pihak yang tidak bertanggung jawab. Pada tahun 2021, karena kesalahan penulisan dalam kontrak pintar, Automated Market Maker (AMM) Uranium Finance dicuri sebesar 50 juta dolar.

Begitu juga pada tahun 2021, karena satu kesalahan kode, Compound Finance secara keliru memberikan hadiah sebesar 80 juta dolar. Pada tahun 2022, karena adanya satu kesalahan dalam kontrak pintar, Wormhole Bridge dicuri sebesar 320 juta dolar.

Oleh karena itu, sangat penting untuk memastikan kontrak pintar benar sejak awal. Kontrak pintar menggunakan model sumber terbuka, yang berarti setelah kontrak ditempatkan, kode akan dipublikasikan. Jika peretas menemukan kesalahan di dalamnya, mereka dapat segera memanfaatkannya. Selain itu, seiring waktu, operasi rutin untuk memperbaiki celah keamanan tidak akan efektif, karena kode kontrak pintar biasanya tidak dapat diubah setelah ditempatkan.

Bagaimana cara kerja verifikasi kontrak pintar?

Verifikasi formal kontrak pintar dilakukan dengan mengubah logika dan perilaku yang diharapkan dari kontrak menjadi pernyataan matematis. Kemudian, auditor menggunakan alat otomatis untuk memeriksa apakah pernyataan tersebut benar.

Proses ini melibatkan:

• Mendefinisikan spesifikasi dan fitur yang diharapkan dari kontrak menggunakan bahasa formal.
• Mengubah kode kontrak menjadi pernyataan formal, seperti model matematis atau logika.
• Menggunakan pembuktian teorema otomatis atau pemeriksaan model untuk memverifikasi spesifikasi dan fitur kontrak.
• Mengulangi proses verifikasi untuk menemukan dan memperbaiki kesalahan atau penyimpangan dari fitur yang diharapkan.

Mengapa verifikasi kontrak pintar penting

Dengan menggunakan penalaran matematis, verifikasi formal membantu memastikan bahwa kontrak pintar yang telah diverifikasi secara formal tidak mengandung kesalahan, celah keamanan, atau situasi merugikan lainnya. Verifikasi ini juga meningkatkan kepercayaan dan keyakinan terhadap kontrak, karena fitur-fiturnya telah melalui pengujian yang ketat dan terbukti benar serta dapat diandalkan.

Berikut ini beberapa contoh yang secara umum menunjukkan bagaimana verifikasi kontrak pintar dapat membantu mencegah kerugian finansial besar dan konsekuensi bencana lainnya.

Uniswap

Uniswap adalah salah satu AMM terkenal. Kontrak pintar Uniswap V1 telah menjalani verifikasi formal selama pengembangannya. Sebelum dirilis, verifikasi formal ini menemukan dan memperbaiki beberapa kesalahan pembulatan, sehingga mencegah dana Uniswap V1 terkuras habis.

Balancer

Balancer V2 juga merupakan AMM yang telah diverifikasi. Verifikasi formal menemukan dan memperbaiki kesalahan perhitungan biaya pada fitur pinjaman kilat dalam kontrak pintar, yang dapat menyebabkan platform rentan terhadap pencurian.

SafeMoon

SafeMoon V1 setelah ditempatkan, melalui verifikasi formal ditemukan sebuah kesalahan yang sangat kecil. Jika kesalahan ini tidak ditemukan, pemilik kontrak bisa saja mendapatkan kembali kontrak tersebut setelah melepaskan kepemilikan, jika mereka melakukan beberapa tindakan tertentu sebelum melepaskan hak kepemilikan.

Sebagian besar audit manual terhadap cabang SafeMoon V1 melewatkan kesalahan ini, karena diperlukan analisis kombinasi variabel program tertentu untuk menemukannya. Manusia sangat mudah melewatkan masalah ini, tetapi mesin dapat mendeteksinya secara tepat waktu.

Bagaimana verifikasi formal dan audit manusia bekerja sama

Verifikasi formal menyediakan metode yang sistematis dan otomatis untuk memeriksa logika dan perilaku kontrak berdasarkan fitur yang diharapkan. Ini memudahkan identifikasi dan perbaikan kesalahan atau celah keamanan yang potensial. Sangat berguna untuk masalah yang kompleks dan halus yang sulit dideteksi melalui pemeriksaan manual.

Audit manusia melibatkan para ahli yang meninjau kode, desain, dan proses deployment kontrak. Auditor menggunakan pengalaman dan keahlian mereka untuk mengidentifikasi risiko keamanan dan menilai keseluruhan keamanan kontrak. Mereka juga dapat memastikan bahwa proses verifikasi formal dilakukan dengan benar dan memeriksa adanya masalah yang mungkin tidak terdeteksi oleh alat otomatis.

Dengan menggabungkan verifikasi formal dan audit manusia, kita dapat melakukan penilaian keamanan kontrak pintar secara menyeluruh. Ini meningkatkan peluang dalam menemukan dan memperbaiki celah keamanan apa pun. Dengan demikian, kita menerapkan bentuk pertahanan mendalam yang menggabungkan keahlian manusia dan mesin.

Penutup

Untuk memastikan keamanan kontrak pintar, harus menggabungkan verifikasi formal dan audit manusia, sehingga penilaian terhadap situasi keamanan kontrak menjadi lengkap dan menyeluruh.

Meskipun verifikasi formal memerlukan sumber daya yang cukup besar, ini adalah investasi yang berharga untuk kontrak yang bernilai tinggi atau berisiko tinggi. Pada akhirnya, keamanan adalah prioritas utama, dan harus diutamakan untuk memastikan kontrak pintar bebas dari kesalahan, celah keamanan, dan perilaku tidak diinginkan yang merugikan. **$BNT **$BROCCOLI