Analisis Keamanan Bahasa Move

Bahasa Move sebagai bahasa kontrak pintar generasi baru, sejak awal desainnya 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 mengabaikan logika non-linear berbasis fleksibilitas, tidak mendukung pengiriman dinamis dan pemanggilan eksternal rekursif, tetapi menggunakan konsep generik, penyimpanan global, sumber daya, dan lain-lain untuk mencapai pola pemrograman alternatif. Desain ini membantu menghindari kerentanan keamanan seperti reentrancy.

Bagian utama dari bahasa Move mencakup:

• Modul: terdiri dari tipe struktur dan definisi proses, dapat mengimpor definisi tipe dari modul lain dan memanggil proses dari modul lain.

• Struktur: dapat didefinisikan sebagai jenis sumber daya, disimpan dalam penyimpanan kunci-nilai global.

• Proses: mendefinisikan fungsi modul, dapat mencakup proses inisialisasi, aman, dan tidak aman.

Mekanisme penyimpanan global di bahasa Move memungkinkan modul untuk menyimpan data yang persisten dan memiliki akses baca-tulis eksklusif terhadap tipe sumber daya yang dideklarasikannya. Mekanisme ini membantu menegakkan batasan keamanan.

Dua fitur pemeriksaan statis penting dalam bahasa Move:

1. Pemeriksaan invariant: Mendefinisikan konservasi status sistem melalui bahasa spesifikasi.

2. Verifier bytecode: menegakkan tipe keamanan dan linierisasi, mencegah operasi ilegal.

2. Mekanisme Operasi Move

Program Move berjalan di mesin virtual, tidak dapat mengakses memori sistem secara langsung. Eksekusi program didasarkan pada tumpukan, penyimpanan global dibagi menjadi memori ( tumpukan ) dan variabel global ( tumpukan ).

Status eksekusi Move VM terdiri dari tumpukan panggilan, memori, variabel global, dan array operasi. Karakteristiknya meliputi:

• Lompatan statis, menghindari pengiriman dinamis
• Panggilan tumpukan berdekatan, mencegah reentrasi
• Pemisahan penyimpanan data dan tumpukan pemanggilan

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 kerjanya:

1. Menerima file sumber Move dan spesifikasi
2. Mengompilasi menjadi bytecode dan model objek validator
3. Mengonversi ke bahasa perantara Boogie
4. Menghasilkan syarat verifikasi
5. Verifikasi menggunakan solver Z3
6. Menghasilkan Laporan Diagnostik

Move Specification Language digunakan untuk menggambarkan spesifikasi perilaku program, dapat ditulis terpisah dari kode bisnis.

Ringkasan

Bahasa Move telah mempertimbangkan secara menyeluruh fitur bahasa, eksekusi mesin virtual, dan lapisan alat keamanan, sehingga dapat secara efektif menghindari banyak kerentanan umum. Namun, tetap disarankan untuk menggunakan layanan audit keamanan pihak ketiga, dan kode standar harus ditulis dan diverifikasi oleh perusahaan keamanan.