تعتبر لغة Move كلغة عقود ذكية من الجيل الجديد، حيث تتميز بتصميم أمان رائع. ستتناول هذه المقالة تحليل أمان Move من ثلاثة جوانب: خصائص اللغة، وآلية التشغيل، وأدوات التحقق.
1. الميزات الأمنية للغة Move
تخلى لغة Move عن المنطق غير الخطي في تصميمها، ولا تدعم التوزيع الديناميكي أو الاستدعاءات الخارجية التكرارية، بل تعتمد على مفاهيم مثل الجينيريك والتخزين العالمي والموارد لتحقيق نماذج برمجية بديلة. هذه الخصائص تتجنب بشكل فعال الثغرات الشائعة مثل إعادة الدخول.
تتضمن آلية الأمان الأساسية لـ Move ما يلي:
الوحدة: تتكون كل وحدة من نوع الهيكل وتعريف العملية، ويمكن استيراد تعريفات النوع من وحدات أخرى.
الهيكل: يمكن تعريفه كنوع من الموارد، مخزنة في التخزين العالمي للمفاتيح والقيم.
التخزين العالمي: يسمح بتخزين البيانات بشكل دائم، ويمكن قراءتها وكتابتها برمجياً فقط من قبل من يمتلك الوحدة.
مُحقق بايت الكود: ينفذ أنواع الأمان والتسلسل الهرمي لمنع العمليات غير القانونية على قيم أنواع الموارد.
قاعدة عدم المتغيرات: يمكن تعريف عدم المتغيرات لفحص ثابت، لضمان أمان الشفرة.
2. آلية تشغيل Move
تعمل برنامج Move في الآلة الافتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. تتكون حالتها من كومة الاستدعاء، والذاكرة، والمتغيرات العالمية، ومصفوفة العمليات.
تقوم MoveVM بفصل تخزين البيانات عن مكدس الاستدعاء، وهذا يختلف بشكل كبير عن EVM. يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الأذونات والموارد، مما يعزز الأمان وكفاءة التنفيذ.
![تحليل أمان Move: لغة العقود الذكية التي غيرت قواعد اللعبة])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. نقل المبرهن
Move Prover هي أداة للتحقق الشكلية، تستخدم خوارزمية التحقق الاستنتاجي للتحقق مما إذا كانت البرامج تتوافق مع التوقعات. سير العمل الخاص بها هو كما يلي:
استلام مدخلات ملف Move المصدر، استخراج المواصفات
تحويل إلى بايت كود، تحويل إلى نموذج كائن المدقق
ترجمة إلى لغة Boogie الوسيطة
إنشاء شروط التحقق
استخدام محلل Z3 للتحقق من صيغ SMT
إنشاء تقرير تشخيصي
تُستخدم لغة مواصفات الحركة لوصف المواصفات، ويمكن كتابتها بشكل مستقل دون التأثير على كود الإنتاج.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
ملخص
تأخذ Move في الاعتبار خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان بشكل شامل. إنها تتجنب الثغرات الشائعة مثل إعادة الدخول، والتجاوز، لكن لا تزال مشاكل إدارة الأذونات، والأخطاء المنطقية تحتاج إلى انتباه المطورين. يُنصح باستخدام تدقيق أمان من طرف ثالث، وترك الأمر لفريق متخصص لكتابة كود معيار التحقق.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تسجيلات الإعجاب 20
أعجبني
20
5
إعادة النشر
مشاركة
تعليق
0/400
MEVHunterZhang
· 07-13 14:53
طالما أن الأمان قوي بما فيه الكفاية، فكل شيء آخر هو وهم.
تحليل شامل لأمان لغة Move: الخصائص والآليات وأدوات التحقق
تحليل أمان لغة Move
تعتبر لغة Move كلغة عقود ذكية من الجيل الجديد، حيث تتميز بتصميم أمان رائع. ستتناول هذه المقالة تحليل أمان Move من ثلاثة جوانب: خصائص اللغة، وآلية التشغيل، وأدوات التحقق.
1. الميزات الأمنية للغة Move
تخلى لغة Move عن المنطق غير الخطي في تصميمها، ولا تدعم التوزيع الديناميكي أو الاستدعاءات الخارجية التكرارية، بل تعتمد على مفاهيم مثل الجينيريك والتخزين العالمي والموارد لتحقيق نماذج برمجية بديلة. هذه الخصائص تتجنب بشكل فعال الثغرات الشائعة مثل إعادة الدخول.
تتضمن آلية الأمان الأساسية لـ Move ما يلي:
الوحدة: تتكون كل وحدة من نوع الهيكل وتعريف العملية، ويمكن استيراد تعريفات النوع من وحدات أخرى.
الهيكل: يمكن تعريفه كنوع من الموارد، مخزنة في التخزين العالمي للمفاتيح والقيم.
التخزين العالمي: يسمح بتخزين البيانات بشكل دائم، ويمكن قراءتها وكتابتها برمجياً فقط من قبل من يمتلك الوحدة.
مُحقق بايت الكود: ينفذ أنواع الأمان والتسلسل الهرمي لمنع العمليات غير القانونية على قيم أنواع الموارد.
قاعدة عدم المتغيرات: يمكن تعريف عدم المتغيرات لفحص ثابت، لضمان أمان الشفرة.
2. آلية تشغيل Move
تعمل برنامج Move في الآلة الافتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. تتكون حالتها من كومة الاستدعاء، والذاكرة، والمتغيرات العالمية، ومصفوفة العمليات.
تقوم MoveVM بفصل تخزين البيانات عن مكدس الاستدعاء، وهذا يختلف بشكل كبير عن EVM. يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الأذونات والموارد، مما يعزز الأمان وكفاءة التنفيذ.
![تحليل أمان Move: لغة العقود الذكية التي غيرت قواعد اللعبة])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
3. نقل المبرهن
Move Prover هي أداة للتحقق الشكلية، تستخدم خوارزمية التحقق الاستنتاجي للتحقق مما إذا كانت البرامج تتوافق مع التوقعات. سير العمل الخاص بها هو كما يلي:
تُستخدم لغة مواصفات الحركة لوصف المواصفات، ويمكن كتابتها بشكل مستقل دون التأثير على كود الإنتاج.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
ملخص
تأخذ Move في الاعتبار خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان بشكل شامل. إنها تتجنب الثغرات الشائعة مثل إعادة الدخول، والتجاوز، لكن لا تزال مشاكل إدارة الأذونات، والأخطاء المنطقية تحتاج إلى انتباه المطورين. يُنصح باستخدام تدقيق أمان من طرف ثالث، وترك الأمر لفريق متخصص لكتابة كود معيار التحقق.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(