Move dili güvenlik analizi: Akıllı sözleşme dili için oyun kurallarını değiştiren

Move dili, MoveVM'yi gerçekleştiren blok zinciri ortamında derlenip çalıştırılabilen bir akıllı sözleşme dilidir. Doğduğu günden itibaren birçok blok zinciri ve akıllı sözleşmenin güvenlik sorunlarını dikkate almış ve RUST dilinin bazı güvenlik tasarımlarından faydalanmıştır. Güvenliği ana özellik olarak öne çıkan yeni nesil bir akıllı sözleşme dili olarak, Move'un güvenliği gerçekten nasıldır? Dil düzeyinde veya ilgili mekanizmalarla EVM, WASM gibi sözleşme sanal makinelerinde sıkça görülen güvenlik tehditlerinden kaçınabilir mi? Kendisi özel güvenlik riskleri barındırıyor mu?

Bu makale, Move dilinin güvenlik sorunlarını dil özellikleri, çalışma mekanizması ve doğrulama araçları üç yönüyle ele alacaktır.

1. Move dilinin güvenlik özellikleri

Mevcut birçok programlama dilinden farklı olarak, Move dilinin tasarım hedefi, güvenilmeyen kodlarla güvenli bir şekilde etkileşimde bulunabilen programların yazımını desteklemek ve aynı zamanda statik doğrulamayı sağlamaktır. Bu hedefe ulaşmak için, Move esneklik dikkate alınarak geliştirilmiş doğrusal mantığı terk etmiş, dinamik dağıtım ve dışarıdan özyinelemeli çağrıları desteklememiş, bunun yerine genel türler, global depolama, kaynaklar gibi kavramları tanıtarak alternatif bir programlama modeli geliştirmiştir. Örneğin, Move dinamik yönlendirme ve özyinelemeli çağrı özelliklerini atlamıştır; bu özellikler diğer akıllı sözleşme dillerinde pahalı yeniden giriş açıklarına neden olabilir.

Move'un temel güvenlik özellikleri şunlardır:

1. Modül (: Her Move modülü bir dizi yapı tipi ve süreç tanımından oluşur. Modül, diğer modüllerde tanımlanan tür tanımlarını içe aktarabilir ve süreçleri çağırabilir.

2. Yapı)Structs(: Kaynak türü olarak tanımlanabilir, kalıcı küresel anahtar/değer depolamasında saklanabilir.

3. süreç )Fonksiyon (: modülün davranış mantığını tanımlama.

4. Küresel Depolama: Move programlarının kalıcı verileri depolamasına izin verir, bu veriler yalnızca onu sahip olan modüller tarafından programatik olarak okunabilir ve yazılabilir.

5. Değişmezlik Kontrolü: Sistem durumunun korunmasını sağlamak için statik kontrol değişmezlikleri tanımlanabilir.

6. Bytecode doğrulayıcı: Bytecode seviyesinde tür sistemini zorlar, yasadışı işlemleri önler.

Move, bu özellikler aracılığıyla derleme zamanında kodun güvenliğini sağlar. Sonraki adımda Move'un çalışma mekanizmasını analiz edeceğiz, MoveVM'nin çalışma zamanında güvenliği nasıl sağladığını göreceğiz.

![Move güvenliği analizi: akıllı sözleşmeler dilinin Oyun Değiştiricisi])https://img-cdn.gateio.im/webp-social/moments-419437619d55298077789e6eca578b48.webp(

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

Move programı sanal makine üzerinde çalışır, çalışma zamanında sistem belleğine erişemez, bu da Move'un güvenilmeyen ortamlarda güvenli bir şekilde çalışmasını sağlar. Move programı yığında çalışır, küresel depolama bellek ) yığın ( ve küresel değişken ) yığını ( olmak üzere iki parçaya ayrılmıştır. Bellek birinci dereceden depolamadır, bellek hücrelerine işaret eden işaretçileri saklayamaz. Küresel değişkenler bellek hücrelerine işaret eden işaretçileri saklamak için kullanılır, ancak indeksleme yöntemi bellekten farklıdır.

Move'nin bytecode talimatları yığın tabanlı yorumlayıcıda yürütülür. Yığın sanal makinesi uygulanması ve kontrol edilmesi kolaydır, donanım ortamı için daha düşük gereksinimlere sahiptir ve blok zinciri senaryoları için uygundur. Kayıt tabanlı yorumlayıcıya kıyasla, yığın tabanlı yorumlayıcı, değişkenler arasındaki kopyalama ve hareketi kontrol etme ve denetleme açısından daha kolaydır.

Move programı çalışırken, durumu ⟨C, M, G, S⟩ dörtlü kümesi şeklindedir ve şunları içerir: çağrı yığını )C(, bellek )M(, küresel değişkenler )G( ve işlemci yığınları )S(. Yığın ayrıca, fonksiyon gövdesini içeren talimatları çözümlemek için fonksiyon tablosu ) modülünü de korur.

MoveVM, verileri depolama ve çağrı yığını ( işlem mantığını ) ayırır, bu EVM ile en büyük farktır. MoveVM'de, kullanıcı durumu ( hesap adresinin altındaki kaynaklar ) bağımsız olarak depolanır, program çağrıları izin ve kaynaklarla ilgili zorunlu kurallara uymalıdı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 iyileşme sağlanmıştır.

3. Move Prover

Move Prover, akıllı sözleşmelerin doğruluğunu sağlamak için geliştiricilere yardımcı olan, program davranışını tanımlamak için formel dil kullanan ve programın beklenenlerle uyumlu olup olmadığını doğrulamak için akıl yürütme algoritmaları kullanan bir akıl yürütmeye dayalı formel doğrulama aracıdır. Bu sayede işlem riskini azaltır.

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

Move Prover'ın iş akışı aşağıdaki gibidir:

1. Move kaynak dosyasını girdi olarak al, bu dosya program girdi standartlarını (specification) olarak ayarlamalıdır.

2. Move Parser, kaynak kodundan standartları çıkarır.

3. Move derleyicisi kaynak dosyayı bayt koduna çevirir, standart sistemle birlikte doğrulayıcı nesne modeline (Prover Object Model) dönüştürür.

4. Modeli Boogie ara diline çevirin.

5. Boogie doğrulama sistemi girdi için "doğrulama koşulu oluşturma"(verification condition generation).

6. Doğrulama koşullarını Z3 çözücüsüne ( Microsoft'un geliştirdiği SMT çözücüsü ).

7. Z3, SMT formülünün ( program kodunun specification规范) ile karşılayıp karşılamadığını kontrol eder.

8. Eğer yerine getirilemezse, standart kurulur; aksi takdirde, koşulları karşılayan bir model oluşturulur ve Boogie formatına dönüştürülerek teşhis raporu yayınlanır.

9. Teşhis raporunu kaynak kodu seviyesindeki hatalara geri döndür.

Move, Move Spesifikasyon Dili kullanarak sistemin gereksinimlerini tanımlar. Bu dil, Move'un bir alt kümesidir ve programın doğru davranışını statik olarak tanımlamayı destekler, üretimi etkilemez. İş kodu ile biçimsel doğrulama kodunu ayıran özel bir gereksinim dosyası bağımsız olarak yazılabilir.

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına yardımcı olan yararlı bir araçtır. Program davranışını tanımlamak için biçimsel bir dil kullanır ve programın bekleneni karşılayıp karşılamadığını doğrulamak için çıkarım algoritmaları kullanır. Bu, işlem riskini azaltmaya yardımcı olur ve geliştiricilerin akıllı sözleşmeleri üretim ortamına daha güvenle dağıtabilmelerini sağlar.

4. Ö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ı açısından kapsamlı bir şekilde düşünülmüştür. Dil özellikleri, bazı esnekliklerden feragat ederek, zorunlu tür kontrolü ve doğrusal mantık ile derleme kontrolü ve biçimsel doğrulamanın otomatikleştirilmesi ve güvenli doğrulanabilirlik açısından kolaylık sağlar. MoveVM tasarımı, durumu mantıktan ayırarak, blockchain üzerindeki varlık güvenliği yönetimi ihtiyaçlarına daha uygun bir yaklaşım benimsemektedir.

Dil seviyesinde, Move, EVM'de sıkça görülen yeniden giriş, taşma, Call/DeleGateCall enjeksiyonu gibi açıkları etkili bir şekilde önleyebilir. Ancak kimlik doğrulama, kod mantığı, büyük tamsayı yapısı taşmaları gibi sorunlar hala geliştiricilerin dikkat etmesi gereken konulardır. Move Prover, genel anlamda dikkatsizlik durumunda etkili olamayabilir.

Move dilinin güvenlik açısından programcılar için birçok şey düşündüğü halde, tamamen güvenli bir dil ya da tamamen güvenli bir program yoktur. Move akıllı sözleşmeler geliştiricilerine üçüncü taraf güvenlik şirketlerinin denetim hizmetlerini kullanmalarını ve spesifikasyon kısmındaki kod yazımını ve doğrulamasını üçüncü taraf güvenlik şirketlerine devretmelerini öneririz.