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

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

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

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

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

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

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

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

3. 过程(Function): تعريف منطق سلوك الوحدة.

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

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

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

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

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

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

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

عند تشغيل برنامج Move، تكون حالته عبارة عن رباعي ⟨C، M، G، S⟩، والذي يتضمن: مكدس الاستدعاء (C)، الذاكرة (M)، المتغيرات العالمية (G) وعداد العمليات (S). كما يحتفظ المكدس بجدول الوظائف ( ووحدة البرنامج نفسها ) لتحليل التعليمات التي تحتوي على جسم الوظيفة.

تفصل MoveVM بين تخزين البيانات ومنطق العمليات في مكدس الاستدعاء (، وهو أكبر اختلاف عن EVM. في MoveVM، يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ) بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع القواعد الإلزامية المتعلقة بالأذونات والموارد. على الرغم من أن هذا sacrifice بعض المرونة، إلا أنه يساعد في تحقيق تحسين كبير في الأمان وكفاءة التنفيذ (، مما يعزز التنفيذ المتوازي ).

3. نقل المدقق

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

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

تدفق عمل Move Prover هو كما يلي:

1. استلام ملف Move كمصدر للإدخال، يجب أن يكون هذا الملف مهيئًا وفقًا لمواصفات إدخال البرنامج (specification).

2. استخرج Parser من الشيفرة المصدرية.

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

4. تحويل النموذج إلى لغة Boogie الوسيطة.

5. نظام Boogie يتحقق من المدخلات من خلال "توليد شروط التحقق" (generation verification condition ).

6. تمرير شروط التحقق إلى محلل Z3 (، محلل SMT الذي طوّرته مايكروسوفت ).

7. Z3 يتحقق من ما إذا كانت كود البرنامج SMT الصيغة ( تلبي specification规范 ) غير قابلة للإرضاء.

8. إذا لم يتم الوفاء بها، فإن ذلك يشير إلى أن المعايير قد تم تأسيسها؛ وإلا، يتم إنشاء نموذج يلبي الشروط، وتحويله مرة أخرى إلى تنسيق Boogie لنشر تقرير التشخيص.

9. استعادة تقرير التشخيص إلى أخطاء على مستوى المصدر.

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

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

4. الملخص

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

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

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