Analisis Keamanan Bahasa Move

Pendahuluan

Move adalah bahasa kontrak pintar yang dapat dijalankan dalam lingkungan blockchain yang mengimplementasikan MoveVM. Sejak awal kelahirannya, bahasa ini telah mempertimbangkan berbagai masalah keamanan yang terkait dengan blockchain dan kontrak pintar, serta mengadopsi beberapa desain keamanan dari bahasa RUST. Sebagai bahasa kontrak pintar generasi baru yang memiliki keamanan sebagai karakteristik utama, bagaimana keamanan Move? Apakah dapat menghindari ancaman keamanan umum yang sering ditemukan pada VM kontrak seperti EVM, WASM, di tingkat bahasa atau mekanisme terkait? Apakah ada risiko keamanan khusus yang melekat padanya?

Artikel ini akan membahas masalah keamanan bahasa Move dari tiga aspek: karakteristik bahasa, mekanisme operasi, dan alat verifikasi.

1. Fitur Keamanan Bahasa Move

Berbeda dengan banyak bahasa pemrograman yang ada, Move dirancang untuk mendukung interaksi yang aman dengan kode yang tidak dipercaya serta mendukung verifikasi statis. Move memiliki fitur keamanan ini karena mengabaikan logika non-linear yang didasarkan pada pertimbangan fleksibilitas, tidak mendukung pengiriman dinamis, dan juga tidak mendukung panggilan eksternal rekursif, tetapi menggunakan konsep generik, penyimpanan global, dan sumber daya untuk mewujudkan pola pemrograman alternatif. Misalnya, Move menghilangkan pengiriman dinamis dan fitur panggilan rekursif yang dapat menyebabkan kerentanan reentrancy.

Fitur keamanan utama dari Move termasuk:

1. Modul (: Setiap modul Move terdiri dari serangkaian tipe struktur dan definisi proses. Modul dapat mengimpor definisi tipe yang dinyatakan oleh modul lain dan memanggil prosesnya.

2. Struktur): dapat didefinisikan sebagai tipe sumber daya, yang menunjukkan dapat disimpan dalam penyimpanan kunci/nilai global yang permanen.

3( proses ) fungsi ): mendefinisikan fungsi spesifik dari modul.

4( Penyimpanan Global: Mengizinkan program Move untuk menyimpan data permanen, data ini hanya dapat dibaca dan ditulis secara terprogram oleh modul yang memilikinya.

5. Pemeriksaan invariant: invariant yang dapat didefinisikan untuk pemeriksaan statis, menjamin integritas sumber daya dalam sistem.

6. Verifier bytecode: memverifikasi tipe keamanan dan linearitas, mencegah nilai sensitif dibuat, dimodifikasi, atau dihancurkan secara ilegal.

![Analisis Keamanan Move: Game Changer Bahasa Kontrak Pintar])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp)

2. Mekanisme Operasi Move

Program Move dijalankan di mesin virtual, tidak dapat mengakses memori sistem secara langsung. Program dieksekusi di tumpukan, penyimpanan global dibagi menjadi memori ( tumpukan ) dan variabel global ( tumpukan ).

Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan, cara ini mudah diimplementasikan dan dikontrol, dengan kebutuhan perangkat keras yang lebih rendah, cocok untuk skenario blockchain. Selain itu, dibandingkan dengan interpreter berbasis register, interpreter berbasis tumpukan lebih mudah untuk mengontrol dan mendeteksi penyalinan dan pemindahan antar variabel.

Selama proses eksekusi, status program Move terdiri dari tumpukan panggilan, memori, variabel global, dan operasi. Tumpukan panggilan berisi semua informasi konteks eksekusi proses. Saat eksekusi instruksi Call, objek tumpukan panggilan baru akan dibuat. Ketika instruksi cabang ditemukan, lompatan statis akan dilakukan di dalam proses.

Berbeda dengan EVM, MoveVM memisahkan penyimpanan data dan tumpukan panggilan, yang lebih cocok untuk kebutuhan manajemen keamanan aset di blockchain. Desain ini memberikan peningkatan besar dalam keamanan dan efisiensi eksekusi.

3. Pindahkan Prover

Move Prover adalah alat verifikasi formal berbasis inferensi, menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma inferensi untuk memverifikasi apakah program sesuai dengan yang diharapkan. Ini dapat membantu pengembang memastikan kebenaran kontrak pintar, mengurangi risiko transaksi.

Move Prover menggunakan algoritma verifikasi deduktif, untuk menyimpulkan perilaku program berdasarkan informasi yang diketahui, memastikan bahwa perilaku tersebut sesuai dengan yang diharapkan. Ini membantu menjamin kebenaran program dan mengurangi beban kerja pengujian manual.

Proses kerja Move Prover adalah sebagai berikut:

1. Menerima file sumber Move sebagai input
2. Ekstrak spesifikasi dan kompilasi menjadi bytecode
3. Mengonversi ke model objek validator
4. Terjemahkan ke dalam bahasa tengah Boogie
5. Menghasilkan kondisi verifikasi
6. Menggunakan pemecah Z3 untuk memverifikasi formula SMT
7. Menghasilkan laporan diagnosis dan mengembalikannya ke kesalahan tingkat sumber kode

Move Specification Language digunakan untuk mendeskripsikan sistem spesifikasi, merupakan subset dari bahasa Move, mendukung deskripsi statis perilaku kebenaran program.

Secara keseluruhan, Move Prover adalah alat yang sangat berguna untuk membantu pengembang memastikan keakuratan kontrak pintar, mengurangi risiko transaksi, dan meningkatkan kepercayaan dalam penerapan kontrak pintar.

4. Ringkasan

Bahasa Move sangat unggul dalam desain keamanan, dengan mempertimbangkan secara menyeluruh pada fitur bahasa, eksekusi mesin virtual, dan lapisan alat keamanan. Ia牺牲了一部分灵活性, pemeriksaan tipe yang ketat, dan logika linier, yang memudahkan pemeriksaan kompilasi dan verifikasi formal. MoveVM memisahkan status dari logika, lebih sesuai dengan kebutuhan manajemen keamanan aset blockchain.

Bahasa Move dapat secara efektif menghindari kerentanan umum dalam EVM seperti reentrancy, overflow, dan injeksi Call/DeleGateCall. Namun, masalah seperti otorisasi, logika kode, dan overflow pada struktur bilangan besar masih memerlukan perhatian ekstra dari pengembang. Meskipun Move Prover menyediakan verifikasi formal, hal itu tidak dapat menutupi kekurangan dalam desain keseluruhan.

Meskipun Move telah mempertimbangkan banyak aspek keamanan, tidak ada bahasa dan program yang sepenuhnya aman. Disarankan agar pengembang kontrak pintar Move tetap menggunakan layanan audit dari perusahaan keamanan pihak ketiga, dan menyerahkan penulisan dan verifikasi bagian spesifikasi kepada tim keamanan profesional.