Move dilinin güvenlik derinliği analizi: dil özellikleri, çalışma mekanizması ve otomatik denetim

Giriş

Move dili, MoveVM'yi gerçekleştiren blok zinciri ortamında çalışan bir akıllı sözleşme dilidir. Doğduğunda blok zinciri ve akıllı sözleşmelerle ilgili birçok güvenlik sorununu göz önünde bulundurarak geliştirilmiş ve RUST dilinin bazı güvenlik tasarımlarından referans almıştır. Güvenliğin ana özellik olarak öne çıktığı yeni nesil bir akıllı sözleşme dili olarak, Move'un güvenliği gerçekte nasıldır? Dili seviyesinde veya ilgili mekanizmalarla EVM, WASM gibi sözleşme sanal makinelerinin yaygın güvenlik tehditlerinden kaçınabilir mi? Kendisi özel güvenlik sorunlarına sahip mi?

Bu makale, Move dilinin güvenlik sorunlarını dil özellikleri, çalışma mekanizması ve doğrulama araçları açısından inceleyecektir.

1. Move dilinin güvenlik özellikleri

Doğru kod yazmak zordur; defalarca test edilse bile kodun tamamen hatasız olduğunu garanti edemezsiniz. Güvenilmeyen kodlarla etkileşim kurarken, temel güvenlik özelliklerini koruyan kod yazmak daha da zorlaşır. Çalışma zamanı güvenliğini zorlamak için kumanda kutusu, işlem izolasyonu, nesne kilitleme gibi birçok teknik vardır; derleme zamanında statik güvenliği belirtmek için de güçlü statik türler veya iddia denetimleri gibi yöntemler kullanılabilir.

Bazen, güvenlik kurallarına uygunluğunu sağlamak için anlamsal analiz ve statik analiz araçlarından yararlanmak mümkündür; bu, güvenilmeyen kodlarla etkileşimde bulunulsa bile bazı kanıtlanabilir mantıksal kuraların değişmeden kalmasını sağlar.

Bu çözümler iyi görünüyor, çalışma zamanı maliyetlerini önleyebilir ve güvenlik sorunlarını önceden tespit edebilir. Ancak ne yazık ki, programlama dilleri bu yöntemlerle elde edilen güvenlik son derece sınırlıdır, bunun başlıca iki nedeni vardır: İlk olarak, genellikle statik analiz araçlarıyla kullanılamayan özelliklere sahiptirler; dinamik dağıtım, paylaşılan değişkenlik ve yansıma gibi doğrusal olmayan mantık, güvenlik değişmezliği kurallarını ihlal eder ve bilgisayar korsanlarına geniş bir saldırı yüzeyi sunar. İkincisi, çoğu programlama dili, güvenlikle ilgili statik araçlar veya ifade gücü yüksek kurallı dillerle genişletmekte zorluk çeker. Her iki genişletme de önceden tanımlanabilir ve önemlidir.

Mevcut birçok programlama dilinden farklı olarak, Move dili tasarlanırken güvensiz kodlarla güvenli etkileşim sağlayacak programların yazılmasını destekleyecek şekilde düşünülmüş ve aynı zamanda statik doğrulama desteği sunulmuştur. Move'un bu tür güvenlik özelliklerine sahip olmasının nedeni, esneklik kaygısına dayanan tüm lineer olmayan mantıkların terk edilmesi, dinamik dağıtımın desteklenmemesi ve dış çağrıların özyinelemeli olarak desteklenmemesidir; bunun yerine, bazı alternatif programlama modellerini gerçekleştirmek için generik, küresel depolama, kaynak gibi kavramlar kullanılmıştır. Örneğin, Move dinamik zamanlama ve özyinelemeli çağrı özelliklerini atlamaktadır; bu özellikler diğer akıllı sözleşme dillerinde maliyetli reentrancy açıklarına yol açmaktadır.

Move dilinin özelliklerini daha iyi anlamak için bir örnek programa bakalım:

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

const ADMIN: address = @0x1;

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

struct Info anahtar {
    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(account: &signer) {
    assert!(imzalayan::address_of(hesap) == YÖNETİCİ, 0);
    move_to(hesap, Bilgi { toplam_tedarik: 0 })
}

public fun mint(account: &signer, amount: u64): Coin edinme Bilgisi {
    assert!(signer::address_of(account) == ADMIN, 0);
    
    let supply = borrow_global_mut\u003cinfo\u003e(ADMIN);
    supply.total_supply = supply.total_supply + amount;
    
    Coin { değer: miktar }
}

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

genel eğlence değer_mut(coin: &mut Coin): &mut u64 {
    &mut coin.value  
}

}

a) Modül(Module): Her Move modülü, bir dizi yapı tipi ve süreç tanımından oluşur. Modüller, tip tanımlarını içe aktarabilir ve diğer modüllerde tanımlanan süreçleri çağırabilir. Modülün tam nitelikli adı, modül kodunun depolandığı 16 baytlık hesap adresi ile başlar. Hesap adresi, aynı isimdeki modülleri ayırt etmek için bir ad alanı olarak kullanılır.

b) Yapılar(: Bu modül, Coin ve Info adında iki yapıyı tanımlar. Coin, kullanıcılara dağıtılan token'i temsil eder, Info ise token'in toplam miktarını kaydeder. Her iki yapı da kaynak türü olarak tanımlanmıştır ve kalıcı küresel anahtar/değer depolama alanında saklanabilir.

c) süreç)function(: Kod, bir başlatma, bir güvenli süreç ve bir güvensiz süreç tanımlar. Coin oluşturulmadan önce initialize süreci çağrılmalıdır, singleton Info değerinin total_supply'ı sıfıra başlatılmalıdır. signer, Move dışı mantık tarafından doğrulanan kullanıcıyı temsil eden özel bir türdür. Assert, yalnızca belirtilen yönetici hesabının bu süreci çağırabileceğini garanti eder. mint süreci, yöneticinin yeni token'lar oluşturmasına izin verir, yine erişim kontrolü vardır. value_mut süreci, Coin'in değişken referansını alır ve value alanına değişken bir referans döner.

Sözleşme yapısı diğer akıllı sözleşme dilleriyle benzerlik gösterirken, kaynak türleri ve global depolama, Move dilindeki depolama ve kaynak güvenliğinin ana mekanizmalarıdır.

Küresel depolama, Move programlarının kalıcı verileri saklamasına izin verir. Bu veriler, yalnızca sahip olduğu modül tarafından programlı bir şekilde okunup yazılabilir, ancak kamu defterinde saklanır ve diğer modül kullanıcıları tarafından görüntülenebilir. Küresel depolamadaki her anahtar, tamamen nitelikli bir tür adı ve bu türün değerini depolayan hesap adresinden oluşur. Küresel depolama tüm modüller arasında paylaşılsa da, her modülün beyan ettiği anahtar üzerinde ayrıcalıklı okuma ve yazma erişimi vardır.

Kaynak türünü belirten modül şunları yapabilir: • Değerleri global depolamaya yayınlamak için move_to komutunu kullanın • move_from komutunu kullanarak küresel depolamadan değeri kaldırın • borrow_global_mut komutunu kullanarak global depolamada bir değerin referansını alın

Modül, kontrol ettiği küresel depolama üzerinde zorunlu kısıtlamalar uygulayabilir. Örneğin, yalnızca ADMIN hesap adresinin Info türündeki yapıların sahibi olmasını sağlamak için initialize sürecini tanımlayarak bunu gerçekleştirebiliriz. Bu süreç, Info türü üzerinde move_to kullanır ve move_to'nun ADMIN adresinde çağrılması için ön koşulları zorunlu kılar.

Aşağıda bu modül kodunun güvenliğini sağlamak için iki statik kontrol özellik mekanizması bulunmaktadır: değişmezlik azaltma ve bytecode doğrulayıcı.

a) Değişmez Kontrol ) şart kontrolü (: Modülün 10. satırı, statik kontrolün değişmezini belirtir - sistemdeki tüm Coin nesnelerinin değer alanlarının toplamı, ADMIN adresinde saklanan Info nesnesinin total_value alanına eşit olmalıdır. Değişmez, biçimsel doğrulama terimidir ve durumun korunmasını ifade eder. Bu korunma özelliği, modülün tüm olası istemcilerine uygulanır.

b) Bytecode doğrulayıcı: Güvenlik türü ve lineerleştirme, bytecode doğrulayıcısının ana doğrulama kapsamıdır. Diğer modüller 0x1::TestCoin::Coin tarafından kontrol edilen küresel depolama birimine erişemese de, bu türü kendi süreç ve yapı beyanlarında kullanabilirler.

Move, bytecode düzeyinde zorunlu bir tür sistemi ) uygulayan bir bytecode doğrulayıcısına sahiptir, bu da modül sahiplerinin istenmeyen sonuçları önlemelerine olanak tanır. Sadece Coin adlı yapı türünü beyan eden modüller şunları yapabilir: • Coin türünde bir değer oluştur • "Coin" türündeki değeri bileşen alanlarına "aç" • Coin alanına referans almak için rust tarzında değişken veya değişmez borç alarak

Doğrulayıcı, modül dışında yapı beyanını doğrulamak için kopyalama ve yok etmeyi doğrusal bir şekilde engellemek amacıyla yapıların varsayılan olarak doğrusal olmasını zorunlu kılar. Aynı zamanda, doğrulayıcı bazı türlerin yaygın bellek sorunlarına zorunlu kontroller de yapar.

Test süreci esasen üç kategoriye ayrılır: 1( Yapı denetimi: Byte kodu bütünlüğünü sağlamak, hatalı yasadışı referansları, yinelenen kaynak varlıklarını ve yasadışı tür imzalarını tespit etmek gibi. 2) Süreç mantığının anlamsal denetimi: parametre türü hataları, döngü indeksleri, boş indeksler ve tekrarlanan değişken tanımları gibi unsurları içerir. 3) Bağlantı sırasında hata, yasadışı iç süreç çağrısı veya bağlantı bildirimi ve tanımının eşleşmeyen süreci.

Doğrulayıcı öncelikle CFG) kontrol akış grafiğini ) oluşturur, ardından yığında çağrılanın erişim alanını tespit eder ve sözleşmeyi çağıranın çağıranın yığın alanına erişemeyeceğini garanti eder. Ayrıca tür kontrolü için, her Value yığını ile ilgili bir Type yığını tutulur.

Sonraki adım kaynak kontrolü ve referans kontrolüdür. Kaynaklar, çift harcama yapılamaz, yok edilemez ve mutlaka aitlik gibi kısıtlamaları kontrol eder. Referans kontrolü, dinamik ve statik analizi birleştirir ve rust tür sistemine benzer bir borç kontrol mekanizması kullanır.

Son olarak, bağlantı kontrolü yapılması gerekiyor; bağlantı nesnelerinin ve beyanların eşleşip eşleşmediği, sürecin erişim kontrolleri gibi unsurların tekrar kontrol edilmesi gerekiyor.

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

Öncelikle, Move programı sanal makinede çalışır ve çalışma zamanında sistem belleğine erişemez. Bu, Move'un güvensiz ortamlarda güvenli bir şekilde çalışmasını sağlar, bozulmaz veya kötüye kullanılmaz.

İkincisi, Move programı yığında çalışır. Küresel depolama, bellek ) yığın ### ve küresel değişkenler ( yığını ) olarak ikiye ayrılır. Bellek, birinci derece depolamadır ve hücreleri bellek hücrelerine işaret eden işaretçileri depolayamaz. Küresel değişkenler, bellek hücrelerine işaret eden işaretçileri depolamak için kullanılır, ancak indeksleme yöntemi farklıdır. Küresel değişkenlere erişildiğinde, kod adresi ve o adrese bağlanan türü sağlar. Bu ayrım, işlemleri basitleştirir ve Move dilinin anlamını daha kolay biçimlendirmeyi sağlar.

Move bytecode talimatları yığın tabanlı yorumlayıcıda yürütülür. Yığın tabanlı sanal makine uygulanması ve kontrol edilmesi kolaydır, donanım ortamı için daha az gereksinim duyar, bu nedenle blok zinciri senaryolarına uygundur. Kayıt tabanlı yorumlayıcıya göre, yığın tabanlı yorumlayıcıda değişkenler arasında kopyalama ve taşıma işlemleri daha kolay kontrol edilebilir ve tespit edilebilir.

Move'de, kaynak olarak tanımlanan değerler yalnızca yıkıcı bir şekilde taşınabilir (, bu da o değeri daha önce saklayan depolama konumunu geçersiz kılar ), ancak bazı değerler (, örneğin tam sayılar ) kopyalanabilir.

Move programı yığın üzerinde çalışırken, durumu ⟨C, M, G, S⟩ dörtlü kümesidir ve çağrı yığını (C), bellek (M), küresel değişkenler (G) ve operatörler (S) içerir. Yığın ayrıca, işlev gövdesini içeren talimatları çözmek için ( modülünün işlev tablosunu ) korur.

Çağrı yığını, işlem yürütmenin tüm bağlam bilgilerini ve talimat numarasını içerir. Call talimatı yürütüldüğünde, yeni bir çağrı yığını nesnesi oluşturulur, çağrı parametreleri bellekte ve global değişkenlerde depolanır, ardından yorumlayıcı yeni sözleşmenin talimatlarını yürütür. Dal talimatıyla karşılaşıldığında, bu süreç içinde statik bir sıçrama gerçekleşir. Modül içindeki süreçler döngüsel olmayan bağımlılıklara sahiptir, ayrıca modül dinamik atama içermez, bu da yürütme sırasında fonksiyon çağrılarının değişmezliğini güçlendirir: procedure yürütme sürecinin çağrı çerçevesi mutlaka komşudur ve yeniden girişi önler. Return çağrısı, çağrıyı sonlandırır ve dönüş değeri yığın üstüne yerleştirilir.

MoveVM kodunu incelediğimizde, MoveVM'in veri depolama ve çağrı yığınını ( işlem mantığı ) ile ayırdığı görülmektedir, bu EVM ile en büyük farktır. EVM'de ERC20 Token'ı uygulamak için mantığın bir sözleşmede düzgün bir şekilde yazılması ve her kullanıcının durumunun kaydedilmesi gerekirken, MoveVM'de kullanıcı durumu ( hesap adresindeki kaynaklar ) bağımsız olarak depolanmaktadır. Program çağrıları yetkilere ve kaynaklarla ilgili zorunlu kurallara uymak zorundadır. Bu belirli bir esnekliği feda etse de, güvenlik ve yürütme verimliliği ( açısından eşzamanlı yürütme ) konusunda büyük bir artış sağlamaktadır.

( 3. Prover Taşı

Son olarak, Move'un sağladığı yardımcı otomatik denetim aracı Move prover hakkında bilgi edinelim.

Move Prover, akıl yürütmeye dayalı bir biçimsel doğrulama aracıdır. Program davranışını tanımlamak için biçimsel bir dil kullanır ve programın beklenildiği gibi olup olmadığını doğrulamak için akıl yürütme algoritmalarını kullanır, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına ve işlem risklerini azaltmalarına yardımcı olur. Kısacası, biçimsel doğrulama, sistemin hatasız olduğunu matematiksel yöntemlerle kanıtlamaktır.

Mevcut ana akım otomatik yazılım doğrulama algoritmaları, )SMT çözücüsüne dayanan tatmin edilebilirlik model teorisi üzerindedir. SMT çözücüsü aslında formül çözücüsüdür. Üst düzey yazılım doğrulama algoritmaları, doğrulama hedefini formüllere ayırır, bunları SMT çözücüsüne teslim eder, sonuçlara göre daha fazla analiz yapar ve nihayetinde doğrulama hedefine ulaşıp ulaşmadığını veya bir karşı örnek bulup bulmadığını rapor eder.

Temel doğrulama algoritması, tümdengelim doğrulaması ###deductive verification(, ayrıca sınırlandırılmış model kontrolü, k-indüksiyon, predikat soyutlama ve yol soyutlaması gibi diğer doğrulama algoritmaları da vardır.

Move Prover, programın beklentilere uygun olup olmadığını doğrulamak için tümevarım doğrulama algoritması kullanır. Bu, Move Prover'ın bilinen bilgilere dayanarak program davranışını çıkarabileceği ve bunun beklentilerle eşleştiğini garanti edebileceği anlamına gelir. Bu, program doğruluğunu sağlamaya yardımcı olur ve manuel test iş yükünü azaltır.

Move Prover genel mimarisi aşağıdaki gibidir:

Öncelikle, Move Prover, program girdi spesifikasyonu ) olan Move kaynak dosyasını alır. Move Parser, kaynak koddan spesifikasyonu çıkarır. Move derleyicisi, kaynak dosyayı byte koduna dönüştürür ve spesifikasyon sistemi ile birlikte doğrulayıcı nesne modeline ( Prover Nesne Modeli ) dönüştürür.

Bu model Boogie ara diline çevrildi. Boogie kodu Boogie doğrulama sistemine iletilir, "doğrulama koşulu oluşturma" gerçekleştirilir. Doğrulama koşulları Z3 çözücüsüne ( Microsoft tarafından geliştirilen SMT çözücüsü ) iletilir.

VC, Z3'e iletildiğinde, doğrulayıcı SMT formülünün ( program kodunun specification规范) ile karşılanıp karşılanmadığını kontrol eder. Eğer karşılanıyorsa, bu, spesifikasyonun geçerli olduğu anlamına gelir. Aksi takdirde, koşulları karşılayan bir model oluşturulur, Boogie formatına dönüştürülür ve bir tanı raporu yayınlanır. Tanı raporu, standart bir derleyici hatasına benzer kaynak düzeyinde hatalara geri dönüştürülür.

![Move安