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

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

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

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

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

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

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

2. الهيكل: يمكن تعريفه كنوع من الموارد، يمثل ما يمكن تخزينه في تخزين المفاتيح/القيم العالمي الدائم.

3. العملية: تحديد وظائف المنصة والمنطق.

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

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

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

من خلال هذه الميزات الأمنية، توفر Move بيئة برمجة أكثر أمانًا وموثوقية لتطوير العقود الذكية.

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

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

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

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

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

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

3. نقل المدقق

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

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

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

1. استلام ملف Move المصدر كمدخلات، والذي يتضمن مواصفات إدخال البرنامج.

2. استخراج المعايير من مصدر Parser.

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

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

5. يقوم نظام Boogie بالتحقق من "توليد شروط التحقق" للمدخلات.

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

7. Z3 يتحقق مما إذا كانت صيغة SMT غير قابلة للتلبية. إذا كان الأمر كذلك، فهذا يعني أن المعيار قائم؛ وإلا يتم إنشاء نموذج يلبي الشروط.

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

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

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

4. الملخص

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

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

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