تحليل أمان لغة Move: مُحدثة الجيل الجديد من لغات العقود الذكية

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

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

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

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

• وحدة (Module): تتكون من سلسلة من أنواع الهياكل وتعريفات العمليات
• الهياكل ( Structs ): يمكن تعريفها كنوع من الموارد، تُخزن في تخزين المفتاح/القيمة العالمي الدائم.
• 过程(function): تعريف الوظائف المحددة للعقود الذكية

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

تضمن لغة Move أمان الكود أثناء وقت الترجمة من خلال آليتين: فحص الثوابت وموثق بايت الكود:

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

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

تعمل برامج Move في بيئة افتراضية، ولا يمكن الوصول إلى ذاكرة النظام أثناء التشغيل، مما يضمن التشغيل الآمن في بيئات غير موثوقة.

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

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

3. نقل المُثبت

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

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

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

ملخص

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