Move dilinin güvenlik analizi

Ön Söz

Move, MoveVM'yi gerçekleştiren blok zinciri ortamında derlenip çalıştırılabilen bir 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ştur ve RUST dilinin bazı güvenlik tasarım ilkelerinden faydalanmıştır. Güvenlik ana özellik olarak öne çıkan yeni nesil bir akıllı sözleşme dili olan Move'un güvenliği gerçekten nasıldır? Dil düzeyinde veya ilgili mekanizmalarla EVM, WASM gibi sözleşme sanal makinelerinin yaygın güvenlik tehditlerinden kaçınabilir mi? Move'un kendisine özgü güvenlik sorunları var mı?

Bu makale, Move dilinin güvenliği sorununu dil özellikleri, çalışma mekanizması ve doğrulama araçları üç açıdan ele alacaktır.

1. Move dilinin güvenlik özellikleri

Hatasız kod yazmak zordur, birçok testten geçse bile tamamen garanti edilemez. Güvensiz kodlarla etkileşimde bulunurken, kritik güvenlik niteliklerini koruyan kod yazmak daha da zorlayıcıdır. Güvenliği çalışma zamanında zorunlu kılacak çeşitli teknikler vardır; örneğin, kum havuzları, süreç izolasyonu, nesne kilitleme gibi programlama modelleri; ayrıca, derleme zamanında statik güvenliği belirlemek için güçlü statik türler veya ifade kontrolü gibi yöntemler de kullanılabilir.

Bazen, kodun güvenlik kurallarına uygunluğunu sağlamak için anlam analizi ve statik analiz araçlarından yararlanmak mümkündür; bu sayede, güvenilmez kodlarla etkileşimde bulunulsa bile belirli kanıtlanabilir mantıksal kısıtlamalar korunabilir. Bu yöntemler iyi görünse de, çalışma zamanı maliyetlerini önleyebilir ve güvenlik sorunlarını erken tespit edebilir. Ancak, programlama dilleri bu yöntemlerle sağlanan güvenlik açısından son derece sınırlıdır, bunun iki ana nedeni vardır: Öncelikle, genellikle statik analiz araçlarıyla analiz edilmesi zor olan dil özelliklerine sahip olmalarıdır; dinamik dağıtım, paylaşılan değişkenlik ve yansıma gibi doğrusal olmayan mantık özellikleri, güvenlik invariat kurallarını ihlal ederek saldırganlara geniş bir saldırı yüzeyi sunmaktadır. İkincisi, çoğu programlama dili, güvenlikle ilgili statik araçları veya güçlü bir şekilde ifade edilebilen kısıtlı dilleri destekleyecek şekilde genişletilmesi zordur; bu iki genişletme de oldukça önemlidir.

Move dilinin tasarımı, güvensiz kodlarla güvenli etkileşim sağlamanın yanı sıra, statik doğrulamayı da destekler. Bu güvenlik özelliklerine sahip olmasının nedeni, esneklik dikkate alınarak oluşturulan tüm lineer olmayan mantıkları terk etmesi, dinamik dağıtımı desteklememesi ve dış çağrılarda özyinelemeyi desteklememesidir. Bunun yerine, bazı alternatif programlama modellerini gerçekleştirmek için genel türler, küresel depolama, kaynaklar gibi kavramları kullanır. Örneğin, Move dinamik yönlendirme ve özyinelemeli çağrı ö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 dilinin ana güvenlik özellikleri şunlardır:

• Modüler: Her Move modülü bir dizi yapı tipi ve işlem tanımından oluşur. Modüller, diğer modüllerde tanımlanan tür tanımlarını içe aktarabilir ve işlemleri çağırabilir.

• Yapı: Global anahtar/değer depolama alanında saklanabilen verileri temsil etmek için kaynak türlerini tanımlayan bir yapı.

• Süreç: Başlatma, güvenli ve güvensiz süreçleri tanımlar. Süreçlerin erişim kontrol kısıtlamaları olabilir.

• Küresel Depolama: Kalıcı verilerin saklanmasına izin verir, yalnızca onu sahip olan modül tarafından programlı olarak okunabilir ve yazılabilir.

• Değişmez kontrolü: Sistem içindeki kaynakların bütünlüğünü sağlamak için statik kontrol değişmezleri tanımlanabilir.

• Bayt kodu doğrulayıcı: Bayt kodu düzeyinde tür sistemini zorlar, kaynakların uygunsuz bir şekilde oluşturulmasını, açılmasını veya referans verilmesini engeller.

Bu özellikler, Move'un hem derleme zamanında hem de çalışma zamanında güçlü güvenlik garantileri sunmasını sağlar.

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

Move programı sanal makine üzerinde çalışır, bu da sistem belleğine doğrudan erişimi engeller, bu da güvenilmeyen ortamlarda güvenli bir şekilde çalışmasını sağlar.

Move, yığın tabanlı bir yürütme modeli kullanır. Küresel depolama, bellek ( yığın ) ve küresel değişken ( yığın ) olmak üzere iki bölümden oluşur. Bellek birinci düzey 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 ve adres ve tür aracılığıyla erişilir.

Move, bytecode talimatlarını yığın tabanlı bir yorumlayıcı ile yürütür. Bu yöntem uygulaması ve kontrol edilmesi kolaydır, donanım gereksinimleri düşüktür ve blok zinciri senaryoları için uygundur. Kayıt tabanlı yorumlayıcılara kıyasla, yığın tabanlı yorumlayıcılar değişkenler arasındaki kopyalama ve taşıma işlemlerini kontrol etmek ve tespit etmek daha kolaydır.

Move programının çalışma durumu bir dörtlü ⟨C, M, G, S⟩'dir; bu, çağrı yığını (C), bellek (M), küresel değişkenler (G) ve operand yığını (S)'yi içerir. Çağrı yığını, işlem sürecinin bağlam bilgilerini ve talimat numarasını içerir. Call talimatı yürütüldüğünde, parametreleri depolayan ve yeni sözleşmenin talimatlarını yürüten yeni bir çağrı yığını nesnesi oluşturulur. Dal talimatıyla karşılaştığında, süreç içinde statik atlama yapılır.

MoveVM, veri depolaması ve çağrı yığınını ayırır, bu da onu EVM'den ayıran ana farktır. Move'da, kullanıcı durumu ( hesap adresi altındaki kaynak ) bağımsız olarak depolanır, program çağrıları izin ve kaynak kurallarına uymalıdır. Bu tasarım, belirli bir esneklikten feragat eder, ancak güvenliği ve yürütme verimliliğini artırır.

3. Move Prover

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamasına ve işlem risklerini azaltmasına yardımcı olan, çıkarıma dayalı bir biçimsel doğrulama aracıdır. Program davranışını biçimsel bir dille tanımlar ve çıkarım algoritmaları aracılığıyla programın beklentilere uygun olup olmadığını doğrular.

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

Move Prover'ın çalışma süreci aşağıdaki gibidir:

1. Program spesifikasyonunu içeren Move kaynak dosyasını girdi olarak al.
2. Ayrıştırıcı standartları çıkarır, derleyici kaynak kodunu bayt koduna derler.
3. Doğrulayıcı nesne modeli oluşturma
4. Modeli Boogie ara diline çevir
5. Boogie doğrulama sistemi doğrulama koşulları oluşturur.
6. Doğrulama koşullarını Z3 çözücüsüne iletin.
7. Tanı raporu oluşturun ve kaynak kodu düzeyinde hataya dönüştürün

Move, programın doğru davranışını statik olarak tanımlayan Move dilinin bir alt kümesi olan Move Specification Language'ı sağlar. Spesifikasyon, iş kodundan bağımsız olarak yazılabilir.

Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına ve işlem risklerini azaltmalarına yardımcı olan güçlü bir araçtır. Beklentilere uygunluğunu doğrulamak için biçimsel yöntemler kullanarak, geliştiricilerin akıllı sözleşmeleri dağıtma konusundaki güvenini artırır.

Özet

Move dili, güvenlik açısından kapsamlı bir şekilde ele alınmıştır; dil özelliklerinden sanal makine yürütmesine ve güvenlik araçlarına kadar güçlü bir koruma sağlamaktadır. Belirli bir esneklikten feragat edilmiştir; zorunlu tür kontrolü ve lineer mantık, derleme denetimi ve biçimsel doğrulamanın otomatikleştirilmesine yardımcı olmaktadır. MoveVM'nin tasarımı, durumu mantıktan ayırarak, blockchain varlık güvenliği yönetimi ihtiyaçlarına daha uygun hale gelmektedir.

Move dili, EVM'de sıkça karşılaşılan reentrancy, taşma, Call/DelegateCall enjeksiyonları gibi açıkları etkili bir şekilde önleyebilir. Ancak, yetkilendirme, kod mantığı, büyük tam sayı yapısı taşmaları gibi sorunlar geliştiricilerin ekstra dikkat etmesi gereken konulardır. Move Prover güçlüdür, ancak genel tasarımda dikkatsizlikleri tamamen önleyemez.

Move, güvenlik açısından birçok düşünce geliştirmiş olsa da, tamamen güvenli bir dil ve program yoktur. Move akıllı sözleşme geliştiricilerine, üçüncü taraf güvenlik şirketlerinin denetim hizmetlerini kullanmalarını ve standartların yazım ve doğrulama kısmını profesyonel güvenlik ekiplerine bırakmalarını öneririz.