Move dilinin güvenliği analizi: akıllı sözleşmelerin devrimcisi

Move dili, MoveVM'i uygulayan blockchain ortamında derlenip çalıştırılabilen bir akıllı sözleşme dilidir. Güvenliği ana özellik olarak öne çıkan yeni nesil bir akıllı sözleşme dili olarak, güvenliği nasıldır? EVM, WASM gibi sözleşme sanal makinelerinin yaygın güvenlik tehditlerinden kaçınabilir mi? Bu makalede, Move dilinin güvenlik sorunları dil özellikleri, çalışma mekanizması ve doğrulama araçları olmak üzere üç düzeyde incelenecektir.

1. Move dilinin güvenlik özellikleri

Mevcut birçok programlama dilinden farklı olarak, Move dili hem güvenilmeyen kodlarla güvenli etkileşimi destekleyecek hem de statik doğrulamayı sağlayacak şekilde tasarlanmıştır. Move, esneklik düşüncesine dayanan doğrusal olmayan mantığı bir kenara bırakmış, dinamik dağıtım ve özyinelemeli dış çağrıları desteklememekte, bunun yerine jenerikler, küresel depolama, kaynaklar gibi kavramları kullanarak alternatif bir programlama modeli gerçekleştirmektedir.

Aşağıda Move dilinde bir token varlık uygulaması örneği verilmiştir:

hareket et modül 0x1::TestCoin { 0x1::imzalayıcıyı kullan

const ADMIN: address = @0x1;

struct Coin anahtar, depola { 
    değer: u64
}

struct Info anahtar içerir {
    toplam_tedarik: u64  
}

spec modülü {
    invariant forall addr: address where exists<coin>(addr):
        global<info>(ADMIN).total_supply >= global<coin>(addr).value;
}

public fun initialize(hesap: &imzalayan) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(hesap, Bilgi { toplam_arıza: 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;
    coin
}

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

}

Bu örnek, Move dilinin bazı önemli güvenlik özelliklerini göstermektedir:

1. Modülerlik: Her Move modülü, yapı tipi ve işlem tanımlarından oluşur; diğer modüllerin tür tanımlarını içe aktarabilir ve diğer modüllerin işlemlerini çağırabilir.

2. Kaynak Türü: has key veya store etiketiyle tanımlanan yapı, kalıcı global anahtar-değer depolamasında saklanabilir.

3. Küresel Depolama: Move programlarının kalıcı verileri depolamasına izin verir, yalnızca modül sahipleri tarafından programlı bir şekilde okunabilir ve yazılabilir, ancak kamu defterinde diğer modüller tarafından görüntülenebilir.

4. Erişim kontrolü: Kritik işlemlere erişim kontrolü, iddia gibi yöntemlerle gerçekleştirilebilir.

5. Değişmezlik Kuralı: Formeleştirilmiş doğrulama için statik kontrol edilebilen değişmezlikler tanımlanabilir.

6. Bayt Kodu Doğrulaması: Güvenlik türlerini ve lineerleştirme doğrulamasını içerir, yasadışı kaynak türü işlemlerini engeller.

Bu özellikler, Move dilinin derleme zamanındaki güvenliğini birlikte sağlar.

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

Move programı sanal makine içinde çalışır, sistem belleğine erişemez ve güvensiz ortamlarda güvenli bir şekilde çalışabilir.

Move programı yığın üzerinde çalışır, global depolama bellek ( yığın ) ve global değişken ( yığını ) olarak ikiye ayrılır. Bellek, bellek hücresine işaret eden işaretçileri depolayamaz, global değişkenler bellek hücresine işaret eden işaretçileri depolamak için kullanılır.

Move'un bytecode komutları, yığın tabanlı yorumlayıcıda çalıştırılır, uygulanması ve kontrol edilmesi kolaydır, blok zinciri senaryoları için uygundur. Kaynak türü değerleri yalnızca yıkıcı bir şekilde taşınabilir.

Move programının çalışma durumu ⟨C, M, G, S⟩ dörtlüsü olarak tanımlanır ve çağrı yığını, bellek, global değişkenler ve operatörleri içerir. İcra sürecinde, fonksiyon çağrıları yeni çağrı yığını nesneleri oluşturur, dallanma talimatları ise statik atlamalar gerçekleştirir ve dinamik dağıtımı önler.

MoveVM, veri depolama ve çağrı yığınını ayırır, bu EVM tasarımından farklıdır. Bu tasarım esneklikten fedakarlık etse de, güvenliği ve yürütme verimliliğini artırır.

3. Move Prover

Move Prover, program davranışını tanımlamak için biçimsel dil kullanan ve programın beklenenle uyumlu olup olmadığını doğrulamak için akıl yürütme algoritmalarını kullanan bir akıllı sözleşmeler biçimsel doğrulama aracıdır.

Move Prover mimarisi aşağıdaki gibidir:

1. Move kaynak dosya girdisini al, program spesifikasyonlarını içerir.
2. Ayrıştırıcı standartları çıkarır, derleyici kaynak kodunu bayt koduna derler.
3. Doğrulayıcı nesne modeline dönüştür.
4. Boogie ara diline çevir.
5. Boogie doğrulama sistemi doğrulama koşullarını oluşturur.
6. Z3 çözücü, SMT formülünün tatmin edilemez olup olmadığını kontrol eder.
7. Tanı raporu oluşturun ve kaynak kodu düzeyinde hataları geri yükleyin.

Move, Move dilinin bir alt kümesi olan Move Specification Language ile tanımlanır.

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına ve işlem risklerini azaltmalarına yardımcı olan yararlı bir araçtır.

Özet

Move dili, güvenlik tasarımı açısından son derece başarılıdır; dil özellikleri, sanal makine yürütmesi ve güvenlik araçları gibi birçok açıdan kapsamlı bir şekilde ele alınmıştır. Esneklikten bir miktar feragat ederek, tür kontrolünü ve lineer mantığı güçlendirmiştir, bu da derleme kontrolü ve biçimsel doğrulama için kolaylık sağlar. MoveVM, durumu ve mantığı ayırarak, blok zincir varlık güvenliği yönetim ihtiyaçlarına daha uygun hale gelmiştir.

Move dili, EVM'nin yaygın yeniden giriş, taşma, enjekte etme gibi açıklarını etkili bir şekilde önleyebilir, ancak kimlik doğrulama, mantık, büyük sayı taşması gibi sorunlar hala geliştiricilerin dikkat etmesi gereken konulardır. Move, güvenlik açısından dikkate alınmış olsa da, yine de üçüncü taraf güvenlik şirketlerinin denetim hizmetlerinin kullanılmasını ve standart kod yazımının ve doğrulamasının profesyonel güvenlik ekiplerine devredilmesini önerir.