Move dilinin güvenlik analizi

Ön söz

Move, MoveVM'yi gerçekleştiren blockchain ortamında çalışan bir akıllı sözleşme dilidir. Doğduğu günden itibaren blockchain ve akıllı sözleşmelerin birçok güvenlik sorununu göz önünde bulundurmuş 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 olan Move'un güvenliği 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? Kendisi özel bir güvenlik riski 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

Mevcut birçok programlama dilinden farklı olarak, Move hem güvenilmeyen kodlarla güvenli etkileşimi desteklemek hem de statik doğrulamayı sağlamak için tasarlanmıştır. Move'un bu güvenlik özelliklerine sahip olmasının nedeni, esneklik düşüncesine dayalı olan doğrusal olmayan mantığı terk etmesi, dinamik dağıtımı desteklememesi ve dışarıdan çağrılara geri dönüşü desteklememesidir; bunun yerine, alternatif programlama modellerini gerçekleştirmek için generikler, küresel depolama, kaynaklar gibi kavramları kullanmaktadır. Örneğin, Move, yeniden giriş açıklarına neden olabilecek dinamik zamanlama ve geri çağırma özelliklerini atlamaktadır.

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

1. Modül(Module): Her Move modülü bir dizi yapı tipi ve işlem tanımından oluşur. Modüller, diğer modüller tarafından tanımlanan tip tanımlarını içe aktarabilir ve bunların işlemlerini çağırabilir.

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

3. süreç ( işlev ): Modülün belirli işlevini tanımlama.

4. Global 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 okunabilir ve yazılabilir.

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

6. Bytecode doğrulayıcı: güvenlik türlerini ve lineerleştirmeyi doğrular, hassas değerlerin yasadışı bir şekilde oluşturulmasını, değiştirilmesini veya yok edilmesini önler.

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

Move programı sanal makinede çalışıyor, sistem belleğine doğrudan erişim yok. Program yığın üzerinde çalışıyor, global depolama iki kısma ayrılıyor: bellek ( yığını ) ve global değişkenler ( yığın ).

Move'nin byte kodu talimatları yığın tabanlı bir yorumlayıcıda çalıştırılır, bu yöntem uygulanması ve kontrol edilmesi kolaydır, donanım gereksinimleri düşüktür ve blok zinciri senaryolarına uygundur. Aynı zamanda kayıt 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.

İşlem sırasında, Move programının durumu çağrı yığını, bellek, küresel değişkenler ve işlemlerden oluşur. Çağrı yığını, süreç yürütmesinin tüm bağlam bilgilerini içerir. Call talimatı yürütüldüğünde yeni bir çağrı yığını nesnesi oluşturulur. Dal talimatı ile karşılaşıldığında, süreç içinde statik atlama yapılır.

EVM'den farklı olarak, MoveVM veri depolama ve çağrı yığınını ayırır, bu da blockchain üzerindeki varlık güvenliği yönetimi ihtiyaçları için daha uygundur. Bu tasarım, güvenlik ve yürütme verimliliğinde büyük bir iyileşme sağlar.

3. Move Prover

Move Prover, program davranışını tanımlamak için formel dil kullanan ve programın beklenenle uyumlu olup olmadığını doğrulamak için akıl yürütme algoritmaları kullanan akıl yürütme tabanlı bir formel 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ı çıkarsamak için bir akıl yürütme doğrulama algoritması kullanır ve bunun beklenen davranışla 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 iş akışı aşağıdaki gibidir:

1. Move kaynak dosyasını girdi olarak al
2. Çıkarma standartlarını belirleyin ve byte koduna derleyin
3. Doğrulayıcı nesne modeline dönüştür
4. Boogie ara diline çevir
5. Doğrulama koşullarını oluştur
6. Z3 çözücüsünü kullanarak SMT formülünü doğrulama
7. Tanı raporu oluşturun ve kaynak kodu seviyesindeki hatalara geri döndürün

Move Spesifikasyon Dili, standart sistemleri tanımlamak için kullanılır ve Move dilinin bir alt kümesidir, programın doğruluk davranışını statik olarak tanımlamayı destekler.

Genel olarak, Move Prover, geliştiricilerin akıllı sözleşmelerin doğruluğunu sağlamalarına, işlem risklerini azaltmalarına ve akıllı sözleşmeleri dağıtmada güvenlerini artırmalarına yardımcı olabilen çok kullanışlı bir araçtır.

4. Özet

Move dili, güvenlik tasarımı açısından son derece başarılıdır ve dil özellikleri, sanal makine yürütmesi ve güvenlik araçları düzeyinde kapsamlı bir şekilde değerlendirilmiştir. Bazı esnekliklerden feragat ederek, derleme kontrolü ve biçimsel doğrulama için zorunlu tür kontrolü ve lineer mantık sağlamaktadır. MoveVM, durum ile mantığı ayırarak, blok zinciri varlıklarının güvenli yönetim ihtiyaçlarına daha uygun hale gelir.

Move dili, EVM'de yaygın olan yeniden giriş, taşma, Call/DeleGateCall enjeksiyonu gibi açıkları etkili bir şekilde önleyebilir. Ancak kimlik doğrulama, kod mantığı, büyük tam sayı yapısı taşması gibi sorunlar geliştiricilerin ekstra dikkat etmesini gerektirir. Move Prover biçimsel doğrulama sağlasa da, genel tasarımda bulunan eksiklikleri gideremez.

Move güvenlik açısından birçok düşünce yapmış olsa da, tamamen güvenli bir dil ve program yoktur. Move akıllı sözleşme geliştiricilerinin yine de üçüncü taraf güvenlik şirketlerinin denetim hizmetlerini kullanmaları ve standartların yazımı ve doğrulanmasını profesyonel güvenlik ekiplerine bırakmaları önerilir.