Analisis Keamanan Bahasa Move: Pengubah Bahasa Kontrak Pintar
Pendahuluan
Bahasa Move adalah bahasa kontrak pintar yang dapat dijalankan di lingkungan blockchain yang mengimplementasikan MoveVM. Desainnya mempertimbangkan berbagai masalah keamanan yang berkaitan dengan blockchain dan kontrak pintar, serta mengambil inspirasi dari beberapa ide desain keamanan bahasa Rust. Sebagai generasi baru bahasa kontrak pintar yang memiliki keamanan sebagai fitur utamanya, seberapa aman Move? Apakah ia dapat menghindari ancaman keamanan umum yang ada pada mesin virtual kontrak seperti EVM, WASM, pada tingkat bahasa atau mekanisme terkait? Apakah Move sendiri memiliki masalah keamanan yang khas?
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, bahasa Move dirancang untuk mendukung interaksi yang aman dengan kode yang tidak tepercaya, serta mendukung verifikasi statis. Move mengabaikan logika non-linear yang berbasis pada fleksibilitas, tidak mendukung pengiriman dinamis dan panggilan eksternal rekursif, melainkan menggunakan konsep generik, penyimpanan global, dan sumber daya untuk mewujudkan pola pemrograman alternatif. Misalnya, Move menghilangkan penjadwalan dinamis dan fitur panggilan rekursif yang dapat menyebabkan kerentanan reentrancy.
Fitur keamanan utama dari Move termasuk:
Modul: Setiap modul Move terdiri dari serangkaian tipe struktur dan definisi proses. Modul dapat mengimpor definisi tipe dan memanggil proses yang dideklarasikan dalam modul lain.
Struktur: dapat didefinisikan sebagai jenis sumber daya, yang menunjukkan dapat disimpan dalam penyimpanan kunci/nilai global yang persisten.
Proses: mendefinisikan inisialisasi, proses keamanan, dan proses yang tidak aman.
Penyimpanan global: Memungkinkan program Move menyimpan data permanen, data ini hanya dapat dibaca dan ditulis secara pemrograman oleh modul yang memilikinya.
Pemeriksaan invarian: Mendukung pemeriksaan invarian statis, memastikan integritas sumber daya dalam sistem.
Verifikasi Bytecode: Menegakkan sistem tipe di tingkat bytecode, mencegah operasi ilegal dari modul klien jahat.
Dengan memeriksa invarian dan mekanisme verifikasi bytecode, Move mencapai jaminan keamanan kode ganda pada saat kompilasi.
2. Mekanisme Operasi Move
Program Move berjalan di dalam mesin virtual, dan selama waktu eksekusi tidak dapat mengakses memori sistem. Ini memungkinkan Move untuk berjalan dengan aman di lingkungan yang tidak tepercaya, tanpa risiko dirusak atau disalahgunakan.
Program Move dijalankan di tumpukan, penyimpanan global dibagi menjadi dua bagian yaitu memori ( tumpukan ) dan variabel global ( tumpukan ). Memori adalah penyimpanan tingkat satu, unitnya tidak dapat menyimpan pointer yang mengarah ke unit memori. Variabel global digunakan untuk menyimpan pointer yang mengarah ke unit memori, tetapi cara pengindeksannya berbeda dari memori.
Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan. Mesin virtual berbasis tumpukan mudah diimplementasikan dan dikendalikan, membutuhkan sedikit persyaratan lingkungan perangkat keras, dan cocok untuk skenario blockchain. Dibandingkan dengan interpreter berbasis register, interpreter berbasis tumpukan lebih mudah untuk mengontrol dan mendeteksi operasi salin dan pindah antar variabel.
Status runtime program Move adalah quadruple ⟨C, M, G, S⟩, termasuk stack panggilan (C), memori (M), variabel global (G), dan operand (S). Stack juga memelihara tabel fungsi untuk memecahkan instruksi yang mengandung tubuh fungsi.
MoveVM memisahkan logika proses penyimpanan dan panggilan tumpukan data (, ini adalah perbedaan terbesar dengan EVM. Di MoveVM, sumber daya di bawah alamat akun status pengguna ) disimpan secara terpisah, pemanggilan program harus mematuhi aturan ketat terkait izin dan sumber daya. Desain ini牺牲一定灵活性, tetapi dalam hal keamanan dan efisiensi eksekusi ( membantu mencapai peningkatan signifikan dalam pelaksanaan bersamaan ).
3. Pindahkan 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 memenuhi harapan, membantu pengembang memastikan kebenaran smart contract, dan mengurangi risiko transaksi.
Move Prover menggunakan algoritma verifikasi deduktif untuk memverifikasi apakah program sesuai dengan yang diharapkan. Ini berarti ia dapat menyimpulkan perilaku program berdasarkan informasi yang diketahui, memastikan kecocokan dengan perilaku yang diharapkan. Ini membantu menjamin kebenaran program, mengurangi beban kerja pengujian manual.
Alur kerja Move Prover adalah sebagai berikut:
Menerima file sumber Move sebagai input, file ini perlu mengatur spesifikasi input program.
Move Parser mengekstrak spesifikasi dari kode sumber.
Compiler Move mengkompilasi file sumber menjadi bytecode, bersama dengan sistem standar yang mengubahnya menjadi model objek validator.
Model ini diterjemahkan ke dalam bahasa perantara Boogie.
Kode Boogie dimasukkan ke dalam sistem verifikasi Boogie, menghasilkan kondisi verifikasi.
Kondisi verifikasi dikirim ke pemecah Z3 ( pemecah SMT yang dikembangkan oleh Microsoft ).
Z3 memeriksa apakah formula SMT tidak dapat dipenuhi. Jika iya, itu menunjukkan bahwa spesifikasi tersebut valid; jika tidak, buat model yang memenuhi kondisi.
Mengembalikan laporan diagnostik ke kesalahan tingkat kode sumber.
Move menggunakan Move Specification Language untuk mendeskripsikan spesifikasi sistem. Ini adalah subset dari bahasa Move, mendukung deskripsi statis perilaku kebenaran program, tanpa mempengaruhi produksi. Dapat ditulis secara independen sebagai dokumen spesifikasi khusus, memisahkan kode bisnis dan kode verifikasi formal.
Move Prover adalah alat yang berguna untuk membantu pengembang memastikan keakuratan smart contract. Ini menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma inferensi untuk memverifikasi apakah program sesuai dengan yang diharapkan, membantu mengurangi risiko transaksi, sehingga pengembang dapat lebih percaya diri dalam menerapkan smart contract ke lingkungan produksi.
4. Ringkasan
Bahasa Move sangat luar biasa dalam desain keamanan, dengan pertimbangan menyeluruh pada fitur bahasa, eksekusi mesin virtual, dan lapisan alat keamanan. Fitur bahasa mengorbankan sebagian fleksibilitas, dengan pemeriksaan tipe yang ketat dan logika linier, yang memudahkan otomatisasi pemeriksaan kompilasi dan verifikasi formal serta keamanan yang dapat diverifikasi. Desain MoveVM memisahkan status dari logika, lebih sesuai dengan kebutuhan manajemen keamanan aset di blockchain.
Dari segi bahasa, Move dapat secara efektif menghindari kerentanan umum EVM seperti reentrancy, overflow, dan injeksi Call/DeleGateCall. Namun, masalah seperti otentikasi, logika kode, dan overflow pada struktur bilangan bulat besar tetap perlu diperhatikan oleh pengembang. Move Prover mungkin tidak dapat berfungsi jika ada kelalaian dalam pemahaman keseluruhan.
Meskipun bahasa Move mempertimbangkan banyak hal untuk keamanan programmer, tidak ada bahasa dan program yang sepenuhnya aman. Disarankan bagi pengembang smart contract Move untuk menggunakan layanan audit perusahaan keamanan pihak ketiga, dan menyerahkan penulisan serta verifikasi bagian spesifikasi kode kepada perusahaan keamanan pihak ketiga.
Halaman ini mungkin berisi konten pihak ketiga, yang disediakan untuk tujuan informasi saja (bukan pernyataan/jaminan) dan tidak boleh dianggap sebagai dukungan terhadap pandangannya oleh Gate, atau sebagai nasihat keuangan atau profesional. Lihat Penafian untuk detailnya.
17 Suka
Hadiah
17
4
Bagikan
Komentar
0/400
DegenRecoveryGroup
· 08-06 15:36
Ada sesuatu, rasa rust terlalu kuat.
Lihat AsliBalas0
AlwaysAnon
· 08-06 01:22
Keamanan luar biasa tetapi ekosistemnya terlalu lemah
Analisis Keamanan Bahasa Move: Paradigma Baru untuk smart contract
Analisis Keamanan Bahasa Move: Pengubah Bahasa Kontrak Pintar
Pendahuluan
Bahasa Move adalah bahasa kontrak pintar yang dapat dijalankan di lingkungan blockchain yang mengimplementasikan MoveVM. Desainnya mempertimbangkan berbagai masalah keamanan yang berkaitan dengan blockchain dan kontrak pintar, serta mengambil inspirasi dari beberapa ide desain keamanan bahasa Rust. Sebagai generasi baru bahasa kontrak pintar yang memiliki keamanan sebagai fitur utamanya, seberapa aman Move? Apakah ia dapat menghindari ancaman keamanan umum yang ada pada mesin virtual kontrak seperti EVM, WASM, pada tingkat bahasa atau mekanisme terkait? Apakah Move sendiri memiliki masalah keamanan yang khas?
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, bahasa Move dirancang untuk mendukung interaksi yang aman dengan kode yang tidak tepercaya, serta mendukung verifikasi statis. Move mengabaikan logika non-linear yang berbasis pada fleksibilitas, tidak mendukung pengiriman dinamis dan panggilan eksternal rekursif, melainkan menggunakan konsep generik, penyimpanan global, dan sumber daya untuk mewujudkan pola pemrograman alternatif. Misalnya, Move menghilangkan penjadwalan dinamis dan fitur panggilan rekursif yang dapat menyebabkan kerentanan reentrancy.
Fitur keamanan utama dari Move termasuk:
Modul: Setiap modul Move terdiri dari serangkaian tipe struktur dan definisi proses. Modul dapat mengimpor definisi tipe dan memanggil proses yang dideklarasikan dalam modul lain.
Struktur: dapat didefinisikan sebagai jenis sumber daya, yang menunjukkan dapat disimpan dalam penyimpanan kunci/nilai global yang persisten.
Proses: mendefinisikan inisialisasi, proses keamanan, dan proses yang tidak aman.
Penyimpanan global: Memungkinkan program Move menyimpan data permanen, data ini hanya dapat dibaca dan ditulis secara pemrograman oleh modul yang memilikinya.
Pemeriksaan invarian: Mendukung pemeriksaan invarian statis, memastikan integritas sumber daya dalam sistem.
Verifikasi Bytecode: Menegakkan sistem tipe di tingkat bytecode, mencegah operasi ilegal dari modul klien jahat.
Dengan memeriksa invarian dan mekanisme verifikasi bytecode, Move mencapai jaminan keamanan kode ganda pada saat kompilasi.
2. Mekanisme Operasi Move
Program Move berjalan di dalam mesin virtual, dan selama waktu eksekusi tidak dapat mengakses memori sistem. Ini memungkinkan Move untuk berjalan dengan aman di lingkungan yang tidak tepercaya, tanpa risiko dirusak atau disalahgunakan.
Program Move dijalankan di tumpukan, penyimpanan global dibagi menjadi dua bagian yaitu memori ( tumpukan ) dan variabel global ( tumpukan ). Memori adalah penyimpanan tingkat satu, unitnya tidak dapat menyimpan pointer yang mengarah ke unit memori. Variabel global digunakan untuk menyimpan pointer yang mengarah ke unit memori, tetapi cara pengindeksannya berbeda dari memori.
Instruksi bytecode Move dieksekusi dalam interpreter berbasis tumpukan. Mesin virtual berbasis tumpukan mudah diimplementasikan dan dikendalikan, membutuhkan sedikit persyaratan lingkungan perangkat keras, dan cocok untuk skenario blockchain. Dibandingkan dengan interpreter berbasis register, interpreter berbasis tumpukan lebih mudah untuk mengontrol dan mendeteksi operasi salin dan pindah antar variabel.
Status runtime program Move adalah quadruple ⟨C, M, G, S⟩, termasuk stack panggilan (C), memori (M), variabel global (G), dan operand (S). Stack juga memelihara tabel fungsi untuk memecahkan instruksi yang mengandung tubuh fungsi.
MoveVM memisahkan logika proses penyimpanan dan panggilan tumpukan data (, ini adalah perbedaan terbesar dengan EVM. Di MoveVM, sumber daya di bawah alamat akun status pengguna ) disimpan secara terpisah, pemanggilan program harus mematuhi aturan ketat terkait izin dan sumber daya. Desain ini牺牲一定灵活性, tetapi dalam hal keamanan dan efisiensi eksekusi ( membantu mencapai peningkatan signifikan dalam pelaksanaan bersamaan ).
3. Pindahkan 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 memenuhi harapan, membantu pengembang memastikan kebenaran smart contract, dan mengurangi risiko transaksi.
Move Prover menggunakan algoritma verifikasi deduktif untuk memverifikasi apakah program sesuai dengan yang diharapkan. Ini berarti ia dapat menyimpulkan perilaku program berdasarkan informasi yang diketahui, memastikan kecocokan dengan perilaku yang diharapkan. Ini membantu menjamin kebenaran program, mengurangi beban kerja pengujian manual.
Alur kerja Move Prover adalah sebagai berikut:
Move menggunakan Move Specification Language untuk mendeskripsikan spesifikasi sistem. Ini adalah subset dari bahasa Move, mendukung deskripsi statis perilaku kebenaran program, tanpa mempengaruhi produksi. Dapat ditulis secara independen sebagai dokumen spesifikasi khusus, memisahkan kode bisnis dan kode verifikasi formal.
Move Prover adalah alat yang berguna untuk membantu pengembang memastikan keakuratan smart contract. Ini menggunakan bahasa formal untuk menggambarkan perilaku program, dan menggunakan algoritma inferensi untuk memverifikasi apakah program sesuai dengan yang diharapkan, membantu mengurangi risiko transaksi, sehingga pengembang dapat lebih percaya diri dalam menerapkan smart contract ke lingkungan produksi.
4. Ringkasan
Bahasa Move sangat luar biasa dalam desain keamanan, dengan pertimbangan menyeluruh pada fitur bahasa, eksekusi mesin virtual, dan lapisan alat keamanan. Fitur bahasa mengorbankan sebagian fleksibilitas, dengan pemeriksaan tipe yang ketat dan logika linier, yang memudahkan otomatisasi pemeriksaan kompilasi dan verifikasi formal serta keamanan yang dapat diverifikasi. Desain MoveVM memisahkan status dari logika, lebih sesuai dengan kebutuhan manajemen keamanan aset di blockchain.
Dari segi bahasa, Move dapat secara efektif menghindari kerentanan umum EVM seperti reentrancy, overflow, dan injeksi Call/DeleGateCall. Namun, masalah seperti otentikasi, logika kode, dan overflow pada struktur bilangan bulat besar tetap perlu diperhatikan oleh pengembang. Move Prover mungkin tidak dapat berfungsi jika ada kelalaian dalam pemahaman keseluruhan.
Meskipun bahasa Move mempertimbangkan banyak hal untuk keamanan programmer, tidak ada bahasa dan program yang sepenuhnya aman. Disarankan bagi pengembang smart contract Move untuk menggunakan layanan audit perusahaan keamanan pihak ketiga, dan menyerahkan penulisan serta verifikasi bagian spesifikasi kode kepada perusahaan keamanan pihak ketiga.