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

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

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

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

تتضمن الميزات الأمنية الرئيسية لـ Move:

• وحدة (Module): تتكون من نوع الهيكل وتعريف العملية، ويمكن استيراد تعريفات النوع والعمليات من وحدات أخرى.

• (Structs): يمكن تعريفها كنوع من الموارد، وتخزينها في تخزين المفتاح/القيمة العالمي.

• العملية ( الوظيفة ): تعرف عملية التهيئة، العملية الآمنة والعملية غير الآمنة.

• التخزين العالمي: يسمح بتخزين البيانات الدائمة، ويمكن قراءتها وكتابتها برمجياً فقط من قبل الوحدة التي تمتلكها.

• فحص الثوابت: يمكن تعريف الثوابت لفحص استاتيكي، لضمان الحفاظ على حالة النظام.

• مدقق بايت كود: يفرض نظام النوع على مستوى بايت كود، لمنع العمليات غير القانونية.

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

تعمل برامج Move داخل آلة افتراضية ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. يتم تنفيذ البرامج على المكدس، ويقسم التخزين العالمي إلى قسمين: ذاكرة (، كومة ) ومتغيرات عالمية ( مكدس ).

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

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

![تحليل أمان Move: تغيير قواعد اللعبة في لغات العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. موفر الحركة

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

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

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

![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

4. الملخص

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

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

![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(