Move dilinin güvenlik analizi

Move dili, yeni nesil bir akıllı sözleşme dili olarak, tasarımının başında blok zinciri ve akıllı sözleşmelerin güvenliği sorunlarını göz önünde bulundurmuştur. Bu makalede, Move dilinin güvenliğini dil özellikleri, çalışma mekanizması ve doğrulama araçları açısından inceleyeceğiz.

1. Move dilinin güvenlik özellikleri

Move dili, esneklik temelli doğrusal mantığı terk etti, dinamik dağıtımı ve dış çağrıları desteklemiyor, bunun yerine alternatif programlama modellerini gerçekleştirmek için genel türler, global depolama, kaynaklar gibi kavramları kullanıyor. Bu tasarımlar, yeniden giriş gibi güvenlik açıklarının önlenmesine yardımcı olur.

Move dilinin ana bileşenleri şunlardır:

• Modül: Yapı türleri ve işlem tanımlarından oluşur, diğer modüllerin tür tanımlarını içe aktarabilir ve diğer modüllerin işlemlerini çağırabilir.

• Yapı: Kaynak türü olarak tanımlanabilir, küresel anahtar-değer deposunda saklanır.

• Süreç: Modülün işlevini tanımlama, başlatma, güvenli ve güvensiz süreçleri içerebilir.

Move dilinin küresel depolama mekanizması, modüllerin kalıcı verileri depolamasına ve beyan ettikleri kaynak türleri üzerinde özel okuma/yazma erişim hakkına sahip olmasına izin verir. Bu mekanizma, güvenlik kısıtlamalarının uygulanmasına yardımcı olur.

Move dilinin iki önemli statik kontrol özelliği:

1. Değişmezlik Kontrolü: Sistem durumunun korunumu, düzenleme dili ile tanımlanır.

2. Bayt kodu doğrulayıcı: güvenli türlerin ve lineerleştirmenin zorunlu uygulanması, yasadışı işlemleri önlemek için.

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

Move programı sanal makinede çalışır, sistem belleğine doğrudan erişemez. Program yürütmesi yığın tabanlıdır, global depolama bellek ( yığını ) ve global değişken ( yığını ) olarak ikiye ayrılır.

Move VM yürütme durumu, çağrı yığını, bellek, küresel değişkenler ve işlem dizisi ile oluşur. Özellikleri şunlardır:

• Statik yönlendirme, dinamik dağıtımın önlenmesi
• Çağrı yığını komşu, yeniden girişi önlemek
• Veri depolama ve çağırma yığınları ayrıdır

Bu tasarım, güvenliği ve uygulama verimliliğini artırmaktadır.

3. Hareket Prover

Move Prover, programların beklenen sonuçlara uygun olup olmadığını doğrulamak için tümevarımsal doğrulama algoritması kullanan bir biçimsel doğrulama aracıdır. İş akışı:

1. Move kaynak dosyalarını ve standartlarını alma
2. Bytecode ve doğrulayıcı nesne modeline derleme
3. Boogie orta diline dönüştür
4. Doğrulama Koşullarını Oluşturma
5. Z3 çözücüsü ile doğrulama
6. Tanı raporu oluşturma

Move Specification Language, iş kodundan bağımsız olarak program davranış kurallarını tanımlamak için kullanılır.

Özet

Move dili, dil özellikleri, sanal makine yürütmesi ve güvenlik araçları açısından kapsamlı bir değerlendirme yapmıştır, birçok yaygın açığı etkili bir şekilde önleyebilir. Ancak, üçüncü taraf güvenlik denetim hizmetlerinin kullanılmasını ve güvenlik şirketleri tarafından standart kod yazım ve doğrulamasının yapılmasını öneririz.