لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم تصميمها مع الأخذ في الاعتبار العديد من القضايا الأمنية المتعلقة بال blockchain والعقود الذكية، واستلهمت من بعض مفاهيم التصميم الأمني في لغة Rust. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان كخاصية رئيسية، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة في آلات العقود الافتراضية مثل EVM وWASM على مستوى اللغة أو من خلال الآليات ذات الصلة؟ هل تحتوي Move على مخاطر أمنية فريدة من نوعها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: خصائص اللغة وآلية التشغيل وأدوات التحقق.
1. الميزات الأمنية للغة Move
على عكس العديد من لغات البرمجة الحالية، فإن الهدف من تصميم لغة Move هو دعم كتابة برامج يمكنها التفاعل بأمان مع الشيفرة غير الموثوق بها، مع دعم التحقق الساكن. تحقق Move هذا الهدف من خلال التخلي عن جميع المنطق غير الخطي القائم على اعتبارات المرونة، حيث لا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، الموارد، وغيرها لتحقيق بعض أنماط البرمجة البديلة.
فيما يلي بعض ميزات الأمان الرئيسية للغة Move:
المعيارية: يتكون كل وحدة Move من سلسلة من الأنواع الهيكلية وتعريفات العمليات. يمكن للوحدة استيراد الأنواع المعلنة في وحدات أخرى واستدعاء عملياتها.
نوع المورد: يتم تعريف الهيكل بواسطة بناء جملة has key كنوع المورد، ويمكن تخزينه في تخزين مفتاح القيمة العالمي الدائم.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، حيث يمكن قراءة هذه البيانات وكتابتها برمجيًا فقط من قبل الوحدة التي تمتلكها، ولكن يمكن للوحدات الأخرى الاطلاع عليها المخزنة في دفتر الأستاذ العام.
نظام النوع الثابت: يحتوي Move على نظام نوع ثابت قوي يمكنه التقاط العديد من الأخطاء في وقت الترجمة.
نوع خطي: نوع المورد افتراضيًا هو نوع خطي، مما يمنع النسخ أو التدمير الضمني.
مبدأ الثوابت: يمكن تعريف الثوابت التي تحافظ على الحالة، لاستخدامها في التحقق الرسمي.
مدقق الشيفرة: فرض نظام النوع على مستوى الشيفرة البايتية لمنع السلوك الضار.
تساهم هذه الخصائص معًا في بناء أساس أمان لغة Move، مما يمكنها من تجنب العديد من الثغرات الشائعة في العقود الذكية.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكنها الوصول إلى ذاكرة النظام أثناء التشغيل، مما يضمن التنفيذ الآمن في بيئات غير موثوقة.
تستخدم Move مفسرًا قائمًا على المكدس لتنفيذ تعليمات بايت كود. تتكون حالته من مكدس الاستدعاء والذاكرة والمتغيرات العالمية ومكدس المعاملات. يجعل هذا التصميم من نسخ المتغيرات وتحريكها أسهل في التحكم والاكتشاف.
يفصل MoveVM بين تخزين البيانات وحزمة استدعاء الوظائف، وهذه هي أكبر اختلاف له عن EVM. يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع القواعد الإلزامية المتعلقة بالأذونات والموارد. هذه التصميم يضحي ببعض المرونة، لكنه يزيد بشكل كبير من الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. نقل المدقق
Move Prover هو أداة للتحقق الرسمي للغة Move، تستخدم خوارزمية التحقق الاستنتاجي للتحقق مما إذا كان البرنامج يتوافق مع السلوك المتوقع. يمكنها استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن تطابقه مع التوقعات، مما يساعد على ضمان صحة البرنامج وتقليل عبء الاختبار اليدوي.
تتضمن عملية Move Prover ما يلي:
استلام ملف Move كمصدر للإدخال، يجب أن يحتوي هذا الملف على مواصفات البرنامج.
استخراج المواصفات وتجميع ملفات المصدر إلى بايت كود.
تحويل المواصفات وبيانات البايت إلى نموذج كائن المدقق.
ترجمة النموذج إلى لغة Boogie الوسيطة.
نظام التحقق من Boogie يولد شروط التحقق.
يقوم موالف Z3 بالتحقق مما إذا كانت شروط التحقق مُلباة.
إنشاء تقرير تشخيص وتحويله إلى خطأ على مستوى المصدر.
تُستخدم لغة مواصفات Move لوصف مواصفات البرنامج، وهي مجموعة فرعية من لغة Move. تدعم الوصف الثابت لسلوك صحة البرنامج دون التأثير على كود الإنتاج. يمكن كتابة المواصفات بشكل مستقل، مما يسهل فصل كود الأعمال عن كود التحقق.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. الملخص
تصميم لغة Move من حيث الأمان ممتاز للغاية، حيث تم أخذ جميع الجوانب في الاعتبار بدءًا من ميزات اللغة، وتنفيذ الآلة الافتراضية، وصولاً إلى أدوات الأمان. لقد sacrificed بعض المرونة، مما يعزز فحص الأنواع والمنطق الخطي، مما يسهل الأتمتة لفحص الترجمة والتحقق الرسمي. تصميم MoveVM يفصل بين الحالة والمنطق، مما يتناسب بشكل أفضل مع احتياجات إدارة أمان الأصول على blockchain.
يمكن للغة Move أن تتجنب بشكل فعال الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وحقن Call/DeleGateCall. ومع ذلك، لا يزال يتعين على المطورين الانتباه بشكل إضافي لمشكلات مثل التحقق من الهوية، ومنطق الشفرة، وتجاوز هياكل الأعداد الكبيرة. على الرغم من أن Move تأخذ بعين الاعتبار الأمان بشكل شامل للمبرمجين، إلا أنه لا توجد لغة أو برنامج آمن بنسبة 100%. يُنصح مطورو عقود Move الذكية باستخدام خدمات تدقيق من شركات أمان خارجية، وتكليف الفرق الأمنية المهنية بكتابة الشيفرات والتأكد من صحتها.
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تسجيلات الإعجاب 17
أعجبني
17
5
إعادة النشر
مشاركة
تعليق
0/400
OptionWhisperer
· 07-15 10:34
انتقل بسرعة إلى أدنى سعر لرؤية الحركة
شاهد النسخة الأصليةرد0
NftCollectors
· 07-14 08:08
تحرك هذه المجموعة من آليات الأمان لا تقل عن النسبة الذهبية لفن البيزنطية من وجهة نظر تاريخ فن البلوكتشين، وهي تمامًا بمثابة معلم.
شاهد النسخة الأصليةرد0
BearMarketSurvivor
· 07-14 03:19
الأمان هو مجرد كلمات فارغة
شاهد النسخة الأصليةرد0
ForkTongue
· 07-14 03:08
هل هناك ألعاب جديدة لكتابة العقود؟
شاهد النسخة الأصليةرد0
FancyResearchLab
· 07-14 03:05
حفرة جديدة يحبها لو بان، من الناحية النظرية، فإنها آمنة إلى حد ما
تحليل أمان لغة Move: معيار جديد لتطوير العقود الذكية
تحليل أمان لغة Move: مبتكر العقود الذكية
لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم تصميمها مع الأخذ في الاعتبار العديد من القضايا الأمنية المتعلقة بال blockchain والعقود الذكية، واستلهمت من بعض مفاهيم التصميم الأمني في لغة Rust. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان كخاصية رئيسية، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة في آلات العقود الافتراضية مثل EVM وWASM على مستوى اللغة أو من خلال الآليات ذات الصلة؟ هل تحتوي Move على مخاطر أمنية فريدة من نوعها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: خصائص اللغة وآلية التشغيل وأدوات التحقق.
1. الميزات الأمنية للغة Move
على عكس العديد من لغات البرمجة الحالية، فإن الهدف من تصميم لغة Move هو دعم كتابة برامج يمكنها التفاعل بأمان مع الشيفرة غير الموثوق بها، مع دعم التحقق الساكن. تحقق Move هذا الهدف من خلال التخلي عن جميع المنطق غير الخطي القائم على اعتبارات المرونة، حيث لا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، الموارد، وغيرها لتحقيق بعض أنماط البرمجة البديلة.
فيما يلي بعض ميزات الأمان الرئيسية للغة Move:
المعيارية: يتكون كل وحدة Move من سلسلة من الأنواع الهيكلية وتعريفات العمليات. يمكن للوحدة استيراد الأنواع المعلنة في وحدات أخرى واستدعاء عملياتها.
نوع المورد: يتم تعريف الهيكل بواسطة بناء جملة has key كنوع المورد، ويمكن تخزينه في تخزين مفتاح القيمة العالمي الدائم.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، حيث يمكن قراءة هذه البيانات وكتابتها برمجيًا فقط من قبل الوحدة التي تمتلكها، ولكن يمكن للوحدات الأخرى الاطلاع عليها المخزنة في دفتر الأستاذ العام.
نظام النوع الثابت: يحتوي Move على نظام نوع ثابت قوي يمكنه التقاط العديد من الأخطاء في وقت الترجمة.
نوع خطي: نوع المورد افتراضيًا هو نوع خطي، مما يمنع النسخ أو التدمير الضمني.
مبدأ الثوابت: يمكن تعريف الثوابت التي تحافظ على الحالة، لاستخدامها في التحقق الرسمي.
مدقق الشيفرة: فرض نظام النوع على مستوى الشيفرة البايتية لمنع السلوك الضار.
تساهم هذه الخصائص معًا في بناء أساس أمان لغة Move، مما يمكنها من تجنب العديد من الثغرات الشائعة في العقود الذكية.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكنها الوصول إلى ذاكرة النظام أثناء التشغيل، مما يضمن التنفيذ الآمن في بيئات غير موثوقة.
تستخدم Move مفسرًا قائمًا على المكدس لتنفيذ تعليمات بايت كود. تتكون حالته من مكدس الاستدعاء والذاكرة والمتغيرات العالمية ومكدس المعاملات. يجعل هذا التصميم من نسخ المتغيرات وتحريكها أسهل في التحكم والاكتشاف.
يفصل MoveVM بين تخزين البيانات وحزمة استدعاء الوظائف، وهذه هي أكبر اختلاف له عن EVM. يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ( بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع القواعد الإلزامية المتعلقة بالأذونات والموارد. هذه التصميم يضحي ببعض المرونة، لكنه يزيد بشكل كبير من الأمان وكفاءة التنفيذ.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(
3. نقل المدقق
Move Prover هو أداة للتحقق الرسمي للغة Move، تستخدم خوارزمية التحقق الاستنتاجي للتحقق مما إذا كان البرنامج يتوافق مع السلوك المتوقع. يمكنها استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن تطابقه مع التوقعات، مما يساعد على ضمان صحة البرنامج وتقليل عبء الاختبار اليدوي.
تتضمن عملية Move Prover ما يلي:
تُستخدم لغة مواصفات Move لوصف مواصفات البرنامج، وهي مجموعة فرعية من لغة Move. تدعم الوصف الثابت لسلوك صحة البرنامج دون التأثير على كود الإنتاج. يمكن كتابة المواصفات بشكل مستقل، مما يسهل فصل كود الأعمال عن كود التحقق.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(
4. الملخص
تصميم لغة Move من حيث الأمان ممتاز للغاية، حيث تم أخذ جميع الجوانب في الاعتبار بدءًا من ميزات اللغة، وتنفيذ الآلة الافتراضية، وصولاً إلى أدوات الأمان. لقد sacrificed بعض المرونة، مما يعزز فحص الأنواع والمنطق الخطي، مما يسهل الأتمتة لفحص الترجمة والتحقق الرسمي. تصميم MoveVM يفصل بين الحالة والمنطق، مما يتناسب بشكل أفضل مع احتياجات إدارة أمان الأصول على blockchain.
يمكن للغة Move أن تتجنب بشكل فعال الثغرات الشائعة في EVM مثل إعادة الإدخال، والتجاوز، وحقن Call/DeleGateCall. ومع ذلك، لا يزال يتعين على المطورين الانتباه بشكل إضافي لمشكلات مثل التحقق من الهوية، ومنطق الشفرة، وتجاوز هياكل الأعداد الكبيرة. على الرغم من أن Move تأخذ بعين الاعتبار الأمان بشكل شامل للمبرمجين، إلا أنه لا توجد لغة أو برنامج آمن بنسبة 100%. يُنصح مطورو عقود Move الذكية باستخدام خدمات تدقيق من شركات أمان خارجية، وتكليف الفرق الأمنية المهنية بكتابة الشيفرات والتأكد من صحتها.