Analisis Keamanan Bahasa Move: Inovator di Bidang Kontrak Pintar

Bahasa Move adalah bahasa kontrak pintar yang dapat dijalankan di lingkungan blockchain yang mendukung MoveVM. Desainnya mempertimbangkan berbagai masalah keamanan yang berkaitan dengan blockchain dan kontrak pintar, serta mengadopsi beberapa konsep desain keamanan dari bahasa Rust. Sebagai generasi baru bahasa kontrak pintar yang berfokus pada keamanan, seberapa aman sebenarnya Move? Apakah itu dapat menghindari ancaman keamanan umum dari mesin virtual kontrak seperti EVM, WASM, dll., baik pada tingkat bahasa maupun mekanisme terkait? Apakah Move sendiri memiliki risiko keamanan unik?

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 tepercaya dengan aman, sambil mendukung validasi statis. Move mengabaikan logika non-linear yang berdasarkan fleksibilitas, tidak mendukung pengiriman dinamis dan pemanggilan eksternal rekursif, tetapi memperkenalkan konsep generik, penyimpanan global, sumber daya, dan lainnya untuk mewujudkan pola pemrograman alternatif. Misalnya, Move menghilangkan fitur pengaturan dinamis dan pemanggilan rekursif, yang dalam bahasa kontrak pintar lainnya dapat menyebabkan kerentanan reentrancy yang mahal.

Fitur keamanan inti dari Move meliputi:

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

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

3. Proses: mendefinisikan fungsi dan logika 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 invariabel: Invariabel yang dapat didefinisikan untuk pemeriksaan statis, memastikan konservasi keadaan sistem.

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

Dengan fitur keamanan ini, Move menyediakan lingkungan pemrograman yang lebih aman dan dapat diandalkan untuk pengembangan smart contract.

2. Mekanisme Operasional Move

Program Move berjalan di dalam mesin virtual, dan tidak dapat mengakses memori sistem saat dijalankan, hal ini memungkinkan Move untuk 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 menunjuk ke unit memori. Variabel global digunakan untuk menyimpan pointer yang menunjuk ke unit memori, tetapi cara indeksnya berbeda dengan memori.

Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan. Dibandingkan dengan interpreter berbasis register, interpreter berbasis tumpukan lebih mudah untuk mengontrol dan mendeteksi operasi penyalinan dan pemindahan antar variabel.

Status runtime dari program Move adalah kuartet ⟨C, M, G, S⟩, yang mencakup stack panggilan (C), memori (M), variabel global (G), dan operand (S). Stack juga memelihara tabel fungsi untuk memecahkan instruksi yang berisi tubuh fungsi.

MoveVM memisahkan penyimpanan data dan logika proses tumpukan pemanggilan (, ini adalah perbedaan utama dengan EVM. Sumber daya ) di bawah alamat akun status pengguna ( disimpan secara independen, pemanggilan program harus mematuhi aturan paksa yang terkait dengan izin dan sumber daya. Desain ini meskipun mengorbankan fleksibilitas tertentu, tetapi mendapatkan peningkatan yang signifikan dalam keamanan dan efisiensi eksekusi.

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

3. Pindahkan Prover

Move Prover adalah alat verifikasi formal berbasis inferensi, yang 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 smart contract, 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 ketepatan program dan mengurangi beban kerja pengujian manual.

Alur kerja Move Prover adalah sebagai berikut:

1. Menerima file sumber Move sebagai input, yang berisi spesifikasi input program.

2. Move Parser mengekstrak spesifikasi dari kode sumber.

3. Kompilator Move mengkompilasi file sumber menjadi bytecode, bersama dengan sistem standar mengubahnya menjadi model objek validator.

4. Model objek diterjemahkan menjadi bahasa menengah Boogie.

5. Sistem verifikasi Boogie melakukan "generasi kondisi verifikasi" untuk input.

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

7. Z3 memeriksa apakah formula SMT tidak dapat dipenuhi. Jika iya, itu menunjukkan bahwa spesifikasi berlaku; jika tidak, menghasilkan model yang memenuhi kondisi.

8. Kembalikan laporan diagnosis ke tingkat kesalahan kode sumber.

Move menggunakan Move Specification Language untuk mendeskripsikan spesifikasi sistem, ini adalah sub-kumpulan dari bahasa Move, yang mendukung deskripsi statis dari perilaku kebenaran program, tanpa mempengaruhi produksi. Spesifikasi dapat ditulis secara independen, memudahkan pemisahan kode bisnis dan kode verifikasi formal.

Move Prover adalah alat yang kuat, dapat membantu pengembang memastikan keakuratan smart contract, mengurangi risiko transaksi, dan meningkatkan kepercayaan dalam menerapkan smart contract ke lingkungan produksi.

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

4. Ringkasan

Bahasa Move sangat unggul dalam desain keamanan, dengan mempertimbangkan secara menyeluruh mulai dari fitur bahasa, eksekusi mesin virtual hingga lapisan alat keamanan. Fitur bahasa牺牲掉 sebagian fleksibilitas, pemeriksaan tipe yang ketat dan logika linier, menguntungkan otomatisasi dan verifikasi yang dapat diverifikasi dari pemeriksaan kompilasi. Desain MoveVM memisahkan status dari logika, lebih sesuai dengan kebutuhan manajemen keamanan aset blockchain.

Pada tingkat bahasa, Move dapat secara efektif menghindari kerentanan umum EVM seperti reentrancy, overflow, dan injeksi Call/DeleGateCall. Namun, masalah seperti otentikasi, logika kode, dan overflow struktur bilangan besar masih memerlukan penanganan hati-hati dari pengembang. Meskipun Move Prover sangat kuat, ia mungkin tidak dapat berfungsi dengan baik jika ada kelalaian dalam desain keseluruhan.

Meskipun bahasa Move memberikan berbagai jaminan keamanan bagi programmer, tidak ada bahasa dan program yang sepenuhnya aman. Disarankan agar pengembang smart contract Move tetap menggunakan layanan audit dari perusahaan keamanan pihak ketiga, dan menyerahkan penulisan serta verifikasi bagian kode spesifikasi kepada tim keamanan profesional, untuk lebih meningkatkan keamanan kontrak.

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