تحليل أمان لغة Move

تعتبر لغة Move كلغة عقود ذكية من الجيل الجديد، حيث تم أخذ مسألة الأمان بعين الاعتبار في التصميم. ستقوم هذه المقالة بتحليل أمان لغة Move من ثلاثة جوانب: خصائص اللغة، آلية التشغيل، وأدوات التحقق.

1. ميزات الأمان في لغة Move

تمتلك لغة Move تصميم أمان على النحو التالي:

• التخلي عن منطق غير الخطي مثل التخصيص الديناميكي واستدعاءات خارجية متكررة، وتجنب ثغرات مثل إعادة الإدخال.
• استخدام نوع الموارد وآلية التخزين العالمية لتحقيق إدارة أمان الأصول
• من خلال تقليل المتغيرات الثابتة ومحقق بايت الكود ، يتم تحقيق التحقق المزدوج للسلامة في وقت الترجمة

إليك مثال بسيط على كود Move:

تحرك الوحدة 0x1::TestCoin { استخدم 0x1::signer;

هيكل Coin يحتوي على مفتاح { 
    القيمة: u64 
}

هيكل المعلومات يحتوي على مفتاح {
    إجمالي العرض: u64
}

const ADMIN: العنوان = @0x1;

// الثوابت لفحص السكون
وحدة المواصفات {
    غير متغير لجميع العناوين: عنوان حيث يوجد<coin>(addr):
        (ADMIN).total_supply > العالمية<info>= العالمية<coin>(addr).value;
}

initialize(account المرح العام: &signer) {
    assert!(signer::address_of(account) == ADMIN, 0);
    نقل إلى ( الحساب، معلومات { إجمالي العرض: 0 } );
}

mint(account المرح العام: & الموقع, المبلغ: u64): عملة {
    assert!(signer::address_of(account) == ADMIN, 0);
    دع المعلومات = borrow_global_mut<info>(ADMIN) ؛
    info.total_supply = info.total_supply + المبلغ ؛
    عملة { القيمة: المبلغ }
}

value_mut(coin المرح العام: & Coin): &MUT U64 {
    &MUT coin.value  
}

}

تقوم Move بتحقيق إدارة أمان الأصول من خلال التخزين العالمي وأنواع الموارد. تمتلك الوحدة حق الوصول الحصري إلى أنواع الموارد التي أعلنت عنها، ويمكنها فرض القيود على إنشاء الموارد وعملياتها.

تقدم تقنيات اختصار الثوابت ومحقق الشيفرات الثنائية فحصين أمان مزدوجين في وقت الترجمة، مما يضمن سلامة الشيفرة وأمان النوع.

2. آلية تشغيل Move

تعمل برامج Move في بيئة افتراضية ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. تتكون حالتها من مكدس الاستدعاء والذاكرة والمتغيرات العالمية ومصفوفات العمليات.

يعمل MoveVM على فصل تخزين البيانات وذاكرة الاستدعاء، مما يساعد على تحسين الأمان وكفاءة التنفيذ:

• حالة المستخدم ( الموارد ) مخزنة بشكل مستقل تحت عنوان الحساب
• يجب أن تتوافق استدعاءات البرنامج مع قواعد الأذونات والموارد
• مكدس استدعاء العملية متجاور، مما يتجنب إعادة الدخول

يتماشى هذا التصميم بشكل أفضل مع احتياجات إدارة أمان الأصول في blockchain.

3. نقل المدقق

Move Prover هو أداة تحقق رسمية، يمكنها أتمتة فحص صحة العقود الذكية. هيكلها كما يلي:

1. استلام ملف Move المصدر والمواصفات كمدخلات
2. تحويل الشيفرة المصدرية إلى بايت كود
3. تحويل إلى نموذج كائن المدقق
4. ترجمة إلى لغة Boogie الوسطى
5. إنشاء شروط التحقق
6. استخدام محلل Z3 للتحقق
7. إنشاء تقرير تشخيصي

تستخدم Move Prover لغة مواصفات Move لوصف مواصفات البرنامج ، ويمكن أن تكون مستقلة عن كود العمل. وهذا يوفر سهولة في التدقيق الأمني من قبل الأطراف الثالثة.

ملخص

تم تصميم لغة Move بشكل شامل من حيث ميزات اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. يمكنها تجنب الثغرات الشائعة مثل إعادة الدخول، والتجاوز بشكل فعال، ولكن لا يزال من الضروري الانتباه إلى التحكم في الأذونات، والأخطاء المنطقية، وغيرها من المشاكل.

نوصي مطوري العقود الذكية Move:

• استخدام خدمات تدقيق الشركات الأمنية التابعة لطرف ثالث
• يتم تكليف شركة الأمن بكتابة وتحقق التعليمات البرمجية وفقًا للمعايير

لا توجد لغات وبرامج آمنة بشكل مطلق، يجب على المطورين أن يظلوا يقظين واتخاذ تدابير أمان شاملة.