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

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

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

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

تشمل المكونات الرئيسية للغة Move:

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

• الهيكل: يمكن تعريفه على أنه نوع من الموارد، مخزنة في تخزين القيم المفتاحية العالمية.

• العملية: تحديد وظيفة الوحدة، ويمكن أن تشمل عمليات التهيئة والأمان وغير الآمنة.

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

الخصائص الهامة لفحص السكون في لغة Move:

1. فحص الثوابت: تعريف استمرارية حالة النظام من خلال لغة القواعد.

2. مفسر البايت كود: تنفيذ الأمان النوعي والخطوط العريضة، لمنع العمليات غير القانونية.

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

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

تتكون حالة تنفيذ VM من مكدس الاستدعاء، والذاكرة، والمتغيرات العالمية، ومصفوفة العمليات. تشمل ميزاتها:

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

هذا التصميم يعزز الأمان وكفاءة التنفيذ.

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

3. نقل المدعي

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

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

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

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

ملخص

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

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