Move dili güvenlik analizi: akıllı sözleşmeler alanındaki yenilikçi

Move dili, MoveVM destekleyen blok zinciri ortamlarında çalışabilen akıllı sözleşme dilidir. Tasarımında blok zinciri ve akıllı sözleşmelerin birçok güvenlik sorununu göz önünde bulundurmuş ve Rust dilinin bazı güvenlik tasarım ilkelerinden faydalanmıştır. Güvenliği temel özelliklerinden biri olan yeni nesil akıllı sözleşme dili Move'un güvenliği ne kadar sağlamdır? Dil seviyesinde veya ilgili mekanizmalarla EVM, WASM gibi sözleşme sanal makinelerinin yaygın güvenlik tehditlerinden kaçınabilir mi? Move'un kendisi benzersiz güvenlik tehlikeleri taşıyor mu?

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

1. Move dilinin güvenlik özellikleri

Move dilinin tasarım hedefi, birçok mevcut programlama dilinden farklı olarak, güvenilmeyen kodlarla güvenli bir şekilde etkileşime girebilen programların yazılmasını desteklemek ve aynı zamanda statik doğrulamayı sağlamaktır. Move, esneklik düşüncesine dayanan doğrusal olmayan mantığı bir kenara bırakmış, dinamik dağıtım ve dışarıdan özyinelemeli çağrıları desteklememekte, bunun yerine genel türler, küresel depolama, kaynaklar gibi kavramları tanıtarak alternatif programlama modelleri gerçekleştirmektedir. Örneğin, Move dinamik zamanlama ve özyinelemeli çağrı özelliklerini atlamaktadır; bu özellikler diğer akıllı sözleşme dillerinde yüksek maliyetli 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 işlem tanımından oluşur. Modül, diğer modüllerde tanımlanan tür tanımlarını içe aktarabilir ve işlemleri çağırabilir.

2. Yapı: Kaynak türü olarak tanımlanabilir, kalıcı küresel anahtar/değer deposunda saklanabilenleri ifade eder.

3. Süreç: Modülün işlevselliğini ve mantığını tanımlamak.

4. Küresel Depolama: Move programının kalıcı verileri depolamasına izin verir, bu veriler yalnızca onu sahip olan modül tarafından programlı olarak okunup yazılabilir.

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

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

Bu güvenlik özellikleri sayesinde, Move akıllı sözleşmeler geliştirme için daha güvenli ve güvenilir bir programlama ortamı sunmaktadır.

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

Move programı sanal makinede çalışır, çalışırken sistem belleğine erişemez, bu da Move'un güvensiz ortamlarda güvenli bir şekilde çalışmasını sağlar.

Move programı yığın üzerinde çalışır, global depolama iki kısma ayrılır: bellek ( yığın ) ve global değişkenler ( yığın ). Bellek birinci dereceden depolamadır, bellek hücrelerine işaret eden işaretçileri depolayamaz. Global değişkenler bellek hücrelerine işaret eden işaretçileri depolamak için kullanılır, ancak dizinleme yöntemi bellekten farklıdır.

Move'un bytecode talimatları, yığın tabanlı yorumlayıcıda yürütülmektedir. Register tabanlı yorumlayıcıya kıyasla, yığın tabanlı yorumlayıcı, değişkenler arasındaki kopyalama ve taşıma işlemlerini kontrol etmek ve tespit etmek için daha kolaydır.

Move programının çalışma durumu ⟨C, M, G, S⟩ dörtlü kümesini içerir, bunlar çağrı yığını (C), bellek (M), global değişkenler (G) ve işletim sayısı (S)'dir. Yığın ayrıca fonksiyon gövdesini içeren talimatları çözmek için bir fonksiyon tablosunu da tutar.

MoveVM, verileri depolama ve çağrı yığınını ( işlem mantığı ) depolamadan ayırır, bu EVM ile ana farktır. Kullanıcı durumu ( hesap adresindeki kaynaklar ) bağımsız olarak depolanır, program çağrıları yetki ve kaynaklarla ilgili zorunlu kurallara uymalıdır. Bu tasarım, belirli bir esneklikten feragat etse de, güvenlik ve yürütme verimliliği açısından önemli bir artış sağlamıştır.

3. Move Prover

Move Prover, program davranışını tanımlamak için biçimsel bir dil kullanan ve programın beklentilere uyup uymadığını doğrulamak için akıl yürütme algoritmaları kullanan bir akıllı sözleşmeler doğrulama aracıdır. Geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına ve işlem risklerini azaltmalarına yardımcı olabilir.

Move Prover, bilinen bilgilere dayanarak program davranışını çıkarım yapmak için tümevarım doğrulama algoritmasını kullanır ve bunun beklenen davranışla eşleşmesini sağlar. Bu, program doğruluğunu garanti etmeye yardımcı olur ve manuel test yükünü azaltır.

Move Prover'ın çalışma akışı aşağıdaki gibidir:

1. Program girdi spesifikasyonlarını içeren Move kaynak dosyasını girdi olarak al.

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

3. Move derleyicisi kaynak dosyayı bayt koduna derler, standart sistemle birlikte doğrulayıcı nesne modeline dönüştür.

4. Nesne modeli Boogie ara diline çevrildi.

5. Boogie doğrulama sistemi giriş için "doğrulama koşulu oluşturma" gerçekleştirir.

6. Doğrulama koşulları Z3 çözücüsüne ( Microsoft tarafından geliştirilen SMT çözücüsüne ).

7. Z3, SMT formülünün karşılanamaz olup olmadığını kontrol eder. Eğer öyleyse, bu durum standardın geçerli olduğunu gösterir; aksi takdirde, koşulları karşılayan bir model oluşturur.

8. Tanı raporunu kaynak kodu düzeyindeki hatalara geri döndür.

Move, Move Specification Language kullanarak sistemin spesifikasyonunu tanımlar, bu Move dilinin bir alt kümesidir ve programın doğruluk davranışını statik olarak tanımlamayı destekler, üretimi etkilemez. Spesifikasyonlar bağımsız olarak yazılabilir, iş kodu ile formel doğrulama kodunun ayrılmasını kolaylaştırır.

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamak, işlem risklerini azaltmak ve akıllı sözleşmeleri üretim ortamına dağıtma konusunda güveni artırmak için yardımcı olan güçlü bir araçtır.

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ı düzeyinde kapsamlı bir şekilde ele alınmıştır. Dil özellikleri, derleme kontrolü ve biçimsel doğrulamanın otomasyonu ve doğrulanabilirliği için yararlı olan zorunlu tür kontrolü ve doğrusal mantık gibi bir miktar esnekliği feda etmiştir. MoveVM tasarımı, durumu mantıktan ayırır ve bu, blok zinciri varlıklarının güvenli yönetim ihtiyaçlarına daha uygundur.

Dil düzeyinde, Move EVM'nin yaygın re-entrant, taşma, Call/DeleGateCall enjekte etme gibi açıklarını etkili bir şekilde önleyebilir. Ancak, kimlik doğrulama, kod mantığı, büyük sayı yapıları taşması gibi sorunlar hala geliştiricilerin dikkatli bir şekilde ele almasına ihtiyaç duymaktadır. Move Prover güçlüdür, ancak genel tasarım ihmal edildiğinde etkili olamayabilir.

Move dilinin programcılara çoklu güvenlik önlemleri sağladığına rağmen, tamamen güvenli bir dil ve program yoktur. Move akıllı sözleşme geliştiricilerine, üçüncü taraf güvenlik şirketlerinin denetim hizmetlerini kullanmaları ve specification bölümündeki kodun yazımı ve doğrulamasını profesyonel güvenlik ekiplerine bırakmaları önerilir, böylece sözleşme güvenliğini daha da artırabilirler.