Analisis mendalam keamanan bahasa Move: fitur bahasa, mekanisme operasi, dan audit otomatis

Pendahuluan

Bahasa Move adalah bahasa kontrak pintar yang dapat dijalankan dalam lingkungan blockchain yang mengimplementasikan MoveVM. Saat lahir, ia mempertimbangkan berbagai masalah keamanan dari blockchain dan kontrak pintar, serta merujuk pada beberapa desain keamanan dari bahasa RUST. Sebagai generasi baru bahasa kontrak pintar yang mengedepankan keamanan, seberapa aman sebenarnya Move? Dapatkah ia menghindari ancaman keamanan umum yang biasa terjadi pada mesin virtual kontrak seperti EVM, WASM, di tingkat bahasa atau mekanisme terkait? Apakah ia sendiri memiliki masalah keamanan yang khas?

Artikel ini akan membahas masalah keamanan bahasa Move dari tiga aspek: karakteristik bahasa, mekanisme operasional, dan alat verifikasi.

1. Fitur keamanan bahasa Move

Menulis kode yang benar sangat sulit, bahkan setelah diuji berkali-kali tidak ada jaminan bahwa kode tersebut benar-benar bebas dari kerentanan. Ketika berinteraksi dengan kode yang tidak tepercaya, akan lebih sulit untuk menulis kode yang dapat mempertahankan atribut keamanan yang penting. Ada banyak teknik yang dapat menegakkan keamanan runtime, seperti sandbox, isolasi proses, kunci objek, dan pola pemrograman lainnya; juga dapat ditentukan keamanan statis pada waktu kompilasi, seperti pengetikan statis yang ketat atau pemeriksaan asersi.

Terkadang dapat menggunakan analisis semantik dan alat analisis statis, untuk memastikan kode mematuhi aturan keamanan, bahkan saat berinteraksi dengan kode yang tidak tepercaya, tetap mempertahankan beberapa kontrak logis yang dapat dibuktikan.

Solusi-solusi ini tampak baik, dapat menghindari overhead saat runtime dan mendeteksi masalah keamanan lebih awal. Namun sayangnya, keamanan yang diperoleh melalui metode ini dalam bahasa pemrograman sangat terbatas, dengan dua alasan utama: pertama, mereka biasanya memiliki karakteristik yang tidak dapat digunakan dengan alat analisis statis, seperti pengiriman dinamis, variabilitas yang dapat dibagi, dan logika non-linear seperti refleksi, yang melanggar aturan invariant keamanan, memberikan para peretas luasnya permukaan serangan. Kedua, sebagian besar bahasa pemrograman sulit untuk diperluas dengan alat statis yang terkait dengan keamanan atau bahasa yang sangat ekspresif dan terencana. Meskipun kedua jenis perluasan ini penting, mereka dapat didefinisikan sebelumnya.

Berbeda dengan banyak bahasa pemrograman yang ada, bahasa Move dirancang dengan mempertimbangkan dukungan untuk menulis program yang berinteraksi secara aman dengan kode yang tidak terpercaya, sambil mendukung verifikasi statis. Move memiliki fitur keamanan seperti itu karena mengabaikan semua logika non-linier yang didasarkan pada pertimbangan fleksibilitas, tidak mendukung pengiriman dinamis, dan juga tidak mendukung panggilan eksternal yang rekursif, melainkan menggunakan konsep generik, penyimpanan global, sumber daya, dan lain-lain untuk mewujudkan beberapa pola pemrograman alternatif. Misalnya, Move menghilangkan fitur penjadwalan dinamis dan pemanggilan rekursif, fitur-fitur ini dalam bahasa kontrak pintar lainnya menyebabkan kerentanan reentrancy yang mahal.

Untuk lebih memahami karakteristik bahasa Move, mari kita lihat program contoh:

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

const ADMIN: address = @0x1;

struct Coin memiliki kunci, menyimpan {
    nilai: u64
}

struct Info memiliki kunci {
    total_supply: u64
}

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

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

public fun mint(account: &signer, amount: u64): Info koin diperoleh {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Koin { nilai: jumlah }
}

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

publik fun value_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value  
}

}

a) Modul(: Setiap modul Move terdiri dari serangkaian tipe struktur dan definisi proses. Modul dapat mengimpor definisi tipe dan memanggil proses yang dinyatakan di modul lain. Nama lengkap modul dimulai dengan alamat akun 16 byte yang menyimpan kode modul. Alamat akun berfungsi sebagai ruang nama untuk membedakan modul dengan nama yang sama.

b) Struktur): Modul ini mendefinisikan dua struktur Coin dan Info. Coin mewakili token yang dialokasikan untuk pengguna, Info mencatat total jumlah token. Kedua struktur didefinisikan sebagai jenis sumber daya, dapat disimpan dalam penyimpanan kunci/nilai global yang permanen.

c( Proses)function): Kode mendefinisikan satu proses inisialisasi, satu proses aman, dan satu proses tidak aman. Proses initialize harus dipanggil sebelum membuat Coin, untuk menginisialisasi total_supply nilai Info instan menjadi nol. signer adalah jenis khusus yang menunjukkan pengguna yang diverifikasi oleh logika eksternal Move. Assert memastikan hanya akun administrator yang ditentukan yang dapat memanggil proses ini. Proses mint memungkinkan administrator untuk membuat token baru, juga dengan kontrol akses. Proses value_mut menerima referensi variabel Coin, dan mengembalikan referensi variabel ke bidang value.

Struktur kontrak mirip dengan bahasa kontrak pintar lainnya, tetapi tipe sumber daya dan penyimpanan global adalah mekanisme kunci untuk penyimpanan dan keamanan sumber daya dalam bahasa Move.

Penyimpanan global memungkinkan program Move untuk menyimpan data persisten, yang hanya dapat dibaca dan ditulis secara pemrograman oleh modul yang memilikinya, tetapi disimpan di buku besar publik, sehingga pengguna modul lain dapat melihatnya. Setiap kunci dalam penyimpanan global terdiri dari nama tipe yang sepenuhnya terqualified dan alamat akun yang menyimpan nilai tipe tersebut. Meskipun penyimpanan global dibagikan di antara semua modul, setiap modul memiliki hak akses baca dan tulis eksklusif untuk kunci yang dinyatakannya.

Modul yang menyatakan jenis sumber daya dapat: • Menerbitkan nilai ke penyimpanan global melalui instruksi move_to • Menghapus nilai dari penyimpanan global menggunakan perintah move_from • Mengambil referensi nilai dalam penyimpanan global melalui instruksi borrow_global_mut

Modul dapat memaksakan kendala pada penyimpanan global yang dikontrolnya. Misalnya, memastikan bahwa hanya alamat akun ADMIN yang dapat memiliki struktur tipe Info, yang diimplementasikan dengan mendefinisikan proses initialize, yang menggunakan move_to pada tipe Info, dan memaksakan syarat sebelum bahwa move_to dipanggil pada alamat ADMIN.

Berikut adalah dua mekanisme fitur pemeriksaan statis yang menjamin keamanan kode modul: pengurangan invarian dan verifikasi bytecode.

a( Pemeriksaan invarian ) Pemeriksaan spesifikasi ): Baris 10 modul menunjukkan invarian pemeriksaan statis — jumlah nilai field dari semua objek Coin dalam sistem harus sama dengan field total_value dari objek Info yang disimpan di alamat ADMIN. Invarian adalah istilah dalam verifikasi formal yang menunjukkan konservasi status. Properti konservasi ini berlaku untuk semua klien yang mungkin dari modul.

b( Verifier bytecode: Tipe keamanan dan linearitas adalah ruang lingkup utama verifikasi oleh verifier bytecode. Meskipun modul lain tidak dapat mengakses unit penyimpanan global yang dikendalikan oleh 0x1::TestCoin::Coin, mereka dapat menggunakan tipe ini dalam deklarasi proses dan struktur mereka sendiri.

Move memiliki validator bytecode ) yang menegakkan sistem tipe di tingkat bytecode ), memungkinkan pemilik modul untuk mencegah hasil yang tidak diinginkan. Hanya modul yang mendeklarasikan tipe struktur Coin yang dapat: • Buat nilai tipe Coin • "Membongkar" nilai tipe Coin ke dalam field komponennya • Mendapatkan referensi ke bidang Coin melalui peminjaman yang dapat diubah atau tidak dapat diubah dengan gaya rust

Validator juga memaksa struktur secara default menjadi linier, untuk memastikan pencegahan salinan dan penghancuran secara linier di luar modul yang menyatakan struktur. Pada saat yang sama, validator juga akan melakukan pemeriksaan paksa terhadap beberapa jenis masalah memori umum.

Proses pengujian terdiri dari tiga kategori utama: 1( Pemeriksaan validitas struktur: menjamin integritas bytecode, mendeteksi kesalahan referensi ilegal, entitas sumber daya duplikat, dan tanda tangan tipe ilegal, dll. 2) Deteksi semantik logika proses: termasuk kesalahan tipe parameter, indeks loop, indeks kosong, dan definisi variabel yang berulang. 3) Kesalahan saat menghubungkan, pemanggilan proses internal yang tidak sah, atau proses yang menyatakan dan mendefinisikan tidak cocok.

Validator pertama membuat CFG) graf aliran kontrol ), kemudian mendeteksi cakupan akses pemanggil di dalam tumpukan, memastikan bahwa pemanggil kontrak tidak dapat mengakses ruang tumpukan pemanggil. Sementara itu, untuk memeriksa tipe, setiap tumpukan Value mempertahankan tumpukan Type yang sesuai.

Selanjutnya adalah pemeriksaan sumber daya dan pemeriksaan referensi. Pemeriksaan sumber daya terutama memeriksa larangan penggandaan, ketidakberdayaan untuk dihancurkan, dan kepemilikan yang harus ada. Pemeriksaan referensi menggabungkan analisis dinamis dan statis, menggunakan mekanisme pemeriksaan pinjam yang mirip dengan sistem tipe rust.

Terakhir adalah pemeriksaan tautan, perlu memeriksa kembali apakah objek tautan dan pernyataan cocok, serta kontrol akses proses.

( 2. Mekanisme Operasi Move

Pertama, program Move berjalan di dalam mesin virtual, yang tidak dapat mengakses memori sistem saat berjalan. Ini memungkinkan Move untuk berjalan dengan aman di lingkungan yang tidak terpercaya, tanpa risiko kerusakan atau penyalahgunaan.

Kedua, program Move dijalankan di tumpukan. Penyimpanan global dibagi menjadi memori ) tumpukan ### dan variabel global ( tumpukan ). Memori adalah penyimpanan tingkat pertama, yang unitnya tidak dapat menyimpan pointer yang menunjuk ke unit memori. Variabel global digunakan untuk menyimpan pointer yang menunjuk ke unit memori, tetapi cara indeksnya berbeda. Saat mengakses variabel global, kode menyediakan alamat dan tipe yang terikat pada alamat tersebut. Pembagian ini menyederhanakan operasi, menjadikan semantik bahasa Move lebih mudah diformalkan.

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

Dalam Move, nilai yang didefinisikan sebagai sumber daya hanya dapat dipindahkan secara destruktif ( sehingga lokasi penyimpanan yang menyimpan nilai tersebut menjadi tidak valid ), tetapi beberapa nilai ( seperti integer ) dapat disalin.

Ketika program Move berjalan di atas tumpukan, statusnya adalah kuartet ⟨C, M, G, S⟩, yang terdiri dari tumpukan panggilan (C), memori (M), variabel global (G), dan operand (S). Tumpukan juga memelihara tabel fungsi ( modul itu sendiri ) untuk mem-parsing instruksi yang berisi tubuh fungsi.

Tumpukan panggilan berisi semua informasi konteks dan nomor instruksi yang terkait dengan eksekusi prosedur. Saat instruksi Call dieksekusi, objek tumpukan panggilan baru dibuat, parameter panggilan disimpan ke dalam memori dan variabel global, kemudian interpreter menjalankan instruksi kontrak baru. Ketika instruksi percabangan ditemukan, lompatan statis terjadi di dalam prosedur ini. Ketergantungan prosedur dalam modul bersifat tanpa siklus, dan ditambah dengan tidak adanya penugasan dinamis dalam modul, memperkuat ketidakberubahan pemanggilan fungsi selama eksekusi: kerangka panggilan prosedur pasti berdekatan, menghindari kemungkinan reentrancy. Pemanggilan return mengakhiri pemanggilan, dan nilai yang dikembalikan diletakkan di puncak tumpukan.

Penelitian terhadap kode MoveVM menunjukkan bahwa MoveVM memisahkan penyimpanan data dan logika proses tumpukan panggilan (, yang merupakan perbedaan terbesar dibandingkan EVM. Di EVM, untuk mengimplementasikan Token ERC20, logika harus ditulis dengan baik dalam satu kontrak dan mencatat status setiap pengguna, sedangkan di MoveVM, status pengguna ) disimpan secara independen di bawah alamat akun (, dan pemanggilan program harus mematuhi aturan ketat tentang hak akses dan sumber daya. Meskipun ini牺牲了一定灵活性, tetapi dalam hal keamanan dan efisiensi eksekusi ) sangat membantu untuk meningkatkan pelaksanaan paralel (.

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

) 3. Pindahkan Prover

Terakhir, mari kita kenali alat audit otomatisasi bantu yang disediakan oleh Move, yaitu Move prover.

Move Prover adalah alat verifikasi formal berbasis inferensi. Ini menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma inferensi untuk memverifikasi apakah program sesuai dengan yang diharapkan, membantu pengembang memastikan keakuratan kontrak pintar, dan mengurangi risiko transaksi. Singkatnya, verifikasi formal adalah metode matematis untuk membuktikan bahwa sistem bebas dari Bug.

Saat ini, algoritma verifikasi perangkat lunak otomatis yang dominan didasarkan pada solver SMT (. Solver SMT pada dasarnya adalah pemecah formula. Algoritma verifikasi perangkat lunak tingkat atas membagi tujuan verifikasi menjadi formula, yang kemudian diserahkan kepada solver SMT untuk diselesaikan, berdasarkan hasilnya dilakukan analisis lebih lanjut, dan akhirnya melaporkan apakah tujuan verifikasi terpenuhi atau menemukan kontra contoh.

Algoritma verifikasi dasar adalah verifikasi deduktif )deductive verification###, serta algoritma verifikasi lainnya seperti pemeriksaan model terbatas, metode k-induksi, abstraksi predikat, dan abstraksi jalur.

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, memastikan kesesuaian dengan perilaku yang diharapkan. Ini membantu memastikan kebenaran program dan mengurangi beban kerja pengujian manual.

Arsitektur keseluruhan Move Prover adalah sebagai berikut:

Pertama, Move Prover menerima file sumber Move yang berisi spesifikasi input program (specification). Move Parser mengekstrak spesifikasi dari kode sumber. Compiler Move mengkompilasi file sumber menjadi bytecode, yang bersama dengan sistem spesifikasi diubah menjadi model objek verifikator (Prover Object Model).

Model ini diterjemahkan ke dalam bahasa perantara Boogie. Kode Boogie dikirim ke sistem verifikasi Boogie untuk "generasi kondisi verifikasi". Kondisi verifikasi dikirim ke solver Z3 (, solver SMT yang dikembangkan oleh Microsoft ).

Setelah VC dimasukkan ke dalam Z3, pemeriksa memeriksa apakah kode program SMT formula ( memenuhi spesifikasi ) yang tidak dapat dipenuhi. Jika ya, berarti spesifikasi tersebut terpenuhi. Jika tidak, menghasilkan model yang memenuhi kondisi, mengonversi kembali ke format Boogie untuk menerbitkan laporan diagnosis. Laporan diagnosis dipulihkan menjadi kesalahan tingkat sumber yang mirip dengan kesalahan kompilator standar.

![Move安