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

المقدمة

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

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

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

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

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

1. نموذج (Module): يتكون كل نموذج Move من مجموعة من أنواع الهيكل والتعريفات العملية. يمكن للنموذج استيراد تعريفات الأنواع المعلنة في نماذج أخرى واستدعاء عملياتها.

2. 结构体(Structs): يمكن تعريفها كنوع من الموارد، مما يعني أنها يمكن أن تُخزن في تخزين المفتاح/القيمة العالمي الدائم.

3. العملية ( الوظيفة ): تحديد الوظائف المحددة للوحدة.

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

5. فحص الثوابت: يمكن تعريف الثوابت لفحص ثابت لضمان تكامل الموارد في النظام.

6. مدقق بايت كود: للتحقق من الأنواع الآمنة والتمخطط، لمنع إنشاء أو تعديل أو تدمير القيم الحساسة بشكل غير قانوني.

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

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

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

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

على عكس EVM، يفصل MoveVM بين تخزين البيانات و stack الاستدعاء، مما يجعله أكثر ملاءمة لاحتياجات إدارة أمان الأصول على blockchain. هذا التصميم يحقق تحسينًا كبيرًا في الأمان وكفاءة التنفيذ.

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

3. نقل المبرهن

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

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

تتمثل عملية عمل Move Prover في ما يلي:

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

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

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

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

4. ملخص

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

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

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