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

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

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

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

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

مدقق البايت كود يقوم بشكل أساسي بـ:

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

من خلال هذه الآليات، يمكن للغة Move ضمان أمان الشيفرة أثناء عملية التجميع.

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

تعمل برنامج Move في آلة افتراضية، وتشمل الخصائص الرئيسية ما يلي:

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

3. نقل موفر

Move Prover هي أداة للتحقق الرسمي، يمكنها إجراء تدقيق تلقائي:

• استخدام خوارزمية التحقق الاستنتاجي للتحقق من صحة البرنامج
• استلام ملفات Move والمواصفات كمدخلات
• تحويل الشيفرة إلى لغة Boogie الوسيطة
• استخدام زحل Z3 SMT للتحقق من صحة المواصفات
• دعم مواصفات لغة Move
• يمكن كتابة وثائق المعايير بشكل مستقل، دون التأثير على كود الأعمال

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

الملخص

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