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

Move dili, MoveVM'i gerçekleştiren blok zinciri ortamlarında çalışabilen akıllı sözleşme dilidir. Tasarım aşamasında blok zinciri ve akıllı sözleşmelerin birçok güvenlik sorununu göz önünde bulundurmuş ve RUST dilinin güvenlik tasarımını referans almıştır. Güvenliği ana özelliklerinden biri olan yeni nesil bir akıllı sözleşme dili olarak, güvenliği nasıldır? Dil seviyesinde ya da ilgili mekanizmalarla EVM, WASM gibi sözleşme sanal makinelerinin sık karşılaşılan güvenlik tehditlerinden kaçınabilir mi? Kendisi özel güvenlik sorunları barındırıyor mu?

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

1. Move dilinin güvenlik özellikleri

Mevcut birçok programlama dilinden farklı olarak, Move dili hem güvensiz kodlarla güvenli etkileşim kuran programların yazılmasını desteklemek hem de statik doğrulamayı desteklemek için tasarlanmıştır. Move'un bu tür güvenlik özelliklerine sahip olmasının nedeni, esneklik düşüncesine dayanan doğrusal olmayan mantıktan vazgeçmesi, dinamik dağıtımı desteklememesi ve dış çağrılara yönelik özyinelemeyi desteklememesi, bunun yerine genel türler, global depolama, kaynaklar gibi kavramları kullanarak bazı alternatif programlama modellerini gerçekleştirmesidir. Örneğin, Move dinamik yönlendirme ve özyineleme çağrısı özelliklerini atlamıştır; bu özellikler diğer akıllı sözleşme dillerinde maliyetli yeniden giriş açıklarına yol açmaktadır.

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

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

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

3. süreç ( Function ): akıllı sözleşmelerin iş mantığını tanımlar.

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ı bir şekilde okunup yazılabilir.

5. Değişmezlik Kontrolü: Sistemdeki kaynakların korunumu anlamına gelen statik kontrol değişmezliklerini tanımlamak mümkündür.

6. Bytecode doğrulayıcı: Bytecode'un güvenlik türü ve lineerleştirme doğrulamasını yaparak, kaynakların oluşturulması, yok edilmesi ve erişim kurallarını zorlar.

Bu özellikler sayesinde, Move derleme zamanında yüksek bir güvenlik sağlamayı garanti edebilir. Sonraki aşamada, Move'un çalışma mekanizmasını analiz edeceğiz ve MoveVM'nin çalışma zamanında güvenliği nasıl sağladığını göreceğiz.

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

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

Move programı yığın üzerinde çalıştırılır. Küresel depolama, bellek ( yığın ) ve küresel değişkenler ( yığın ) olmak üzere iki parçaya ayrılır. Bellek birinci derece depolamadır ve 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 dizinleme yöntemi bellekten farklıdır.

Move'in bayt kodu talimatları yığın tabanlı yorumlayıcıda yürütülmektedir. Yığın tabanlı sanal makine uygulanması ve kontrol edilmesi kolaydır, donanım ortamı için düşük gereksinimlere sahiptir ve blok zinciri senaryolarına uygundur. Aynı zamanda, 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 izlenebilir.

Move programının çalışma durumu ⟨C, M, G, S⟩ dörtlü olarak, çağrı yığını (C), bellek (M), global değişkenler (G) ve işlemciler (S) ile oluşturulmaktadır. Yığın ayrıca fonksiyon gövdesini içeren talimatları çözümlemek için bir fonksiyon tablosu da tutar.

Çağrı yığını, süreç yürütmesinin tüm bağlam bilgilerini ve talimat numarasını içerir. Call talimatı yürütülürken yeni bir çağrı yığını nesnesi oluşturulur, çağrı parametreleri saklanır ve ardından yeni sözleşme talimatı yürütülür. Şube talimatlarıyla karşılaşıldığında süreç içinde statik atlama yapılır. Bu tasarım, dinamik dağıtımı önleyerek, işlev çağrısının değişmezliğini artırır ve böylece yeniden giriş olasılığını ortadan kaldırır.

MoveVM, veri depolama ve çağrı yığını ( işlem mantığı ) depolamasını ayırır, bu EVM ile en büyük farktır. MoveVM'de, kullanıcı durumu ( hesap adresi altındaki kaynaklar ) bağımsız olarak depolanır, program çağrıları yetki ve kaynakla ilgili zorunlu kurallara uymak zorundadır. Bu tasarım, belirli bir esnekliği feda etse de, güvenlik ve yürütme verimliliği açısından büyük bir iyileşme sağlamıştır.

3. Move Prover

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 beklenilenle uyumlu olup olmadığını doğrulamak için akıl yürütme algoritmaları kullanır, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına yardımcı olur ve böylece işlem riskini azaltır.

Move Prover, programın beklenen davranışa uyup uymadığını doğrulamak için çıkarımsal doğrulama algoritması kullanır. Bilinen bilgilere dayanarak programın davranışını çıkarabilir ve bunun beklenen davranışla eşleşmesini sağlar. Bu, programın doğruluğunu sağlamaya yardımcı olur ve manuel test iş yükünü azaltır.

Move Prover'ın iş akışı şu şekildedir:

1. Move kaynak dosyasını girdi olarak alın, bu dosyada program girdi standartlarının ayarlanması gerekmektedir.
2. Move Parser, kaynak kodundan standartları çıkarır.
3. Move derleyicisi kaynak dosyayı byte koduna çevirir ve bu, doğrulayıcı nesne modeline dönüştürülmek üzere standart sistemle birlikte çalışır.
4. Bu model Boogie ara diline çevrildi.
5. Boogie doğrulama sistemi girdi için "doğrulama koşulu oluşturma" yapar.
6. Doğrulama koşulları Z3 çözümleyicisine kontrol için iletilir.
7. Eğer standart geçerliyse, doğrulama başarılı; aksi takdirde bir teşhis raporu oluşturulur.

Standart sistemleri tanımlamak için Move, Move Specification Language'ı kullanır; bu, Move dilinin bir alt kümesidir ve statik program doğruluğu davranışlarını tanımlama desteği sunar. Move Specification Language, iş kodu ile biçimsel doğrulama kodunu ayırarak, bağımsız olarak özel bir kurallaştırma dosyası olarak kullanılabilir.

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına yardımcı olan çok faydalı bir araçtır. Program davranışını tanımlamak için formel bir dil kullanır ve programın beklenen sonuçlara uygun olup olmadığını doğrulamak için akıl yürütme algoritmaları kullanır. Bu, işlem risklerini azaltmaya yardımcı olur ve geliştiricilerin akıllı sözleşmeleri üretim ortamında daha güvenle dağıtmalarını sağlar.

4. Özet

Move dili güvenlik tasarımında oldukça başarılıdır, dil özellikleri, sanal makine yürütmesi ve güvenlik araçları açısından kapsamlı bir değerlendirme sunmaktadır. Dil özellikleri açısından bir miktar esneklikten ödün verilmiş, zorunlu tür kontrolü ve lineer mantık uygulanmış, bu da derleme kontrolü ve biçimsel doğrulama sırasında daha otomatik ve güvenli doğrulanabilirlik sağlamaktadır. MoveVM tasarımı, durumu ve mantığı birbirinden ayırarak, blok zincirindeki varlık güvenliği yönetimi ihtiyacına daha uygun hale getirilmiştir.

Dil seviyesinde, Move, EVM'de yaygın olan yeniden giriş, taşma, Call/DeleGateCall enjeksiyonu gibi güvenlik açıklarını etkili bir şekilde önleyebilir. Ancak, yetkilendirme, kod mantığı, büyük tam sayı yapısı taşması gibi sorunlar geliştiricilerin ek dikkatine ihtiyaç duyar. Move Prover güçlüdür, ancak genel anlamda dikkatsizlik olduğunda etkili olamayabilir.

Move dilinin güvenlik açısından programcılar için pek çok şeyi düşündüğü halde, 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ı üçüncü taraf güvenlik şirketine devretmeleri önerilir, böylece sözleşme güvenliği daha da artırılabilir.