تحليل أمان لغة Move: مغير قواعد اللعبة في مجال العقود الذكية

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

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

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

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

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

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

من خلال هذه الآليات، يمكن لـ Move ضمان أمان عالي للكود في وقت الترجمة.

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

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

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

هذا التصميم حقق تحسينات كبيرة في الأمان وكفاءة التنفيذ.

3. نقل المدقق

Move Prover هو أداة تحقق رسمية قائمة على الاستدلال يمكنها:

• استخدام لغة رسمية لوصف سلوك البرنامج
• التحقق من صحة البرنامج من خلال خوارزميات الاستدلال
• اعتماد خوارزمية التحقق الاستنتاجي
• استخدم لغة Move لوصف معايير التحقق
• إنشاء تقرير التحقق، يشير إلى المشكلات المحتملة

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

ملخص

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

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