Move dilinin güvenlik analizi

Move dili, yeni nesil bir akıllı sözleşme dili olarak, tasarımı sırasında blok zinciri ve akıllı sözleşmelerin güvenlik sorunlarını tam olarak göz önünde bulundurmuştur. Bu makale, Move dilinin güvenliğini dil özellikleri, çalışma mekanizması ve doğrulama araçları üç boyutta analiz edecektir.

1. Move dilinin güvenlik özellikleri

Move dilinin aşağıdaki birkaç ana güvenlik özelliği vardır:

• Dinamik dağıtım, özyinelemeli dış çağrılar gibi doğrusal olmayan mantıkları terk etti, yeniden giriş gibi açıkları önledi.
• Kaynak türleri ve küresel depolama mekanizmasını kullanarak depolama ve kaynakların güvenli yönetimini sağlamak
• Değişmezlik indirgeme ve bytecode doğrulayıcı ile derleme aşamasında çift güvenlik kontrolü yapmak

Aşağıda basit bir Move sözleşmesi örneği bulunmaktadır:

taşımak modül 0x1::TestCoin { 0x1::imza kullan

const ADMIN: address = @0x1;

struct Coin anahtar içerir {
    değer: u64
}

struct Bilgi anahtar içerir {
    toplam_arz: u64  
}

invariant forall addr: address where exists<coin>(addr):
    global<info>(ADMIN).toplam_tedarik >= global<coin>(addr).değer;

public fun initialize(account: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(hesap, Bilgi { toplam_tedarik: 0 });
}

public fun mint(account: &imzalayıcı, amount: u64): Coin {
    assert!(imzalayan::adres_olarak(hesap) == YÖNETİCİ, 1);
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + miktar;
    Coin { value: miktar }
}

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

}

Move, kod güvenliğini sağlamak için değişmezlik azaltmaları ve bytecode doğrulayıcıları kullanır:

1. Değişmezlik Kuralı: Sistem içindeki tüm Coin nesnelerinin değerlerinin toplamının Info'daki total_supply ile eşit olmasını sağlamak için kullanılır.

2. Bytecode doğrulayıcı: zorunlu tür kontrolü ve lineer mantık, kaynakların yasadışı bir şekilde oluşturulmasını, kopyalanmasını veya yok edilmesini önler.

2. Move'un çalışma mekanizması

Move programı sanal makinede çalışır ve aşağıdaki özelliklere sahiptir:

• Çalışma sırasında sistem belleğine erişilemez, güvensiz bir ortamda güvenli bir şekilde çalışmayı garanti eder.
• Yığın tabanlı bir yorumlayıcı ile bayt kodu talimatlarını yürütmek, uygulanması ve kontrol edilmesi kolaydır.
• Veri depolama ve çağrı yığınını ayırarak güvenliği ve yürütme verimliliğini artırın.
• Kaynaklar yalnızca yıkıcı bir şekilde taşınabilir, kopyalanamaz.

Move programının çalışma durumu dörtlü ⟨C, M, G, S⟩ ile oluşur:

• C: Çağrı Yığını
• M: Bellek ( yığın )
• G: Global değişken ( yığın )
• S: İşlemci

Bu tasarım, kullanıcı durumunu ve program mantığını ayırarak güvenliği ve eşzamanlı yürütme verimliliğini artırır.

3. Move Prover

Move Prover, akıllı sözleşmelerin doğruluğunu sağlamak için kullanılan bir biçimsel doğrulama aracıdır. İş akışı aşağıdaki gibidir:

1. Move kaynak dosyalarını ve standartlarını girdi olarak al
2. Çekim standartlarını çıkarın ve byte koduna derleyin
3. Doğrulayıcı nesne modeline dönüştür
4. Boogie orta dile çevir
5. Doğrulama koşullarını oluştur
6. Z3 çözücüsü ile formülü doğrulayın
7. Tanı raporu oluşturma

Move Prover, program spesifikasyonlarını tanımlamak için Move Specification Language kullanır. Bu dil, Move'un bir alt kümesidir ve iş kodundan bağımsız olarak spesifikasyonlar yazılabilir.

Özet

Move dili, dil özellikleri, sanal makine yürütmesi ve güvenlik araçları açısından kapsamlı bir güvenlik değerlendirmesi yapmıştır. Yeniden giriş, taşma gibi yaygın açıkları etkili bir şekilde önleyebilir, ancak kimlik doğrulama, mantık gibi sorunlara dikkat edilmesi gerekmektedir. Geliştiricilerin üçüncü taraf denetim hizmetlerini kullanmaları ve standart yazımını güvenlik şirketlerine yaptırmaları önerilir, bu da sözleşme güvenliğini daha da artıracaktır.