Analisis Keamanan Bahasa Move

Bahasa Move sebagai bahasa kontrak pintar generasi baru, sejak awal perancangannya telah mempertimbangkan masalah keamanan blockchain dan kontrak pintar. Artikel ini akan membahas keamanan bahasa Move dari tiga aspek: karakteristik bahasa, mekanisme operasi, dan alat verifikasi.

1. Fitur Keamanan Bahasa Move

Bahasa Move memiliki beberapa fitur keamanan utama sebagai berikut:

• Meninggalkan logika non-linier, tidak mendukung pengiriman dinamis dan pemanggilan eksternal secara rekursif
• Menggunakan konsep generik, penyimpanan global, sumber daya, dan lain-lain untuk mewujudkan pola pemrograman alternatif
• Desain modular, setiap modul terdiri dari jenis struktur dan definisi proses
• Tipe sumber daya dan mekanisme penyimpanan global menjamin keamanan penyimpanan dan sumber daya
• Implementasi pengurangan invarian dan validator bytecode untuk pemeriksaan keamanan saat kompilasi

Verifikator bytecode melakukan tiga jenis pemeriksaan:

1. Pemeriksaan validitas struktur
2. Deteksi semantik logika proses
3. Deteksi kesalahan saat menghubungkan

Melalui mekanisme ini, Move dapat menjamin tingkat keamanan yang tinggi pada saat kompilasi.

2. Mekanisme Operasi Move

Program Move dijalankan di dalam mesin virtual, tidak dapat mengakses memori sistem secara langsung. Statusnya terdiri dari tumpukan panggilan, memori, variabel global, dan array operasi.

Berbeda dengan EVM, MoveVM memisahkan penyimpanan data dan tumpukan pemanggilan. Status pengguna disimpan secara independen, dan pemanggilan program harus mematuhi aturan izin dan sumber daya. Desain ini meningkatkan keamanan dan efisiensi eksekusi.

3. Pindahkan Prover

Move Prover adalah alat verifikasi formal yang menggunakan algoritma verifikasi deduktif untuk memverifikasi apakah program memenuhi harapan. Proses verifikasinya adalah sebagai berikut:

1. Menerima file sumber Move dan spesifikasi
2. Mengompilasi menjadi bytecode dan model objek validasi
3. Terjemahkan ke dalam bahasa tengah Boogie
4. Menghasilkan syarat verifikasi
5. Verifikasi menggunakan pemecah Z3
6. Menghasilkan laporan diagnosis

Move Specification Language digunakan untuk mendeskripsikan sistem spesifikasi, merupakan subkumpulan dari bahasa Move.

Secara keseluruhan, Move Prover adalah alat keamanan yang kuat, tetapi tidak dapat sepenuhnya menggantikan audit manual. Disarankan agar pengembang tetap menggunakan layanan audit keamanan pihak ketiga dan menyerahkan bagian spesifikasi kepada perusahaan keamanan.