لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئات blockchain التي تنفذ MoveVM. تم تصميمها مع مراعاة العديد من قضايا الأمان المتعلقة بالبلوكشين والعقود الذكية، واستمدت بعض أفكار تصميم الأمان من لغة Rust. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة التي تواجهها الآلات الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو من خلال آليات ذات صلة؟ هل توجد مشاكل أمان فريدة خاصة بـ Move؟
ستتناول هذه المقالة قضية أمان لغة Move من ثلاثة جوانب: خصائص اللغة، وآلية التشغيل، وأدوات التحقق.
1. ميزات الأمان في لغة Move
على عكس العديد من لغات البرمجة الموجودة، تم تصميم لغة Move لدعم التفاعل الآمن مع التعليمات البرمجية غير الموثوقة، بالإضافة إلى دعم التحقق الثابت. تتخلى Move عن المنطق غير الخطي القائم على المرونة، ولا تدعم التوزيع الديناميكي أو الاستدعاءات الخارجية العودية، بل تستخدم مفاهيم مثل الجنريك، التخزين العالمي، والموارد لتحقيق نماذج برمجة بديلة. على سبيل المثال، تتجاوز Move الخصائص الديناميكية مثل الجدولة الديناميكية والاستدعاءات العودية التي قد تؤدي إلى ثغرات إعادة الدخول.
تشمل الخصائص الأمنية الرئيسية لـ Move:
الوحدة: تتكون كل وحدة Move من سلسلة من تعريفات الأنواع الهيكلية والإجراءات. يمكن للوحدة استيراد تعريفات الأنواع واستدعاء الإجراءات المعلنة في وحدات أخرى.
الهيكل: يمكن تعريفه كنوع من الموارد، ويشير إلى ما يمكن تخزينه في تخزين المفاتيح/القيم العالمي الدائم.
العملية: تعريف عملية التهيئة، وعملية الأمان، وعملية عدم الأمان.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، والتي يمكن قراءتها وكتابتها برمجياً فقط بواسطة الوحدة التي تمتلكها.
فحص الثوابت: يدعم فحص الثوابت الثابتة، لضمان سلامة الموارد في النظام.
مُحقق بايت كود: يُنفذ نظام النوع على مستوى بايت كود، لمنع العمليات غير القانونية لوحدات العميل الخبيثة.
من خلال آلية فحص الثوابت ومدقق بايت الكود، يحقق Move ضمانًا مزدوجًا لسلامة الكود في وقت الترجمة.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكن الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يجعل Move تعمل بأمان في بيئات غير موثوقة، دون أن تتعرض للتلف أو الإساءة.
تتم تنفيذ برنامج Move على المكدس، حيث يتم تقسيم التخزين العالمي إلى قسمين: الذاكرة ( المكدس ) والمتغيرات العالمية (. الذاكرة هي تخزين من الدرجة الأولى، حيث لا يمكن لوحداتها تخزين مؤشرات تشير إلى وحدات الذاكرة. يتم استخدام المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، ولكن طريقة الفهرسة تختلف عن الذاكرة.
تُنفذ تعليمات بايت كود Move في مفسر يعتمد على المكدس. من السهل تنفيذ الماكينة الافتراضية المكدسية والتحكم فيها، وتتطلب متطلبات أقل من البيئة المادية، مما يجعلها مناسبة لمشاهد blockchain. مقارنةً بالمفسر القائم على السجلات، يكون من الأسهل التحكم في عمليات النسخ والتحريك بين المتغيرات واكتشافها باستخدام المفسر القائم على المكدس.
تكون حالة تشغيل برنامج Move عبارة عن رباعي ⟨C، M، G، S⟩، والذي يتضمن مكدس الاستدعاء )C(، الذاكرة )M(، المتغيرات العالمية )G( وOperands )S(. كما يحتفظ المكدس بجدول الدوال لتحليل التعليمات التي تحتوي على جسم الدالة.
تقوم MoveVM بفصل البيانات المخزنة ومنطق العملية على مكدس الاستدعاء )، وهذا هو الاختلاف الأكبر مع EVM. في MoveVM، يتم تخزين الموارد ( تحت عنوان حساب حالة المستخدم ) بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع القواعد الإلزامية المتعلقة بالأذونات والموارد. هذه التصميم يضحي ببعض المرونة، لكنه يساعد في تحقيق تحسين كبير في الأمان وكفاءة التنفيذ ( من حيث التنفيذ المتزامن ).
3. نقل البروفر
Move Prover هي أداة للتحقق الرسمي تستند إلى الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات.
تستخدم Move Prover خوارزمية التحقق الاستنتاجي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. وهذا يعني أنه يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن التطابق مع السلوك المتوقع. يساعد ذلك في ضمان صحة البرنامج وتقليل عبء العمل اليدوي للاختبار.
تدفق العمل لـ Move Prover كما يلي:
استلام ملف Move كمصدر للإدخال، يجب إعداد هذا الملف وفقًا لمعايير إدخال البرنامج.
يقوم Parser باستخراج المعايير من الشيفرة المصدرية.
يقوم مترجم Move بتحويل ملفات المصدر إلى بايت كود، مع النظام القياسي، لتحويله إلى نموذج كائنات المدقق.
تم ترجمة النموذج إلى لغة Boogie الوسيطة.
يتم تمرير كود Boogie إلى نظام التحقق من Boogie، لتوليد شروط التحقق.
تمرير شروط التحقق إلى محلل Z3 ( محلل SMT الذي طوّرته مايكروسوفت ).
Z3 يتحقق مما إذا كانت صيغة SMT غير قابلة للإرضاء. إذا كان الأمر كذلك، فهذا يدل على أن المواصفة صحيحة؛ وإلا يتم إنشاء نموذج يفي بالشروط.
استعادة تقرير التشخيص إلى أخطاء على مستوى المصدر.
تستخدم Move لغة مواصفات Move لوصف النظام. إنها مجموعة فرعية من لغة Move، تدعم الوصف الثابت لسلوك صحة البرنامج دون التأثير على الإنتاج. يمكن كتابتها بشكل مستقل كملف مخصص، يفصل بين كود الأعمال وكود التحقق الشكلية.
Move Prover هو أداة مفيدة تساعد المطورين على ضمان صحة العقود الذكية. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع المتوقع، مما يساعد على تقليل مخاطر المعاملات، مما يسمح للمطورين بنشر العقود الذكية في بيئة الإنتاج بثقة أكبر.
4. الملخص
تتميز لغة Move بتصميم أمان ممتاز، حيث تقدم اعتبارات شاملة في خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. تضحي خصائص اللغة بجزء من المرونة، مما يفرض الفحص الصارم للأنواع والمنطق الخطي، ما يسهل الأتمتة والتحقق الرسمي من الفحص والأمان القابل للتحقق. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى مع متطلبات إدارة أمان الأصول على البلوكشين.
على المستوى اللغوي، يمكن لـ Move تجنب الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وحقن Call/DeleGateCall بشكل فعال. ومع ذلك، لا تزال مشكلات مثل المصادقة، ومنطق الشيفرة، وتجاوز هياكل الأعداد الكبيرة بحاجة إلى اهتمام المطورين. قد لا يعمل Move Prover عندما يكون هناك إهمال في الفهم العام.
على الرغم من أن لغة Move اعتبرت الكثير من الأمور المتعلقة بالأمان للمبرمجين، إلا أنه لا توجد لغة أو برامج آمنة تمامًا. يُنصح مطوري العقود الذكية بلغة Move باستخدام خدمات تدقيق الشركات الأمنية الخارجية، وتفويض كتابة والتحقق من جزء من الشيفرة الخاصة بالمواصفات لشركات الأمان الخارجية.
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تحليل أمان لغة Move: نموذج جديد للعقود الذكية
تحليل أمان لغة Move: ثائر لغة العقود الذكية
المقدمة
لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئات blockchain التي تنفذ MoveVM. تم تصميمها مع مراعاة العديد من قضايا الأمان المتعلقة بالبلوكشين والعقود الذكية، واستمدت بعض أفكار تصميم الأمان من لغة Rust. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة التي تواجهها الآلات الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو من خلال آليات ذات صلة؟ هل توجد مشاكل أمان فريدة خاصة بـ Move؟
ستتناول هذه المقالة قضية أمان لغة Move من ثلاثة جوانب: خصائص اللغة، وآلية التشغيل، وأدوات التحقق.
1. ميزات الأمان في لغة Move
على عكس العديد من لغات البرمجة الموجودة، تم تصميم لغة Move لدعم التفاعل الآمن مع التعليمات البرمجية غير الموثوقة، بالإضافة إلى دعم التحقق الثابت. تتخلى Move عن المنطق غير الخطي القائم على المرونة، ولا تدعم التوزيع الديناميكي أو الاستدعاءات الخارجية العودية، بل تستخدم مفاهيم مثل الجنريك، التخزين العالمي، والموارد لتحقيق نماذج برمجة بديلة. على سبيل المثال، تتجاوز Move الخصائص الديناميكية مثل الجدولة الديناميكية والاستدعاءات العودية التي قد تؤدي إلى ثغرات إعادة الدخول.
تشمل الخصائص الأمنية الرئيسية لـ Move:
الوحدة: تتكون كل وحدة Move من سلسلة من تعريفات الأنواع الهيكلية والإجراءات. يمكن للوحدة استيراد تعريفات الأنواع واستدعاء الإجراءات المعلنة في وحدات أخرى.
الهيكل: يمكن تعريفه كنوع من الموارد، ويشير إلى ما يمكن تخزينه في تخزين المفاتيح/القيم العالمي الدائم.
العملية: تعريف عملية التهيئة، وعملية الأمان، وعملية عدم الأمان.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، والتي يمكن قراءتها وكتابتها برمجياً فقط بواسطة الوحدة التي تمتلكها.
فحص الثوابت: يدعم فحص الثوابت الثابتة، لضمان سلامة الموارد في النظام.
مُحقق بايت كود: يُنفذ نظام النوع على مستوى بايت كود، لمنع العمليات غير القانونية لوحدات العميل الخبيثة.
من خلال آلية فحص الثوابت ومدقق بايت الكود، يحقق Move ضمانًا مزدوجًا لسلامة الكود في وقت الترجمة.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكن الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يجعل Move تعمل بأمان في بيئات غير موثوقة، دون أن تتعرض للتلف أو الإساءة.
تتم تنفيذ برنامج Move على المكدس، حيث يتم تقسيم التخزين العالمي إلى قسمين: الذاكرة ( المكدس ) والمتغيرات العالمية (. الذاكرة هي تخزين من الدرجة الأولى، حيث لا يمكن لوحداتها تخزين مؤشرات تشير إلى وحدات الذاكرة. يتم استخدام المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، ولكن طريقة الفهرسة تختلف عن الذاكرة.
تُنفذ تعليمات بايت كود Move في مفسر يعتمد على المكدس. من السهل تنفيذ الماكينة الافتراضية المكدسية والتحكم فيها، وتتطلب متطلبات أقل من البيئة المادية، مما يجعلها مناسبة لمشاهد blockchain. مقارنةً بالمفسر القائم على السجلات، يكون من الأسهل التحكم في عمليات النسخ والتحريك بين المتغيرات واكتشافها باستخدام المفسر القائم على المكدس.
تكون حالة تشغيل برنامج Move عبارة عن رباعي ⟨C، M، G، S⟩، والذي يتضمن مكدس الاستدعاء )C(، الذاكرة )M(، المتغيرات العالمية )G( وOperands )S(. كما يحتفظ المكدس بجدول الدوال لتحليل التعليمات التي تحتوي على جسم الدالة.
تقوم MoveVM بفصل البيانات المخزنة ومنطق العملية على مكدس الاستدعاء )، وهذا هو الاختلاف الأكبر مع EVM. في MoveVM، يتم تخزين الموارد ( تحت عنوان حساب حالة المستخدم ) بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع القواعد الإلزامية المتعلقة بالأذونات والموارد. هذه التصميم يضحي ببعض المرونة، لكنه يساعد في تحقيق تحسين كبير في الأمان وكفاءة التنفيذ ( من حيث التنفيذ المتزامن ).
3. نقل البروفر
Move Prover هي أداة للتحقق الرسمي تستند إلى الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات.
تستخدم Move Prover خوارزمية التحقق الاستنتاجي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. وهذا يعني أنه يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن التطابق مع السلوك المتوقع. يساعد ذلك في ضمان صحة البرنامج وتقليل عبء العمل اليدوي للاختبار.
تدفق العمل لـ Move Prover كما يلي:
تستخدم Move لغة مواصفات Move لوصف النظام. إنها مجموعة فرعية من لغة Move، تدعم الوصف الثابت لسلوك صحة البرنامج دون التأثير على الإنتاج. يمكن كتابتها بشكل مستقل كملف مخصص، يفصل بين كود الأعمال وكود التحقق الشكلية.
Move Prover هو أداة مفيدة تساعد المطورين على ضمان صحة العقود الذكية. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع المتوقع، مما يساعد على تقليل مخاطر المعاملات، مما يسمح للمطورين بنشر العقود الذكية في بيئة الإنتاج بثقة أكبر.
4. الملخص
تتميز لغة Move بتصميم أمان ممتاز، حيث تقدم اعتبارات شاملة في خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. تضحي خصائص اللغة بجزء من المرونة، مما يفرض الفحص الصارم للأنواع والمنطق الخطي، ما يسهل الأتمتة والتحقق الرسمي من الفحص والأمان القابل للتحقق. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى مع متطلبات إدارة أمان الأصول على البلوكشين.
على المستوى اللغوي، يمكن لـ Move تجنب الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وحقن Call/DeleGateCall بشكل فعال. ومع ذلك، لا تزال مشكلات مثل المصادقة، ومنطق الشيفرة، وتجاوز هياكل الأعداد الكبيرة بحاجة إلى اهتمام المطورين. قد لا يعمل Move Prover عندما يكون هناك إهمال في الفهم العام.
على الرغم من أن لغة Move اعتبرت الكثير من الأمور المتعلقة بالأمان للمبرمجين، إلا أنه لا توجد لغة أو برامج آمنة تمامًا. يُنصح مطوري العقود الذكية بلغة Move باستخدام خدمات تدقيق الشركات الأمنية الخارجية، وتفويض كتابة والتحقق من جزء من الشيفرة الخاصة بالمواصفات لشركات الأمان الخارجية.