لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم تصميمها مع الأخذ في الاعتبار العديد من مشكلات الأمان المتعلقة بالـ blockchain والعقود الذكية، واستندت إلى تصميم الأمان في لغة RUST. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان، ما مدى أمانها؟ هل يمكنها تجنب التهديدات الأمنية الشائعة في الآلات الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو من خلال الآليات ذات الصلة؟ هل لديها مشكلات أمان فريدة من نوعها؟
ستتناول هذه المقالة قضايا أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية، آلية التشغيل وأدوات التحقق.
1. ميزات الأمان في لغة Move
تختلف لغة Move عن العديد من لغات البرمجة الحالية، حيث تم تصميمها لدعم كتابة البرامج التي تتفاعل بأمان مع الشيفرات غير الموثوقة، وكذلك لدعم التحقق الثابت. تتمتع Move بهذه الميزات الأمنية لأنها تتخلى عن المنطق غير الخطي القائم على المرونة، ولا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، الموارد، وغيرها لتحقيق أنماط برمجة بديلة. على سبيل المثال، تتجاهل Move ميزات التوزيع الديناميكي والاستدعاء التكراري، وهي ميزات تؤدي في لغات العقود الذكية الأخرى إلى ثغرات إعادة إدخال مكلفة.
تشمل الخصائص الأمنية الرئيسية لـ Move:
模块(Module): كل وحدة Move تتكون من سلسلة من أنواع الهياكل وتعريفات العمليات. يمكن للوحدات استيراد تعريفات الأنواع واستدعاء العمليات المعلن عنها في وحدات أخرى.
结构体(Structs): يمكن تعريفها على أنها نوع من الموارد، مما يعني أنه يمكن تخزينها في التخزين الدائم للمفاتيح/القيم العالمية.
过程(Function): تعريف المنطق التجاري للعقود.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، والتي يمكن قراءتها/كتابتها برمجياً فقط من قبل الوحدة التي تمتلكها.
فحص الثوابت: يمكن تعريف الثوابت لفحصها بشكل ثابت، مما يدل على الحفاظ على الموارد في النظام.
مُحقق بايت كود: يقوم بالتحقق من الأنواع الآمنة والتسوية لبايت كود، ويفرض قواعد إنشاء الموارد وتدميرها والوصول إليها.
من خلال هذه الميزات، يمكن لـ Move ضمان مستوى عالٍ من الأمان أثناء وقت الترجمة. بعد ذلك، سنحلل آلية تشغيل Move، لنرى كيف يضمن MoveVM أمان وقت التشغيل.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكن الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يسمح لـ Move بالعمل بأمان في بيئات غير موثوقة، دون أن تتعرض للتلف أو الإساءة.
تتم عملية تنفيذ برنامج Move على المكدس. يتم تقسيم التخزين العالمي إلى جزئين: الذاكرة ( الكومة ) ومتغيرات عالمية ( المكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكنها تخزين مؤشرات تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، لكن طريقة الفهرسة تختلف عن الذاكرة.
تُنفذ تعليمات بايت كود Move في مفسر قائم على المكدس. يُعتبر المفسر القائم على المكدس سهل التنفيذ والتحكم، ولا يتطلب بيئة أجهزة متقدمة، مما يجعله مناسبًا لمشاهد blockchain. في الوقت نفسه، مقارنةً بمفسر قائم على السجلات، فإن المفسر القائم على المكدس يسهل التحكم والكشف بين المتغيرات عند النسخ والتحريك.
تكون حالة تشغيل برنامج Move رباعية الأبعاد ⟨C, M, G, S⟩، وتتكون من مكدس الاستدعاء (C)، والذاكرة (M)، والمتغيرات العالمية (G)، وعوامل التشغيل (S). كما يحتفظ المكدس بجدول دوال لتحليل التعليمات التي تحتوي على جسم الدالة.
تحتوي مكدس الاستدعاء على جميع معلومات السياق ورقم التعليمات لتنفيذ العملية. يتم إنشاء كائن مكدس استدعاء جديد عند تنفيذ تعليمات Call، وتخزين معاملات الاستدعاء، ثم تنفيذ تعليمات العقد الجديدة. عند مواجهة تعليمات فرعية، يتم إجراء الانتقال الثابت داخل العملية. هذا التصميم يتجنب التوزيع الديناميكي، ويعزز عدم قابلية تغيير استدعاءات الدوال، مما يمنع إمكانية إعادة الدخول.
يعمل MoveVM على فصل تخزين البيانات ومنطق تنفيذ المكدس (، وهو أكبر اختلاف عن EVM. في MoveVM، يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ) بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الإذن والموارد الإلزامية. على الرغم من أن هذا التصميم يضحي ببعض المرونة، إلا أنه حقق تحسينًا كبيرًا في الأمان وكفاءة التنفيذ.
3. نقل البروفر
Move Prover هي أداة للتحقق الرسمي تعتمد على الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية، وبالتالي تقليل مخاطر المعاملات.
تستخدم Move Prover خوارزمية التحقق الاستدلالي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، والتأكد من تطابقه مع السلوك المتوقع. يساعد ذلك في ضمان صحة البرنامج، ويقلل من عبء العمل للاختبارات اليدوية.
تدفق عمل Move Prover هو كما يلي:
استلام ملف Move كمصدر للإدخال، يجب أن يحتوي هذا الملف على معايير إدخال البرنامج.
نقل المحلل من المصدر لاستخراج المواصفات.
يقوم مترجم Move بتحويل الملفات المصدرية إلى بايت كود، ويحولها مع النظام القياسي إلى نموذج كائنات المدققين.
تم ترجمة هذا النموذج إلى لغة Boogie المتوسطة.
نظام Boogie للتحقق من "توليد شروط التحقق" للإدخال.
تمرير شروط التحقق إلى محلل Z3 لإجراء الفحص.
إذا تم اعتماد المعايير، يتم التحقق من الصحة؛ وإلا يتم إنشاء تقرير تشخيصي.
لوصف نظام المواصفات، تستخدم Move لغة مواصفات Move، وهي مجموعة فرعية من لغة Move، حيث تقدم دعمًا لوصف سلوك صحة البرنامج بشكل ثابت. يمكن أن تكون لغة مواصفات Move مستقلة كملف مخصص للتوصيف، مما يسمح بفصل كود الأعمال وكود التحقق الرسمي.
Move Prover هي أداة مفيدة جدًا يمكن أن تساعد المطورين في ضمان صحة العقود الذكية. إنها تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. يساعد ذلك في تقليل مخاطر المعاملات، مما يمنح المطورين مزيدًا من الثقة في نشر العقود الذكية في بيئة الإنتاج.
4. الملخص
تتمتع لغة Move بتصميم أمان ممتاز، حيث توفر اعتبارات شاملة من حيث خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. في خصائص اللغة، تم التضحية ببعض المرونة، مع فرض فحص الأنواع المنطقية والخطية، مما يسهل الأتمتة والتحقق الآمن أثناء الفحص التجميعي والتحقق الرسمي. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى بشكل أفضل مع احتياجات إدارة أمان الأصول على blockchain.
على المستوى اللغوي، يمكن أن تتجنب Move بشكل فعال الثغرات الشائعة مثل إعادة الدخول، والانفجار، وإدخال Call/DeleGateCall في EVM. لكن لا تزال هناك مشاكل تتعلق بالتحقق، ومنطق الشيفرة، وانفجار الهياكل ذات الأعداد الكبيرة التي تحتاج إلى اهتمام خاص من المطورين. على الرغم من أن Move Prover قوي، إلا أنه قد لا يعمل بشكل فعال عندما يتم إغفال الفكرة العامة.
على الرغم من أن لغة Move تأخذ في الاعتبار الكثير من الأمور الأمنية للمبرمجين، إلا أنه لا توجد لغة أو برامج آمنة تمامًا. يُنصح مطوري العقود الذكية بلغة Move باستخدام خدمات تدقيق من شركات أمان طرف ثالث، وتفويض كتابة والتحقق من جزء specification من الكود لشركات الأمان الطرف الثالث، لزيادة أمان العقود بشكل أكبر.
This page may contain third-party content, which is provided for information purposes only (not representations/warranties) and should not be considered as an endorsement of its views by Gate, nor as financial or professional advice. See Disclaimer for details.
تحليل العمق لأمان لغة Move: معيار جديد لتطوير العقود الذكية
تحليل أمان لغة Move: ثائر لغة العقود الذكية
لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم تصميمها مع الأخذ في الاعتبار العديد من مشكلات الأمان المتعلقة بالـ blockchain والعقود الذكية، واستندت إلى تصميم الأمان في لغة RUST. كجيل جديد من لغات العقود الذكية التي تتميز بالأمان، ما مدى أمانها؟ هل يمكنها تجنب التهديدات الأمنية الشائعة في الآلات الافتراضية للعقود مثل EVM وWASM على مستوى اللغة أو من خلال الآليات ذات الصلة؟ هل لديها مشكلات أمان فريدة من نوعها؟
ستتناول هذه المقالة قضايا أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية، آلية التشغيل وأدوات التحقق.
1. ميزات الأمان في لغة Move
تختلف لغة Move عن العديد من لغات البرمجة الحالية، حيث تم تصميمها لدعم كتابة البرامج التي تتفاعل بأمان مع الشيفرات غير الموثوقة، وكذلك لدعم التحقق الثابت. تتمتع Move بهذه الميزات الأمنية لأنها تتخلى عن المنطق غير الخطي القائم على المرونة، ولا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنماط العامة، التخزين العالمي، الموارد، وغيرها لتحقيق أنماط برمجة بديلة. على سبيل المثال، تتجاهل Move ميزات التوزيع الديناميكي والاستدعاء التكراري، وهي ميزات تؤدي في لغات العقود الذكية الأخرى إلى ثغرات إعادة إدخال مكلفة.
تشمل الخصائص الأمنية الرئيسية لـ Move:
模块(Module): كل وحدة Move تتكون من سلسلة من أنواع الهياكل وتعريفات العمليات. يمكن للوحدات استيراد تعريفات الأنواع واستدعاء العمليات المعلن عنها في وحدات أخرى.
结构体(Structs): يمكن تعريفها على أنها نوع من الموارد، مما يعني أنه يمكن تخزينها في التخزين الدائم للمفاتيح/القيم العالمية.
过程(Function): تعريف المنطق التجاري للعقود.
التخزين العالمي: يسمح لبرامج Move بتخزين البيانات الدائمة، والتي يمكن قراءتها/كتابتها برمجياً فقط من قبل الوحدة التي تمتلكها.
فحص الثوابت: يمكن تعريف الثوابت لفحصها بشكل ثابت، مما يدل على الحفاظ على الموارد في النظام.
مُحقق بايت كود: يقوم بالتحقق من الأنواع الآمنة والتسوية لبايت كود، ويفرض قواعد إنشاء الموارد وتدميرها والوصول إليها.
من خلال هذه الميزات، يمكن لـ Move ضمان مستوى عالٍ من الأمان أثناء وقت الترجمة. بعد ذلك، سنحلل آلية تشغيل Move، لنرى كيف يضمن MoveVM أمان وقت التشغيل.
2. آلية تشغيل Move
تعمل برامج Move في بيئة افتراضية، ولا يمكن الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يسمح لـ Move بالعمل بأمان في بيئات غير موثوقة، دون أن تتعرض للتلف أو الإساءة.
تتم عملية تنفيذ برنامج Move على المكدس. يتم تقسيم التخزين العالمي إلى جزئين: الذاكرة ( الكومة ) ومتغيرات عالمية ( المكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكنها تخزين مؤشرات تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، لكن طريقة الفهرسة تختلف عن الذاكرة.
تُنفذ تعليمات بايت كود Move في مفسر قائم على المكدس. يُعتبر المفسر القائم على المكدس سهل التنفيذ والتحكم، ولا يتطلب بيئة أجهزة متقدمة، مما يجعله مناسبًا لمشاهد blockchain. في الوقت نفسه، مقارنةً بمفسر قائم على السجلات، فإن المفسر القائم على المكدس يسهل التحكم والكشف بين المتغيرات عند النسخ والتحريك.
تكون حالة تشغيل برنامج Move رباعية الأبعاد ⟨C, M, G, S⟩، وتتكون من مكدس الاستدعاء (C)، والذاكرة (M)، والمتغيرات العالمية (G)، وعوامل التشغيل (S). كما يحتفظ المكدس بجدول دوال لتحليل التعليمات التي تحتوي على جسم الدالة.
تحتوي مكدس الاستدعاء على جميع معلومات السياق ورقم التعليمات لتنفيذ العملية. يتم إنشاء كائن مكدس استدعاء جديد عند تنفيذ تعليمات Call، وتخزين معاملات الاستدعاء، ثم تنفيذ تعليمات العقد الجديدة. عند مواجهة تعليمات فرعية، يتم إجراء الانتقال الثابت داخل العملية. هذا التصميم يتجنب التوزيع الديناميكي، ويعزز عدم قابلية تغيير استدعاءات الدوال، مما يمنع إمكانية إعادة الدخول.
يعمل MoveVM على فصل تخزين البيانات ومنطق تنفيذ المكدس (، وهو أكبر اختلاف عن EVM. في MoveVM، يتم تخزين الموارد تحت عنوان حساب حالة المستخدم ) بشكل مستقل، ويجب أن تتوافق استدعاءات البرنامج مع قواعد الإذن والموارد الإلزامية. على الرغم من أن هذا التصميم يضحي ببعض المرونة، إلا أنه حقق تحسينًا كبيرًا في الأمان وكفاءة التنفيذ.
3. نقل البروفر
Move Prover هي أداة للتحقق الرسمي تعتمد على الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية، وبالتالي تقليل مخاطر المعاملات.
تستخدم Move Prover خوارزمية التحقق الاستدلالي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، والتأكد من تطابقه مع السلوك المتوقع. يساعد ذلك في ضمان صحة البرنامج، ويقلل من عبء العمل للاختبارات اليدوية.
تدفق عمل Move Prover هو كما يلي:
لوصف نظام المواصفات، تستخدم Move لغة مواصفات Move، وهي مجموعة فرعية من لغة Move، حيث تقدم دعمًا لوصف سلوك صحة البرنامج بشكل ثابت. يمكن أن تكون لغة مواصفات Move مستقلة كملف مخصص للتوصيف، مما يسمح بفصل كود الأعمال وكود التحقق الرسمي.
Move Prover هي أداة مفيدة جدًا يمكن أن تساعد المطورين في ضمان صحة العقود الذكية. إنها تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. يساعد ذلك في تقليل مخاطر المعاملات، مما يمنح المطورين مزيدًا من الثقة في نشر العقود الذكية في بيئة الإنتاج.
4. الملخص
تتمتع لغة Move بتصميم أمان ممتاز، حيث توفر اعتبارات شاملة من حيث خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. في خصائص اللغة، تم التضحية ببعض المرونة، مع فرض فحص الأنواع المنطقية والخطية، مما يسهل الأتمتة والتحقق الآمن أثناء الفحص التجميعي والتحقق الرسمي. تصميم MoveVM يفصل الحالة عن المنطق، مما يتماشى بشكل أفضل مع احتياجات إدارة أمان الأصول على blockchain.
على المستوى اللغوي، يمكن أن تتجنب Move بشكل فعال الثغرات الشائعة مثل إعادة الدخول، والانفجار، وإدخال Call/DeleGateCall في EVM. لكن لا تزال هناك مشاكل تتعلق بالتحقق، ومنطق الشيفرة، وانفجار الهياكل ذات الأعداد الكبيرة التي تحتاج إلى اهتمام خاص من المطورين. على الرغم من أن Move Prover قوي، إلا أنه قد لا يعمل بشكل فعال عندما يتم إغفال الفكرة العامة.
على الرغم من أن لغة Move تأخذ في الاعتبار الكثير من الأمور الأمنية للمبرمجين، إلا أنه لا توجد لغة أو برامج آمنة تمامًا. يُنصح مطوري العقود الذكية بلغة Move باستخدام خدمات تدقيق من شركات أمان طرف ثالث، وتفويض كتابة والتحقق من جزء specification من الكود لشركات الأمان الطرف الثالث، لزيادة أمان العقود بشكل أكبر.