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

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

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

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

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

تقوم مدققات بايت كود بإجراء ثلاثة أنواع من الفحوصات:

1. فحص صلاحية الهيكل
2. الكشف الدلالي لمنطق العملية
3. كشف الأخطاء عند الاتصال

من خلال هذه الآليات، يمكن لـ Move ضمان مستوى عالٍ من الأمان أثناء وقت الترجمة.

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

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

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

3. نقل المدقق

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

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

تُستخدم لغة مواصفات Move لوصف أنظمة المواصفات، وهي مجموعة فرعية من لغة Move.

بشكل عام، يعد Move Prover أداة أمان قوية، ولكن لا يمكن أن تحل محل التدقيق اليدوي تمامًا. يُنصح المطورون بمواصلة استخدام خدمات التدقيق الأمني من طرف ثالث، وترك جزء المواصفات لشركة الأمان لإكماله.