Analisis Keamanan Bahasa Move: Pengubah Aturan Permainan untuk Bahasa Kontrak Pintar

Bahasa Move adalah bahasa kontrak pintar yang dapat dikompilasi dan dijalankan dalam lingkungan blockchain yang mengimplementasikan MoveVM. Sejak awal kelahirannya, bahasa ini mempertimbangkan berbagai masalah keamanan yang terkait dengan blockchain dan kontrak pintar, serta mengadopsi beberapa desain keamanan dari bahasa RUST. Sebagai generasi baru bahasa kontrak pintar yang memiliki keamanan sebagai karakteristik utama, seberapa aman sebenarnya Move? Dapatkah ia menghindari ancaman keamanan yang umum ditemukan pada mesin virtual kontrak seperti EVM, WASM, dan sebagainya, baik di tingkat bahasa maupun mekanisme terkait? Apakah ada risiko keamanan khusus yang melekat pada bahasa itu sendiri?

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, tujuan desain bahasa Move adalah untuk mendukung penulisan program yang dapat berinteraksi dengan kode yang tidak dipercaya dengan aman, sambil mendukung verifikasi statis. Untuk mencapai tujuan ini, Move mengabaikan logika non-linear yang berbasis pada fleksibilitas, tidak mendukung pengiriman dinamis dan pemanggilan eksternal rekursif, melainkan memperkenalkan konsep generik, penyimpanan global, sumber daya, dan lain-lain untuk mewujudkan pola pemrograman alternatif. Misalnya, Move menghilangkan fitur penjadwalan dinamis dan pemanggilan rekursif, yang dalam bahasa smart contract lain dapat menyebabkan kerentanan reentrancy yang mahal.

Fitur keamanan inti dari Move termasuk:

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

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

3( proses ) Fungsi ): mendefinisikan logika perilaku modul.

4( Penyimpanan Global: Memungkinkan program Move untuk menyimpan data yang persisten, data ini hanya dapat dibaca dan ditulis secara pemrograman oleh modul yang memilikinya.

5. Pemeriksaan invariant: dapat mendefinisikan invariant pemeriksaan statis untuk memastikan konservasi status sistem.

6. Verifier bytecode: menegakkan sistem tipe di tingkat bytecode, mencegah operasi ilegal.

Move menjamin keamanan kode pada saat kompilasi melalui fitur-fitur ini. Selanjutnya, kita akan menganalisis mekanisme kerja Move, dan melihat bagaimana MoveVM menjamin keamanan pada saat runtime.

![Analisis Keamanan Move: Game Changer Bahasa Smart Contract])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp)

2. Mekanisme Operasi Move

Program Move berjalan di mesin virtual, yang tidak dapat mengakses memori sistem selama runtime, sehingga Move dapat berjalan dengan aman di lingkungan yang tidak terpercaya. Program Move dieksekusi di tumpukan, penyimpanan global dibagi menjadi memori ( tumpukan ) dan variabel global ( tumpukan ) dua bagian. Memori adalah penyimpanan tingkat satu, tidak dapat menyimpan pointer yang mengarah ke unit memori. Variabel global digunakan untuk menyimpan pointer yang mengarah ke unit memori, tetapi cara pengindeksan berbeda dengan memori.

Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan. Mesin virtual berbasis tumpukan mudah untuk diimplementasikan dan dikendalikan, serta memiliki persyaratan yang lebih rendah terhadap lingkungan perangkat keras, sehingga cocok untuk skenario blockchain. Dibandingkan dengan interpreter berbasis register, interpreter berbasis tumpukan lebih mudah untuk mengontrol dan mendeteksi salinan dan pemindahan antar variabel.

Status program Move saat berjalan adalah ⟨C, M, G, S⟩ quadruple, yang terdiri dari: stack panggilan (C), memori (M), variabel global (G), dan operand (S). Stack juga memelihara tabel fungsi ( modul itu sendiri ) untuk memecahkan instruksi yang berisi badan fungsi.

MoveVM memisahkan penyimpanan data dan tumpukan pemanggilan ( logika proses ), ini adalah perbedaan terbesar dengan EVM. Dalam MoveVM, sumber daya ( di bawah alamat akun status pengguna ) disimpan secara independen, pemanggilan program harus mematuhi aturan paksa yang terkait dengan izin dan sumber daya. Meskipun ini牺牲了一定灵活性, namun dalam keamanan dan efisiensi eksekusi ( membantu mencapai eksekusi bersamaan ) telah mendapat peningkatan yang signifikan.

3. Pindahkan Prover

Move Prover adalah alat verifikasi formal berbasis penalaran. Ini menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma penalaran untuk memverifikasi apakah program sesuai dengan yang diharapkan, membantu pengembang memastikan kebenaran smart contract, sehingga mengurangi risiko transaksi.

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

Proses kerja Move Prover adalah sebagai berikut:

1. Menerima file sumber Move sebagai input, file ini harus mengatur spesifikasi input program (specification).

2. Move Parser mengekstrak spesifikasi dari kode sumber.

3. Move compiler mengompilasi file sumber menjadi bytecode, bersama dengan sistem spesifikasi mengubahnya menjadi model objek prover (Prover Object Model).

4. Menerjemahkan model ke dalam bahasa perantara Boogie.

5. Sistem verifikasi Boogie melakukan "generasi kondisi verifikasi"(verification condition generation).

6. Mengirimkan kondisi verifikasi ke solver Z3 ( SMT solver yang dikembangkan oleh Microsoft ).

7. Z3 memeriksa apakah kode program SMT formula ( memenuhi spesifikasi ) tidak dapat dipenuhi.

8. Jika tidak dapat dipenuhi, menunjukkan bahwa norma telah terbentuk; jika tidak, buat model yang memenuhi syarat, konversi kembali ke format Boogie untuk menerbitkan laporan diagnosis.

9. Mengembalikan laporan diagnosis menjadi kesalahan tingkat sumber.

Move menggunakan Move Specification Language untuk mendeskripsikan spesifikasi sistem. Bahasa ini adalah subset dari Move, mendukung deskripsi statis perilaku kebenaran program, tanpa mempengaruhi produksi. Dapat menulis dokumen spesifikasi yang khusus secara mandiri, memisahkan kode bisnis dan kode verifikasi formal.

Move Prover adalah alat berguna yang dapat membantu pengembang memastikan keakuratan smart contract. Ini menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma pembuktian untuk memverifikasi apakah program sesuai dengan yang diharapkan. Ini membantu mengurangi risiko transaksi, memungkinkan pengembang untuk lebih percaya diri dalam menerapkan smart contract ke lingkungan produksi.

4. Ringkasan

Bahasa Move sangat unggul dalam desain keamanan, dengan mempertimbangkan secara menyeluruh pada tingkat fitur bahasa, eksekusi mesin virtual, dan alat keamanan. Fitur bahasa牺牲 sebagian fleksibilitas, memaksakan pemeriksaan tipe dan logika linier, yang memudahkan otomatisasi pemeriksaan kompilasi dan verifikasi formal serta keamanan yang dapat diverifikasi. Desain MoveVM memisahkan status dari logika, lebih sesuai dengan kebutuhan manajemen keamanan aset di blockchain.

Di tingkat bahasa, Move dapat secara efektif menghindari kerentanan umum yang ada di EVM seperti reentrancy, overflow, dan injeksi Call/DeleGateCall. Namun, masalah seperti otentikasi, logika kode, dan overflow struktur bilangan bulat besar masih perlu diperhatikan oleh pengembang. Move Prover mungkin tidak dapat berfungsi ketika ada kelalaian dalam pemahaman keseluruhan.

Meskipun bahasa Move telah mempertimbangkan banyak hal untuk keamanan programmer, tidak ada bahasa yang sepenuhnya aman, dan tidak ada program yang sepenuhnya aman. Disarankan agar pengembang smart contract Move menggunakan layanan audit dari perusahaan keamanan pihak ketiga, dan menyerahkan penulisan serta verifikasi bagian kode spesifikasi kepada perusahaan keamanan pihak ketiga.