Pengenalan

Saat nilai aset di blockchain tumbuh dengan cepat dengan beberapa proyek bergantian meluncurkan berbagai kasus penggunaan dalam ekonomi kripto, menjaga keunggulan dari celah dan ancaman yang mungkin lebih penting dari sebelumnya.

Bitcoin diciptakan untuk menggantikan bank, tetapi teknologi yang mendasarinya, blockchain membuktikan bahwa itu bisa menggantikan hampir semua perantara. Melangkah lebih jauh, itu tidak berhenti di situ melihat potensi besar yang dimiliki uang digital yang tidak pernah dimiliki uang kertas dan itu melibatkan kemampuan untuk memprogram uang. Tiba-tiba, pengacara dan kontrak bisa digantikan dalam transaksi keuangan. Bentuk mata uang digital ini memajukan desentralisasi dengan memungkinkan eksekusi otomatis kontrak dengan transparansi penuh dan tanpa intervensi manusia. Namun, bagaimana tepatnya kontrak pintar beroperasi? Apakah benar-benar dapat diandalkan untuk mempercayai sistem ini yang tidak memiliki kepercayaan?

Dalam artikel ini, kami akan menjelajahi pertanyaan-pertanyaan yang luas tentang verifikasi formal dari kontrak cerdas, membahas kelebihan, kekurangan, dampaknya pada ekosistem kripto, dan banyak lagi dengan penekanan pada Ethereum.

Sejarah Singkat Kontrak Pintar

Sumber: CryptoSlate

Nick Szabo, seorang ilmuwan komputer dan kriptografer Amerika yang sering dispekulasikan sebagai Satoshi Nakamoto, adalah pelopor smart contract, pertama kali memperkenalkan konsep tersebut pada tahun 1994. Szabo menggambarkan smart contract sebagai protokol transaksi digital yang dirancang untuk secara otomatis menegakkan persyaratan suatu kesepakatan. Tujuannya adalah untuk meningkatkan metode transaksi elektronik, seperti sistem penjualan, dan memperluas kemampuan mereka ke dunia digital.

Szabo membayangkan masa depan di mana perjanjian dapat berfungsi seperti mesin penjual otomatis — otomatis, andal, dan anti-rusak. Meskipun teknologi pada masanya tidak cukup maju untuk sepenuhnya mewujudkan visinya, ide-ide Szabo meletakkan dasar untuk apa yang nantinya akan merevolusi industri blockchain. Kapan Ethereum diluncurkanpada tahun 2015, itu menghadirkan kontrak pintar ke dalam penggunaan praktis, mengubah konsep teoritis Szabo menjadi komponen penting dari aplikasi terdesentralisasi.

Visinya adalah kontrak yang dapat mengelola hubungan dengan persyaratan otomatis yang tepat, mengurangi kebutuhan untuk campur tangan dan pengawasan manusia. Pendekatan ini bertujuan untuk menciptakan cara yang lebih aman dan efisien dalam menangani perjanjian, membuka jalan bagi perkembangan smart contract menjadi alat yang kuat dalam ekosistem blockchain. Wawasan awal Szabo terus membentuk lanskap transaksi digital dan pengembangan smart contract saat ini.

Apa itu Verifikasi Formal?

Sumber: Medium

Verifikasi Formal adalah proses menilai dengan ketat apakah sebuah sistem, seperti smart contract, beroperasi sesuai dengan seperangkat aturan atau spesifikasi yang ditentukan. Pada dasarnya, hal ini memeriksa apakah sistem tersebut berperilaku sesuai yang diharapkan, memastikan bahwa sistem memenuhi kondisi yang diperlukan dan melakukan fungsi yang dimaksud tanpa kesalahan.

Untuk mencapai hal ini, perilaku yang diharapkan dari sistem diuraikan menggunakan model formal, sementara bahasa spesifikasi digunakan untuk menentukan properti yang tepat yang harus dipenuhi kontrak dan kita akan melihat skenario yang lebih praktis seiring berjalannya artikel. Teknik verifikasi formal kemudian mencocokkan implementasi kontrak dengan spesifikasinya, memberikan bukti matematis tentang kebenarannya. Ketika kontrak memenuhi spesifikasi ini, itu dianggap "benar secara fungsional" atau "benar dengan desain," menegaskan keandalan dan keamanannya di lingkungan blockchain.

Jenis Spesifikasi Formal untuk Kontrak Pintar

Sumber: Ever Scale

Spesifikasi formal menyediakan cara terstruktur untuk menggunakan pemikiran matematis untuk memverifikasi akurasi eksekusi program. Spesifikasi ini dapat menggambarkan properti tingkat tinggi, yang berfokus pada perilaku keseluruhan, atau detail tingkat rendah tentang bagaimana kontrak beroperasi secara internal. Dengan mendefinisikan perilaku ini secara matematis, spesifikasi formal memastikan bahwa kontrak berfungsi seperti yang dimaksudkan.

Spesifikasi tingkat tinggi

Spesifikasi tingkat tinggi, juga dikenal sebagai spesifikasi berorientasi model, menggambarkan perilaku keseluruhan dari smart contract, memperlakukannya sebagai mesin keadaan terbatas (FSM) yang bertransisi antara berbagai keadaan melalui operasi tertentu. Logika temporal sering digunakan untuk mendefinisikan aturan formal yang mengatur transisi ini, menjelaskan bagaimana kontrak bergerak antara keadaan dari waktu ke waktu dan kondisi yang harus dipenuhi untuk melakukannya dengan benar.

Spesifikasi ini menangkap dua properti penting: keamanan dan keberlangsungan. Keamanan memastikan bahwa peristiwa yang tidak diinginkan tidak terjadi, seperti mencegah saldo pengirim turun di bawah jumlah yang dibutuhkan untuk transaksi. Sebaliknya, keberlangsungan memastikan bahwa kontrak terus berfungsi dan berkembang, seperti menjaga likuiditas agar pengguna dapat menarik dana jika diminta. Kedua properti ini memastikan smart contract beroperasi dengan aman dan dapat diandalkan, menjaga interaksi dan aset pengguna.

Spesifikasi tingkat rendah

Spesifikasi tingkat rendah, juga dikenal sebagai spesifikasi berorientasi pada properti, berfokus pada mendefinisikan perilaku yang benar dari kontrak pintar dengan menganalisis proses eksekusi internalnya. Berbeda dengan spesifikasi tingkat tinggi yang memodelkan kontrak sebagai mesin keadaan terbatas, spesifikasi tingkat rendah memandang kontrak pintar sebagai sistem fungsi matematika dan memeriksa urutan eksekusi fungsi, yang dikenal sebagai jejak, yang mengubah keadaan kontrak.

Teknik Verifikasi Formal Kontrak Pintar

Sumber: Ever Scale

Pemeriksaan Model

Model checking adalah metode verifikasi formal yang menggunakan algoritma untuk mengevaluasi apakah model kontrak pintar sesuai dengan spesifikasinya. Kontrak pintar biasanya direpresentasikan sebagai sistem transisi keadaan, dan properti-properti mereka didefinisikan menggunakan temporallogika. Proses ini melibatkan pembuatan model matematika dari kontrak dan mengungkapkan propertinya melalui rumus logika, memungkinkan algoritma untuk memverifikasi apakah model tersebut memenuhi spesifikasi ini.

Pembuktian Teorema

Berbeda dengan model checking, pembuktian teorema adalah pendekatan matematis yang digunakan untuk menetapkan kebenaran program, termasuk kontrak pintar. Metode ini melibatkan mengonversi model dan spesifikasi kontrak menjadi rumus logika untuk memverifikasi kesetaraan logika mereka, artinya suatu pernyataan benar jika yang lain benar. Dengan merumuskan hubungan ini sebagai teorema, pembuktian otomatis teorema dapat memvalidasi kebenaran model kontrak terhadap spesifikasinya.

Dalam kontras tajam dengan pemeriksaan model, yang terbatas pada sistem berkeadaan terbatas, pembuktian teorema dapat menganalisis sistem berkeadaan tak terbatas tetapi sering memerlukan bimbingan manusia untuk menavigasi masalah logika yang kompleks. Akibatnya, pembuktian teorema cenderung lebih membutuhkan sumber daya daripada proses pemeriksaan model yang sepenuhnya otomatis.

Simulasi Simbolik

Eksekusi simbolik adalah metode analisis yang kuat untuk smart contract yang melibatkan eksekusi fungsi dengan nilai simbolik daripada input spesifik. Teknik verifikasi formal ini memungkinkan penalaran tentang properti tingkat jejak dalam kode kontrak dengan mewakili jalur eksekusi sebagai rumus matematika, yang dikenal sebagai predikat jalur. Solver SMT kemudian digunakan untuk menentukan apakah predikat-predikat ini memuaskan, yang berarti input yang memenuhi kondisi ada.

Misalnya, jika fungsi kontrak melempar kembali saat nilai berada antara 5 dan 10, eksekusi simbolik dapat secara efisien mengidentifikasi nilai-nilai yang memicu seperti itu dengan mengevaluasi kondisi sebagai X > 5 ∧ X < 10. Metode ini seringkali lebih efektif daripada pengujian tradisional, menghasilkan lebih sedikit positif palsu dan langsung menghasilkan nilai-nilai konkret yang mereplikasi solusi SMT apa pun kemudian digunakan untuk menentukan kesalahan yang ditemukan, sehingga menjadikannya alat berharga untuk memastikan keandalan kontrak pintar.

Apa itu smart contract?

Sumber: Tenderly

Smart contract adalah program komputer otomatis yang beroperasi pada blockchain, mengeksekusi tindakan ketika kondisi tertentu terpenuhi. Mereka dapat bervariasi dari perjanjian sederhana hingga proses yang sangat kompleks dan dapat mengelola aset senilai jutaan atau bahkan miliaran dolar.

Sementara smart contract memiliki potensi untuk merevolusi berbagai sektor seperti pemungutan suara politik, manajemen rantai pasokan, perawatan kesehatan, dan real estat, artikel ini masih mempertahankan fokusnya pada dampaknya di ranah cryptocurrency. Desain mereka memungkinkan beberapa pihak untuk bekerja sama tanpa risiko manipulasi, menawarkan kerangka kerja transparan dan aman yang meningkatkan efisiensi dan inovasi. Namun, penting untuk diakui bahwa smart contract juga datang dengan kerentanan dan tantangan.

Kerentanan dengan Smart Contact

kerentanan keamanandalam kode kontrak pintar dapat menyebabkan hasil yang sangat buruk, seperti total kehilangan aset yang disimpan dalam kontrak, seperti yang ditunjukkan oleh insiden-insiden terbaru.

• Pada tahun 2021, pasar pembuat otomatis Uranium Finance mengalami pencurian $50 jutakarena kesalahan ketik sederhana dalam kontrak pintar.
• Juga pada tahun 2021, Compound Finance secara tidak sengaja mendistribusikan $80 jutadi hadiah yang tidak pantas, lagi-lagi karena kesalahan satu karakter.
• Pelanggaran yang lebih signifikan terjadi pada tahun 2022ketika $320 juta dicuri dari Wormhole Bridge karena bug di salah satu kontrak pintarnya.

Dengan contoh-contoh ini, sangat penting untuk memastikan bahwa kontrak pintar dikode dengan akurat dari awal. Setelah diterapkan, kontrak pintar bersifat open-source, artinya kode mereka dapat diakses secara publik, memudahkan para hacker untuk mengeksploitasi kerentanan yang ditemukan. Selain itu, sifat yang tidak dapat diubah dari kontrak pintar berarti bahwa setelah mereka diluncurkan, kode mereka biasanya tidak dapat diubah untuk memperbaiki kelemahan keamanan, membuat mereka selalu berisiko jika tidak dikembangkan dengan presisi yang paling tinggi.

Bagaimana Verifikasi Kontrak Pintar Bekerja?

Sumber: Certik

Proses ini meliputi:

• Menentukan spesifikasi dan properti yang diinginkan dari kontrak menggunakan bahasa formal.
• Menerjemahkan kode kontrak ke representasi formal, seperti model matematika atau ekspresi logis.
• Pemecah teorema otomatis atau pemeriksa model digunakan untuk mengonfirmasi validitas spesifikasi dan properti kontrak.
• Berulang kali ulangi proses verifikasi untuk mengidentifikasi dan memperbaiki kesalahan atau penyimpangan dari properti yang dimaksud.

Fitur Utama dari Kontrak Pintar

Sumber: Certik

Pikirkan smart contract sebagai perjanjian yang terukir dalam batu setelah dibuat, mereka tidak dapat diubah. Beroperasi pada buku besar blockchain yang tidak dapat diubah, kontrak ini secara otomatis menegakkan ketentuan tanpa perlu perantara, yang mempercepat transaksi dan mengurangi biaya. Sifat yang tetap ini meningkatkan keamanan dan mendekentralisasi kontrol, secara signifikan mengurangi kemungkinan penipuan dan korupsi.

Mengapa Verifikasi Smart Contract Penting

Pemikiran matematis memainkan peran penting dalam memastikan bahwa kontrak pintar yang diverifikasi secara formal bebas dari bug, kerentanan, dan perilaku yang tak terduga. Proses yang ketat ini meningkatkan kepercayaan dan keyakinan pada kontrak karena propertinya telah divalidasi secara menyeluruh.

Contoh verifikasi smart contract yang berhasil menyoroti pentingnya dalam mencegah kerugian keuangan yang signifikan.

Uniswap

Sebagai contoh, Uniswap, seorang pembuat pasar otomatis (AMM) yang terkenal, menjalani verifikasi formal selama pengembangan kontrak cerdas V1-nya, yang mengidentifikasi dan memperbaiki kesalahan pembulatanyang dapat menguras dana.

Balancer

Demikian pula, Balancer V2, AMM lain, mendapat manfaat dari verifikasi formal yang menemukan perhitungan biaya yang tidak benarterkait dengan pinjaman kilat, mencegah pencurian potensial.

SafeMoon

SafeMoon V1 memiliki bug yang halusdiidentifikasi melalui verifikasi formal setelah implementasi. Bug ini memungkinkan pemilik untuk menolak kepemilikan dan mendapatkannya kembali dalam kondisi tertentu, detail ini yang kebanyakan audit manual lewat karena kompleksitasnya. Kemampuan verifikasi formal dalam menganalisis kombinasi nilai variabel tertentu membuatnya menjadi alat yang efektif untuk menangkap masalah yang mungkin terlewatkan oleh auditor manusia.

Bagaimana Verifikasi Formal dan Audit Manual Bekerja Sama

Verifikasi Formal menawarkan metode sistematis dan otomatis untuk memeriksa logika dan perilaku kontrak pintar terhadap propertinya yang dimaksudkan. Pendekatan ini menyederhanakan identifikasi dan perbaikan kesalahan atau bug potensial, terutama masalah kompleks yang mungkin terlewatkan oleh pemeriksaan manual.

Di sisi lain, audit manual melibatkan tinjauan menyeluruh dari kode, desain, dan implementasi kontrak oleh ahli. Auditor memanfaatkan pengalamannya untuk menemukan risiko keamanan dan menilai postur keamanan keseluruhan dari kontrak. Mereka juga dapat memvalidasi kebenaran proses verifikasi formal dan mengidentifikasi masalah yang mungkin terlewat oleh alat otomatis. Menggabungkan verifikasi formal dengan audit manual menciptakan evaluasi keamanan yang komprehensif, meningkatkan kemungkinan untuk menemukan dan menyelesaikan kerentanan, serta membentuk strategi pertahanan yang tangguh dengan memanfaatkan keunggulan keahlian manusia dan analisis otomatis.

Pro dan Kontra dari Kontrak Pintar

Sumber: Blockonomi

Smart contract bukanlah sempurna, namun keuntungan mereka jauh lebih besar daripada kerugiannya. Mereka menyederhanakan transaksi kompleks, menghemat waktu dan uang sambil mempromosikan transparansi dan mengurangi perselisihan. Karena mereka beroperasi berdasarkan kode, mereka meminimalkan kesalahan manusia. Keamanan mereka kuat, berkat perlindungan kriptografis. Namun, smart contract dapat kaku dan kesulitan beradaptasi dengan situasi yang tidak terduga. Selain itu, menyiapkan mereka memerlukan keterampilan pemrograman khusus, yang dapat menjadi hambatan bagi sebagian orang. Meskipun tantangan ini, smart contract sedang mengubah industri.

Kelebihan dari Kontrak Pintar

• Meningkatkan efisiensi dengan mengotomatisasi tugas, menghemat waktu dan uang.
• Meningkatkan transparansi dengan memberikan akses kepada semua pihak untuk mendapatkan informasi yang sama, mengurangi perselisihan.
• Mengurangi kesalahan dengan mengandalkan kode, yang menghilangkan kesalahan manusia.
• Perkuat keamanan dengan perlindungan kriptografi, membuat pengubahan sulit.

Kerugian dari Smart Contract

• Ketidakfleksibelan untuk menyesuaikan diri dengan situasi yang tidak terduga karena sifat yang kaku.
• Membutuhkan pengetahuan pemrograman khusus, yang membatasi adopsi yang luas.

Alat Verifikasi Formal untuk Kontrak Pintar Ethereum

Sumber: Calibraint

Bahasa spesifikasi untuk membuat spesifikasi formal

• Act: Act memungkinkan pengguna untuk mendefinisikan pembaruan penyimpanan, pra dan pasca-kondisi, dan invarian kontrak. Suite alatnya mencakup backend bukti yang dapat memvalidasi berbagai properti menggunakan Coq, solver SMT, atau hevm.

GitHub

Dokumentasi

• Scribble: Scribble mengubah anotasi kode yang ditulis dalam bahasa spesifikasi menjadi asersi khusus yang memverifikasi spesifikasinya.

Dokumentasi

• Dafny: Dafny adalah bahasa pemrograman yang dirancang untuk verifikasi, menggunakan annotasi tingkat tinggi untuk membantu merasionalkan dan mengonfirmasi kebenaran kode.

GitHub

Program verifiers untuk memeriksa kebenaran

• Certora Prover: Certora Prover adalah alat verifikasi formal otomatis yang memeriksa kebenaran kode kontrak pintar. Spesifikasi dibuat menggunakan Bahasa Verifikasi Certora (CVL), dan itu mendeteksi pelanggaran properti melalui kombinasi analisis statis dan teknik pemecahan kendala.

Situs web

Dokumentasi

• Solidity SMTChecker: SMTChecker Solidity adalah pemeriksa model terintegrasi yang menggunakan Satisfiability Modulo Theories (SMT) dan pemecahan Tanduk. Ini memverifikasi apakah kode sumber kontrak selaras dengan spesifikasi selama kompilasi dan memeriksa pelanggaran properti keselamatan.

GitHub

• Solc-verify: Solc-verify adalah versi yang ditingkatkan dari kompilator Solidity yang memungkinkan verifikasi formal otomatis dari kode Solidity melalui anotasi dan verifikasi program modular.

GitHub

• KEVM: KEVM secara formal mewakili Mesin Virtual Ethereum(EVM)dibuat menggunakan kerangka K. Ini dapat dieksekusi dan dapat memverifikasi klaim terkait properti tertentu melalui logika jangkauan.

GitHub

Dokumentasi

Kerangka kerja logis untuk pembuktian teorema

• Isabelle: Isabelle/HOL adalah asisten bukti yang membantu pengguna mengungkapkan rumus matematika dalam bahasa formal dan menyediakan alat untuk membuktikannya. Penggunaan utamanya adalah memformalkan bukti matematika, terutama untuk memverifikasi kebenaran perangkat keras dan perangkat lunak komputer serta properti bahasa pemrograman dan protokol.

GitHub

Dokumentasi

• Coq - Coq adalah pembuktian teorema interaktif yang memungkinkan Anda untuk mendefinisikan program dengan teorema dan membuat bukti yang diperiksa mesin atas kebenaran mereka melalui proses interaktif.

GitHub

Dokumentasi

Alat berbasis eksekusi simbolik untuk mendeteksi pola rentan pada kontrak pintar

• Manticore - Sebuah alat yang menganalisis bytecode EVM menggunakan eksekusi simbolik.

GitHub

Dokumentasi

• Hevm - hevm adalah mesin eksekusi simbolik yang memeriksa kesamaan bytecode EVM.

GitHub

• Mythril - Sebuah alat eksekusi simbolis yang digunakan untuk menemukan kerentanan dalam smart contract Ethereum.

GitHub

Dokumentasi

Kesimpulan

Untuk melindungi smart contract, menggabungkan verifikasi formal dengan pemeriksaan manual sangat penting untuk penilaian komprehensif terhadap keamanannya. Meskipun verifikasi formal dapat membutuhkan sumber daya yang besar, ini adalah investasi berharga untuk kontrak yang melibatkan risiko tinggi atau risiko signifikan. Smart contract lebih dari sekadar konsep yang trendi; mereka sedang mengubah operasi bisnis global, dan meskipun mereka datang dengan tantangan, kemampuan mereka yang tak tertandingi untuk meningkatkan efisiensi, meminimalkan kesalahan, dan memperkuat keamanan tidak dapat diabaikan. Smart contract memiliki potensi besar untuk menyederhanakan proses dan membangun kepercayaan dalam transaksi digital. Untuk tujuan ini, organisasi yang mengadopsi teknologi ini hari ini akan siap untuk berkembang di masa depan yang memprioritaskan transparansi dan keandalan.