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

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

1. الخصائص الأمنية للغة Move

تتميز لغة Move بالخصائص الأمنية الرئيسية التالية:

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

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

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

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

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

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

ثابت لكل عنوان: عنوان حيث توجد <coin>(addr):
    (ADMIN).total_supply > العالمية<info>= العالمية<coin>(addr).value;

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

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

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

}

تضمن Move أمان الشفرة من خلال تقليل المتغيرات الثابتة ومحقق بايت الكود:

1. متغير ثابت: يستخدم للتحقق من أن مجموع قيم جميع كائنات Coin في النظام يجب أن يساوي total_supply في Info.

2. مدقق بايت كود: تحقق من الأنواع الإلزامية والمنطق الخطي، لمنع إنشاء أو نسخ أو تدمير الموارد بشكل غير قانوني.

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

تعمل برامج Move في جهاز افتراضي ولها الميزات التالية:

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

تتكون حالة تشغيل برنامج Move من رباعية ⟨C، M، G، S⟩:

• C: مكدس الاستدعاءات
• م: الذاكرة ( كومة )
• G: المتغيرات العالمية ( مكدس )
• S:عامل

هذا التصميم يفصل بين حالة المستخدم ومنطق البرنامج، مما يزيد من الأمان وكفاءة التنفيذ المتزامن.

3. نقل الإثبات

Move Prover هو أداة للتحقق الرسمي تُستخدم لضمان صحة العقود الذكية. تتلخص خطوات عمله كما يلي:

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

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

ملخص

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