لغة Move هي لغة العقود الذكية المصممة لبيئة البلوكشين، ويمكن تشغيلها على السلاسل التي تدعم MoveVM. تم تصميمها مع مراعاة قضايا الأمان المتعلقة بالبلوكشين والعقود الذكية، واستندت إلى بعض مبادئ التصميم الآمن للغة Rust. ستتناول هذه المقالة تحليل أمان لغة Move من ثلاثة جوانب: ميزات اللغة، وآلية التشغيل، وأدوات التحقق.
1. ميزات الأمان في لغة Move
تزيد لغة Move الأمان من خلال التخلي عن بعض المرونة، ولا تدعم التوزيع الديناميكي واستدعاءات خارجية تكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، والموارد لتحقيق نمط برمجة بديل.
تشمل المكونات الرئيسية لـ Move:
الوحدة: تتكون من نوع الهيكل وتعريف العملية
الهيكل: يمكن تعريفه كنوع من الموارد، يتم تخزينه في التخزين العالمي للمفاتيح والقيم.
العملية: تعريف منطق العقد
تسمح التخزين العالمي لـ Move بتخزين البيانات بشكل دائم، ويمكن قراءتها وكتابتها برمجيًا فقط بواسطة الوحدات المالكة، ولكن يمكن عرضها في دفتر الأستاذ العام.
تضمن Move أمان الكود أثناء الترجمة من خلال آليتين:
قاعدة الثوابت: تستخدم للفحص الثابت، وتحديد الحفاظ على حالة النظام
مدقق بايت كود: تنفيذ نوع الأمان والخطية بشكل إلزامي، لمنع العمليات غير القانونية
2. آلية تشغيل Move
تعمل برامج Move داخل آلة افتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. تستخدم نموذج تنفيذ قائم على المكدس، وتقسم التخزين العالمي إلى ذاكرة ( ومكدس ) للمتغيرات العالمية (.
تتكون حالة Move من مكدس الاستدعاء والذاكرة والمتغيرات العالمية والعمليات. خلال التنفيذ، يحتفظ مكدس الاستدعاء بمعلومات السياق، وتجنب القفز الثابت التوزيع الديناميكي، مما يمنع هجمات إعادة الدخول.
تقوم MoveVM بفصل تخزين البيانات وعداد الاستدعاء، مما يميزها عن EVM. يعزز هذا التصميم الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغات العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
) 3. نقل المدقق
Move Prover هي أداة تحقق رسمية تستخدم خوارزميات التحقق الاستنتاجي للتحقق من صحة البرامج. يتمثل سير العمل الخاص بها في:
استلام ملف Move المصدر والمعايير
تحويل إلى بايت كود والتحقق من نموذج الكائنات
تحويل إلى لغة Boogie الوسيطة
إنشاء شروط التحقق
استخدام محلل Z3 للتحقق
إنشاء تقرير تشخيصي
تستخدم لغة مواصفات الحركة لوصف مواصفات البرنامج، ويمكن كتابتها بشكل مستقل عن رمز العمل.
4. ملخص
تأخذ لغة Move في الاعتبار الجوانب المتعلقة بتصميم اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان بشكل شامل. لقد sacrificed بعض المرونة، ولكن هذا أدى إلى تحسين الأمان وقابلية التحقق. يمكن تجنب الثغرات الشائعة في EVM مثل إعادة الدخول والتجاوز بفعالية، ولكن لا يزال من الضروري الانتباه إلى مشكلات مثل التحقق من الهوية، والمنطق، وتجاوز الأعداد الكبيرة.
على الرغم من أن Move توفر ضمانات أمان متعددة، إلا أنه يُنصح المطورين باستخدام خدمات التدقيق الأمني من طرف ثالث، وإعطاء كتابة المعايير والتحقق منها لشركات الأمن المتخصصة.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية]###https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تسجيلات الإعجاب 26
أعجبني
26
8
إعادة النشر
مشاركة
تعليق
0/400
CountdownToBroke
· 08-04 13:47
مرة أخرى قام rust哥 بالنسخ، تقريبًا يعادل أن铁子 كتب نسخة مُنقَّحة
شاهد النسخة الأصليةرد0
TerraNeverForget
· 08-03 01:26
أنت تتحدث عن "卷move" مرة أخرى، أليس كذلك؟ إذن سأشارك أيضًا.
شاهد النسخة الأصليةرد0
DuckFluff
· 08-02 19:38
واستفاد من Rust جزئيًا، يبدو أن كل شيء معقد جدًا.
شاهد النسخة الأصليةرد0
SurvivorshipBias
· 08-01 22:52
نقل آمن للغاية، بعد الآن لن يكون لدى عصابة القرش ما تأكله.
تحليل شامل لسلامة لغة Move: ميزات اللغة، آلية التشغيل وأدوات التحقق
تحليل أمان لغة Move
المقدمة
لغة Move هي لغة العقود الذكية المصممة لبيئة البلوكشين، ويمكن تشغيلها على السلاسل التي تدعم MoveVM. تم تصميمها مع مراعاة قضايا الأمان المتعلقة بالبلوكشين والعقود الذكية، واستندت إلى بعض مبادئ التصميم الآمن للغة Rust. ستتناول هذه المقالة تحليل أمان لغة Move من ثلاثة جوانب: ميزات اللغة، وآلية التشغيل، وأدوات التحقق.
1. ميزات الأمان في لغة Move
تزيد لغة Move الأمان من خلال التخلي عن بعض المرونة، ولا تدعم التوزيع الديناميكي واستدعاءات خارجية تكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، والموارد لتحقيق نمط برمجة بديل.
تشمل المكونات الرئيسية لـ Move:
تسمح التخزين العالمي لـ Move بتخزين البيانات بشكل دائم، ويمكن قراءتها وكتابتها برمجيًا فقط بواسطة الوحدات المالكة، ولكن يمكن عرضها في دفتر الأستاذ العام.
تضمن Move أمان الكود أثناء الترجمة من خلال آليتين:
قاعدة الثوابت: تستخدم للفحص الثابت، وتحديد الحفاظ على حالة النظام
مدقق بايت كود: تنفيذ نوع الأمان والخطية بشكل إلزامي، لمنع العمليات غير القانونية
2. آلية تشغيل Move
تعمل برامج Move داخل آلة افتراضية، ولا يمكنها الوصول مباشرة إلى ذاكرة النظام. تستخدم نموذج تنفيذ قائم على المكدس، وتقسم التخزين العالمي إلى ذاكرة ( ومكدس ) للمتغيرات العالمية (.
تتكون حالة Move من مكدس الاستدعاء والذاكرة والمتغيرات العالمية والعمليات. خلال التنفيذ، يحتفظ مكدس الاستدعاء بمعلومات السياق، وتجنب القفز الثابت التوزيع الديناميكي، مما يمنع هجمات إعادة الدخول.
تقوم MoveVM بفصل تخزين البيانات وعداد الاستدعاء، مما يميزها عن EVM. يعزز هذا التصميم الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغات العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
) 3. نقل المدقق
Move Prover هي أداة تحقق رسمية تستخدم خوارزميات التحقق الاستنتاجي للتحقق من صحة البرامج. يتمثل سير العمل الخاص بها في:
تستخدم لغة مواصفات الحركة لوصف مواصفات البرنامج، ويمكن كتابتها بشكل مستقل عن رمز العمل.
4. ملخص
تأخذ لغة Move في الاعتبار الجوانب المتعلقة بتصميم اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان بشكل شامل. لقد sacrificed بعض المرونة، ولكن هذا أدى إلى تحسين الأمان وقابلية التحقق. يمكن تجنب الثغرات الشائعة في EVM مثل إعادة الدخول والتجاوز بفعالية، ولكن لا يزال من الضروري الانتباه إلى مشكلات مثل التحقق من الهوية، والمنطق، وتجاوز الأعداد الكبيرة.
على الرغم من أن Move توفر ضمانات أمان متعددة، إلا أنه يُنصح المطورين باستخدام خدمات التدقيق الأمني من طرف ثالث، وإعطاء كتابة المعايير والتحقق منها لشركات الأمن المتخصصة.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية]###https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(