Move هي لغة عقود ذكية يمكن تجميعها وتشغيلها في بيئات سلسلة الكتل التي تنفذ MoveVM. تم تصميمها مع مراعاة العديد من قضايا الأمان المتعلقة بسلسلة الكتل والعقود الذكية، واستفادت من بعض أفكار تصميم الأمان من لغة RUST. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان كخاصية رئيسية، كيف هي أمان Move في الواقع؟ هل يمكنها تجنب التهديدات الأمنية الشائعة لأجهزة الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو الآليات ذات الصلة؟ هل توجد مشكلات أمان خاصة بـ Move نفسها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية وآلية التشغيل وأدوات التحقق.
1. ميزات الأمان للغة Move
كتابة كود خالي من الثغرات أمر صعب، حتى مع الاختبار المتكرر لا يمكن ضمان ذلك بشكل كامل. يصبح من التحدي أكثر كتابة كود يحافظ على الخصائص الأمنية الأساسية عند التفاعل مع كود غير موثوق. هناك تقنيات متعددة يمكن استخدامها لفرض الأمان أثناء التشغيل، مثل الصناديق الرملية، وعزل العمليات، وأنماط برمجة قفل الكائنات؛ كما يمكن تحديد الأمان الثابت أثناء الترجمة، مثل فرض الأنواع الثابتة أو فحوصات التأكيد.
أحيانًا يمكن الاستعانة بتحليل المعاني وأدوات التحليل الثابت للتأكد من توافق الشيفرة مع قواعد الأمان، حتى عند التفاعل مع شيفرة غير موثوقة يمكن الحفاظ على بعض الشروط المنطقية القابلة للإثبات. تبدو هذه الأساليب جيدة، حيث يمكن أن تتجنب تكاليف التشغيل وتكتشف المشكلات الأمنية مسبقًا. ومع ذلك، فإن الأمان الذي تحققه لغات البرمجة من خلال هذه الأساليب محدود للغاية، لسببين رئيسيين: أولاً، غالبًا ما تحتوي على ميزات لغوية يصعب تحليلها باستخدام أدوات التحليل الثابت، مثل التوزيع الديناميكي، والقدرة على المشاركة والتغيير، والانعكاس، وغيرها من المنطق غير الخطي، وهذه الميزات تنتهك قواعد الثوابت الأمنية، مما يوفر لمهاجميها مساحة واسعة للهجوم. ثانيًا، من الصعب توسيع معظم لغات البرمجة لدعم أدوات تحليل ثابتة ذات صلة بالأمان أو لغات تعبيرية قوية، على الرغم من أن كلا التوسيعين مهمان.
تصميم لغة Move يدعم التفاعل الآمن مع التعليمات البرمجية غير الموثوق بها وكذلك التحقق الثابت. إنها تتمتع بهذه الميزات الأمنية لأنها تتخلى عن جميع المنطق غير الخطي القائم على اعتبارات المرونة، ولا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنواع العامة، والتخزين العالمي، والموارد لتحقيق بعض أنماط البرمجة البديلة. على سبيل المثال، تتجاهل Move ميزات التوزيع الديناميكي والاستدعاء التكراري، وهي ميزات أدت في لغات العقود الذكية الأخرى إلى ثغرات إعادة الدخول المكلفة.
تشمل الميزات الأمنية الرئيسية للغة Move:
التعديل: يتكون كل وحدة Move من سلسلة من تعريفات الأنواع الهيكلية والعمليات. يمكن للوحدات استيراد تعريفات الأنواع المعلنة في وحدات أخرى واستدعاء العمليات.
الهيكل: يمكن تعريف الهيكل من نوع المورد، والذي يستخدم لتمثيل البيانات القابلة للتخزين في تخزين المفاتيح/القيم العالمي.
العملية: تم تعريف عملية التهيئة، والأمان، والعمليات غير الآمنة. يمكن أن تحتوي العمليات على قيود التحكم في الوصول.
التخزين العالمي: يسمح بتخزين البيانات الدائمة، ويمكن قراءتها وكتابتها برمجيًا فقط بواسطة الوحدة المالكة لها.
فحص الثوابت: يمكن تعريف الثوابت لفحص ثابت لضمان سلامة الموارد في النظام.
مدقق بايت كود: يفرض نظام النوع على مستوى بايت كود، مما يمنع إنشاء أو فك أو الإشارة إلى الموارد بشكل غير مناسب.
تتيح هذه الميزات لـ Move تقديم ضمانات أمان قوية في كل من وقت الترجمة ووقت التشغيل.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام، مما يضمن أنها يمكن أن تعمل بأمان في بيئات غير موثوقة.
تستخدم Move نموذج تنفيذ قائم على المكدس. يتم تقسيم التخزين العالمي إلى قسمين: الذاكرة ( كومة ) ومتغيرات عالمية ( مكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكنها تخزين المؤشرات التي تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين المؤشرات التي تشير إلى وحدات الذاكرة، ويتم الوصول إليها عبر العنوان والنوع.
يستخدم Move مفسر قائم على المكدس لتنفيذ تعليمات بايت كود، هذه الطريقة سهلة التنفيذ والتحكم، وتتطلب متطلبات منخفضة من الأجهزة، مما يجعلها مناسبة لسيناريوهات البلوكشين. مقارنةً بمفسر قائم على المسجل، فإن المفسر القائم على المكدس يسهل التحكم والكشف عن نسخ وتحركات المتغيرات.
حالة تشغيل برنامج Move هي رباعية ⟨C, M, G, S⟩، تشمل مكدس الاستدعاء (C)، الذاكرة (M)، المتغيرات العالمية (G) ومكدس المعاملات (S). يحتوي مكدس الاستدعاء على معلومات سياق تنفيذ العملية ورقم التعليمات. عند تنفيذ تعليمة Call، يتم إنشاء كائن مكدس استدعاء جديد، وتخزين المعلمات وتنفيذ تعليمات العقد الجديد. عند مواجهة تعليمات الفرع، يتم إجراء قفز ثابت داخل العملية.
يفصل MoveVM بين تخزين البيانات ومكدس الاستدعاء، وهذه هي الفروق الرئيسية بينها وبين EVM. في Move، يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الأذونات والموارد. تضحي هذه التصميم بقدر من المرونة، لكنها تعزز الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. نقل المدقق
Move Prover هو أداة تحقق رسمية قائمة على الاستدلال، يمكن أن تساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. يستخدم لغة رسمية لوصف سلوك البرنامج، ومن خلال خوارزميات الاستدلال يتحقق مما إذا كان البرنامج يتوافق مع التوقعات.
تستخدم Move Prover خوارزمية التحقق الاستدلالي لاستنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن توافقه مع التوقعات. يساعد ذلك في ضمان صحة البرنامج وتقليل عبء العمل للاختبارات اليدوية.
تدفق عمل Move Prover هو كما يلي:
استلام ملف Move المصدر كمدخل، والذي يحتوي على مواصفات البرنامج
يقوم المحلل باستخراج المواصفات، والمترجم يجمع الشيفرة المصدرية إلى بايت كود
إنشاء نموذج كائن المدقق
ترجمة النموذج إلى لغة Boogie الوسيطة
نظام بوغي للتحقق من توليد شروط التحقق
تمرير شروط التحقق إلى محلل Z3 للفحص
إنشاء تقرير تشخيصي وتحويله إلى أخطاء على مستوى الشيفرة المصدرية
توفر Move لغة مواصفات Move لوصف المواصفات، وهي مجموعة فرعية من لغة Move، تدعم الوصف الثابت لسلوك صحة البرنامج. يمكن كتابة المواصفات بشكل مستقل عن كود الأعمال.
Move Prover هي أداة قوية يمكن أن تساعد المطورين في ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. إنها تستخدم طرقًا رسمية للتحقق مما إذا كانت البرامج تتوافق مع التوقعات، مما يزيد من ثقة المطورين عند نشر العقود الذكية.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
ملخص
تعتبر لغة Move شاملة من حيث الأمان، حيث توفر حماية قوية من خصائص اللغة، وتنفيذ الآلة الافتراضية، إلى أدوات الأمان. لقد sacrificedت بعض المرونة، حيث تفرض فحص الأنواع والتحقق المنطقي الخطي، مما يفيد في أتمتة عملية الفحص والترتيب الرسمي. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى أكثر مع متطلبات إدارة أمان الأصول على blockchain.
لغة Move يمكن أن تتجنب بشكل فعال الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وثغرات Call/DeleGateCall. ولكن لا يزال يتعين على المطورين الانتباه بشكل خاص لمشاكل مثل التحقق من الهوية، ومنطق الشفرة، وتجاوز بنية الأعداد الكبيرة. على الرغم من أن Move Prover قوي، إلا أنه لا يمكنه تجنب الإغفالات في التصميم العام تمامًا.
على الرغم من أن Move قد أخذت في الاعتبار الكثير من جوانب الأمان، إلا أنه لا توجد لغة أو برنامج آمن تمامًا. يُنصح مطورين العقود الذكية باستخدام خدمات تدقيق الشركات الأمنية الخارجية، وتكليف الفرق الأمنية المتخصصة بكتابة والتحقق من أجزاء المعايير.
![تحليل أمان Move: لغة العقود الذكية التي غيرت اللعبة])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تحليل عميق لخصائص الأمان في لغة Move: من تصميم اللغة إلى التحقق الرسمي
تحليل أمان لغة Move
المقدمة
Move هي لغة عقود ذكية يمكن تجميعها وتشغيلها في بيئات سلسلة الكتل التي تنفذ MoveVM. تم تصميمها مع مراعاة العديد من قضايا الأمان المتعلقة بسلسلة الكتل والعقود الذكية، واستفادت من بعض أفكار تصميم الأمان من لغة RUST. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان كخاصية رئيسية، كيف هي أمان Move في الواقع؟ هل يمكنها تجنب التهديدات الأمنية الشائعة لأجهزة الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو الآليات ذات الصلة؟ هل توجد مشكلات أمان خاصة بـ Move نفسها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية وآلية التشغيل وأدوات التحقق.
1. ميزات الأمان للغة Move
كتابة كود خالي من الثغرات أمر صعب، حتى مع الاختبار المتكرر لا يمكن ضمان ذلك بشكل كامل. يصبح من التحدي أكثر كتابة كود يحافظ على الخصائص الأمنية الأساسية عند التفاعل مع كود غير موثوق. هناك تقنيات متعددة يمكن استخدامها لفرض الأمان أثناء التشغيل، مثل الصناديق الرملية، وعزل العمليات، وأنماط برمجة قفل الكائنات؛ كما يمكن تحديد الأمان الثابت أثناء الترجمة، مثل فرض الأنواع الثابتة أو فحوصات التأكيد.
أحيانًا يمكن الاستعانة بتحليل المعاني وأدوات التحليل الثابت للتأكد من توافق الشيفرة مع قواعد الأمان، حتى عند التفاعل مع شيفرة غير موثوقة يمكن الحفاظ على بعض الشروط المنطقية القابلة للإثبات. تبدو هذه الأساليب جيدة، حيث يمكن أن تتجنب تكاليف التشغيل وتكتشف المشكلات الأمنية مسبقًا. ومع ذلك، فإن الأمان الذي تحققه لغات البرمجة من خلال هذه الأساليب محدود للغاية، لسببين رئيسيين: أولاً، غالبًا ما تحتوي على ميزات لغوية يصعب تحليلها باستخدام أدوات التحليل الثابت، مثل التوزيع الديناميكي، والقدرة على المشاركة والتغيير، والانعكاس، وغيرها من المنطق غير الخطي، وهذه الميزات تنتهك قواعد الثوابت الأمنية، مما يوفر لمهاجميها مساحة واسعة للهجوم. ثانيًا، من الصعب توسيع معظم لغات البرمجة لدعم أدوات تحليل ثابتة ذات صلة بالأمان أو لغات تعبيرية قوية، على الرغم من أن كلا التوسيعين مهمان.
تصميم لغة Move يدعم التفاعل الآمن مع التعليمات البرمجية غير الموثوق بها وكذلك التحقق الثابت. إنها تتمتع بهذه الميزات الأمنية لأنها تتخلى عن جميع المنطق غير الخطي القائم على اعتبارات المرونة، ولا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنواع العامة، والتخزين العالمي، والموارد لتحقيق بعض أنماط البرمجة البديلة. على سبيل المثال، تتجاهل Move ميزات التوزيع الديناميكي والاستدعاء التكراري، وهي ميزات أدت في لغات العقود الذكية الأخرى إلى ثغرات إعادة الدخول المكلفة.
تشمل الميزات الأمنية الرئيسية للغة Move:
التعديل: يتكون كل وحدة Move من سلسلة من تعريفات الأنواع الهيكلية والعمليات. يمكن للوحدات استيراد تعريفات الأنواع المعلنة في وحدات أخرى واستدعاء العمليات.
الهيكل: يمكن تعريف الهيكل من نوع المورد، والذي يستخدم لتمثيل البيانات القابلة للتخزين في تخزين المفاتيح/القيم العالمي.
العملية: تم تعريف عملية التهيئة، والأمان، والعمليات غير الآمنة. يمكن أن تحتوي العمليات على قيود التحكم في الوصول.
التخزين العالمي: يسمح بتخزين البيانات الدائمة، ويمكن قراءتها وكتابتها برمجيًا فقط بواسطة الوحدة المالكة لها.
فحص الثوابت: يمكن تعريف الثوابت لفحص ثابت لضمان سلامة الموارد في النظام.
مدقق بايت كود: يفرض نظام النوع على مستوى بايت كود، مما يمنع إنشاء أو فك أو الإشارة إلى الموارد بشكل غير مناسب.
تتيح هذه الميزات لـ Move تقديم ضمانات أمان قوية في كل من وقت الترجمة ووقت التشغيل.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام، مما يضمن أنها يمكن أن تعمل بأمان في بيئات غير موثوقة.
تستخدم Move نموذج تنفيذ قائم على المكدس. يتم تقسيم التخزين العالمي إلى قسمين: الذاكرة ( كومة ) ومتغيرات عالمية ( مكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكنها تخزين المؤشرات التي تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين المؤشرات التي تشير إلى وحدات الذاكرة، ويتم الوصول إليها عبر العنوان والنوع.
يستخدم Move مفسر قائم على المكدس لتنفيذ تعليمات بايت كود، هذه الطريقة سهلة التنفيذ والتحكم، وتتطلب متطلبات منخفضة من الأجهزة، مما يجعلها مناسبة لسيناريوهات البلوكشين. مقارنةً بمفسر قائم على المسجل، فإن المفسر القائم على المكدس يسهل التحكم والكشف عن نسخ وتحركات المتغيرات.
حالة تشغيل برنامج Move هي رباعية ⟨C, M, G, S⟩، تشمل مكدس الاستدعاء (C)، الذاكرة (M)، المتغيرات العالمية (G) ومكدس المعاملات (S). يحتوي مكدس الاستدعاء على معلومات سياق تنفيذ العملية ورقم التعليمات. عند تنفيذ تعليمة Call، يتم إنشاء كائن مكدس استدعاء جديد، وتخزين المعلمات وتنفيذ تعليمات العقد الجديد. عند مواجهة تعليمات الفرع، يتم إجراء قفز ثابت داخل العملية.
يفصل MoveVM بين تخزين البيانات ومكدس الاستدعاء، وهذه هي الفروق الرئيسية بينها وبين EVM. في Move، يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الأذونات والموارد. تضحي هذه التصميم بقدر من المرونة، لكنها تعزز الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. نقل المدقق
Move Prover هو أداة تحقق رسمية قائمة على الاستدلال، يمكن أن تساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. يستخدم لغة رسمية لوصف سلوك البرنامج، ومن خلال خوارزميات الاستدلال يتحقق مما إذا كان البرنامج يتوافق مع التوقعات.
تستخدم Move Prover خوارزمية التحقق الاستدلالي لاستنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن توافقه مع التوقعات. يساعد ذلك في ضمان صحة البرنامج وتقليل عبء العمل للاختبارات اليدوية.
تدفق عمل Move Prover هو كما يلي:
توفر Move لغة مواصفات Move لوصف المواصفات، وهي مجموعة فرعية من لغة Move، تدعم الوصف الثابت لسلوك صحة البرنامج. يمكن كتابة المواصفات بشكل مستقل عن كود الأعمال.
Move Prover هي أداة قوية يمكن أن تساعد المطورين في ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. إنها تستخدم طرقًا رسمية للتحقق مما إذا كانت البرامج تتوافق مع التوقعات، مما يزيد من ثقة المطورين عند نشر العقود الذكية.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
ملخص
تعتبر لغة Move شاملة من حيث الأمان، حيث توفر حماية قوية من خصائص اللغة، وتنفيذ الآلة الافتراضية، إلى أدوات الأمان. لقد sacrificedت بعض المرونة، حيث تفرض فحص الأنواع والتحقق المنطقي الخطي، مما يفيد في أتمتة عملية الفحص والترتيب الرسمي. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى أكثر مع متطلبات إدارة أمان الأصول على blockchain.
لغة Move يمكن أن تتجنب بشكل فعال الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وثغرات Call/DeleGateCall. ولكن لا يزال يتعين على المطورين الانتباه بشكل خاص لمشاكل مثل التحقق من الهوية، ومنطق الشفرة، وتجاوز بنية الأعداد الكبيرة. على الرغم من أن Move Prover قوي، إلا أنه لا يمكنه تجنب الإغفالات في التصميم العام تمامًا.
على الرغم من أن Move قد أخذت في الاعتبار الكثير من جوانب الأمان، إلا أنه لا توجد لغة أو برنامج آمن تمامًا. يُنصح مطورين العقود الذكية باستخدام خدمات تدقيق الشركات الأمنية الخارجية، وتكليف الفرق الأمنية المتخصصة بكتابة والتحقق من أجزاء المعايير.
![تحليل أمان Move: لغة العقود الذكية التي غيرت اللعبة])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(