Analisis Keamanan Bahasa Move: Pengubah Kontrak Cerdas

Bahasa Move adalah bahasa kontrak pintar yang dapat dikompilasi dan dijalankan dalam lingkungan blockchain yang mengimplementasikan MoveVM. Sebagai bahasa kontrak pintar generasi baru yang memiliki keamanan sebagai fitur utama, seberapa aman kah? Apakah dapat menghindari ancaman keamanan yang umum terjadi pada mesin virtual kontrak seperti EVM, WASM, dll? Artikel ini akan membahas masalah keamanan bahasa Move dari tiga aspek: fitur bahasa, mekanisme operasi, dan alat verifikasi.

1. Fitur Keamanan Bahasa Move

Berbeda dengan banyak bahasa pemrograman yang ada, bahasa Move dirancang untuk mendukung interaksi aman dengan kode yang tidak tepercaya dan juga mendukung verifikasi statis. Move mengabaikan logika non-linear yang didasarkan pada pertimbangan fleksibilitas, tidak mendukung pemanggilan dinamis dan pemanggilan eksternal rekursif, melainkan menggunakan konsep generik, penyimpanan global, sumber daya, dan lainnya untuk mewujudkan pola pemrograman alternatif.

Berikut adalah contoh implementasi aset token dalam bahasa Move:

pindah modul 0x1::TestCoin { gunakan 0x1::signer;

const ADMIN: address = @0x1;

struct Coin memiliki kunci, simpan { 
    value: u64
}

struct Info memiliki kunci {
    total_supply: u64  
}

modul spesifikasi {
    invariant forall addr: address where exists<coin>(addr):
        global\u003cinfo\u003e(ADMIN).total_supply \u003e= global\u003ccoin\u003e(addr).value;
}

publik menyenangkan initialize(akun: &penandatangan) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(akun, Info { total_supply: 0 })
}

public fun mint(account: &signer, amount: u64): Coin {
    assert!(signer::address_of(account) == ADMIN, 1);
    let coin = Coin { value: amount };
    let info = borrow_global_mut\u003cinfo\u003e(ADMIN);
    info.total_supply = info.total_supply + amount;
    koin
}

public fun value(coin: &Coin): u64 { 
    coin.value  
}

}

Contoh ini menunjukkan beberapa fitur keamanan kunci dari bahasa Move:

1. Modular: Setiap modul Move terdiri dari tipe struktur dan definisi proses, dapat mengimpor definisi tipe dari modul lain dan memanggil proses dari modul lain.

2. Jenis sumber daya: Struktur yang ditandai dengan kunci has atau store didefinisikan sebagai jenis sumber daya, dapat disimpan dalam penyimpanan nilai kunci global yang persisten.

3. Penyimpanan Global: Memungkinkan program Move untuk menyimpan data yang persisten, hanya dapat dibaca dan ditulis secara terprogram oleh pemilik modul, tetapi disimpan di buku besar publik yang dapat dilihat oleh modul lain.

4. Kontrol akses: Kontrol akses terhadap operasi penting dapat diimplementasikan melalui pernyataan dan cara lainnya.

5. Reduksi Invarian: dapat mendefinisikan invarian pemeriksaan statis yang digunakan untuk verifikasi formal.

6. Verifikasi bytecode: mencakup verifikasi jenis keamanan dan linearitas, mencegah operasi ilegal pada jenis sumber daya.

Fitur-fitur ini bersama-sama menjamin keamanan bahasa Move saat kompilasi.

2. Mekanisme Operasional Move

Program Move berjalan di dalam mesin virtual, tidak dapat mengakses memori sistem, dapat berjalan dengan aman di lingkungan yang tidak terpercaya.

Program Move dieksekusi di tumpukan, penyimpanan global dibagi menjadi memori ( tumpukan ) dan variabel global ( tumpukan ). Memori tidak dapat menyimpan pointer yang menunjuk ke unit memori, variabel global digunakan untuk menyimpan pointer yang menunjuk ke unit memori.

Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan, memudahkan implementasi dan kontrol, cocok untuk skenario blockchain. Nilai dari jenis sumber daya hanya bisa dipindahkan secara destruktif.

Status eksekusi program Move adalah kuartet ⟨C, M, G, S⟩, yang mencakup tumpukan panggilan, memori, variabel global, dan operand. Selama eksekusi, pemanggilan fungsi menciptakan objek tumpukan panggilan baru, instruksi cabang melakukan lompatan statis, menghindari pengiriman dinamis.

MoveVM memisahkan penyimpanan data dan tumpukan pemanggilan, berbeda dengan desain EVM. Desain ini meskipun mengorbankan fleksibilitas, tetapi meningkatkan keamanan dan efisiensi eksekusi.

3. Pindahkan Prover

Move Prover adalah alat verifikasi formal berbasis inferensi, yang menggunakan bahasa formal untuk mendeskripsikan perilaku program, dan menggunakan algoritma inferensi untuk memverifikasi apakah program tersebut sesuai dengan yang diharapkan.

Arsitektur Move Prover adalah sebagai berikut:

1. Menerima input file sumber Move, termasuk spesifikasi program.
2. Parser mengekstrak spesifikasi, compiler mengkompilasi kode sumber menjadi bytecode.
3. Mengonversi ke model objek validator.
4. Terjemahkan ke dalam bahasa menengah Boogie.
5. Sistem verifikasi Boogie menghasilkan syarat verifikasi.
6. Z3 solver memeriksa apakah formula SMT tidak dapat dipenuhi.
7. Menghasilkan laporan diagnosa dan mengembalikannya ke kesalahan tingkat sumber.

Move menggunakan Move Specification Language untuk mendeskripsikan spesifikasi, merupakan subset dari bahasa Move.

Move Prover adalah alat yang berguna, dapat membantu pengembang memastikan keakuratan smart contract, mengurangi risiko transaksi.

Ringkasan

Bahasa Move sangat unggul dalam desain keamanan, mempertimbangkan berbagai aspek mulai dari fitur bahasa, eksekusi mesin virtual, hingga alat keamanan. Bahasa ini mengorbankan sebagian fleksibilitas, memperkuat pemeriksaan tipe dan logika linier, sehingga 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 EVM seperti reentrancy, overflow, dan injection, tetapi masalah seperti otentikasi, logika, dan overflow bilangan bulat besar masih perlu diperhatikan oleh pengembang. Meskipun Move mempertimbangkan keamanan dengan baik, tetap disarankan untuk menggunakan layanan audit dari perusahaan keamanan pihak ketiga, dan menyerahkan penulisan dan verifikasi kode yang sesuai kepada tim keamanan profesional.