تحليل أمان لغة Move: المحول للعقود الذكية

لغة Move هي لغة عقود ذكية يمكن تجميعها وتشغيلها في بيئة blockchain التي تنفذ MoveVM. كجيل جديد من لغات العقود الذكية التي تركز على الأمان، كيف هي أمانها؟ هل يمكنها تجنب التهديدات الأمنية الشائعة في آلات العقود الافتراضية مثل EVM وWASM؟ ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: خصائص اللغة، آلية التشغيل، وأدوات التحقق.

1. الخصائص الأمنية للغة Move

على عكس العديد من لغات البرمجة الحالية، تم تصميم لغة Move لدعم التفاعل الآمن مع الشيفرات غير الموثوق بها، وكذلك دعم التحقق الثابت. تخلت Move عن المنطق غير الخطي المستند إلى المرونة، ولا تدعم التوزيع الديناميكي أو الاستدعاءات الخارجية المتكررة، بل تستخدم مفاهيم مثل الجينات، التخزين العالمي، والموارد لتحقيق نماذج برمجة بديلة.

إليك مثال على تنفيذ أصل توكن بلغة Move:

تحرك الوحدة 0x1::TestCoin { استخدم 0x1::signer;

const ADMIN: العنوان = @0x1;

هيكل Coin لديه مفتاح، متجر { 
    القيمة: u64
}

هيكل المعلومات لديه مفتاح {
    total_supply: U64  
}

وحدة المواصفات {
    ثابت forall addr: العنوان حيث يوجد<coin>(addr):
        (ADMIN).total_supply > العالمية<info>= العالمية<coin>(addr).value;
}

initialize(account المرح العام: &signer) {
    assert!(signer::address_of(account) == ADMIN, 1);
    move_to(account, معلومات { total_supply: 0 })
}

mint(account المرح العام: & الموقع, المبلغ: u64): عملة {
    assert!(signer::address_of(account) == ADMIN, 1);
    دع عملة = عملة { القيمة: المبلغ } ؛
    دع المعلومات = borrow_global_mut<info>(ADMIN) ؛
    info.total_supply = info.total_supply + المبلغ ؛
    عملة
}

value(coin المرح العام: &Coin): U64 {
    قيمة العملة  
}

}

توضح هذه العينة بعض الميزات الأمنية الرئيسية للغة Move:

1. التوصيف: كل وحدة Move تتكون من نوع هيكلي وتعريف عملية، ويمكن استيراد تعريفات الأنواع من وحدات أخرى واستدعاء عمليات وحدات أخرى.

2. نوع المورد: يتم تعريفه كنوع مورد بواسطة بنية محددة بواسطة has key أو store، ويمكن تخزينه في تخزين القيمة المفتاحية العالمية الدائم.

3. التخزين العالمي: يسمح لبرنامج Move بتخزين البيانات الدائمة، ويمكن قراءتها وكتابتها برمجيًا فقط من قبل الوحدة المالكة، ولكن يمكن للوحدات الأخرى الاطلاع عليها المخزنة في السجل العام.

4. التحكم في الوصول: يمكن تحقيق التحكم في الوصول إلى العمليات الرئيسية من خلال طرق مثل التأكيد.

5. تقليص الثوابت: يمكن تعريف الثوابت التي يتم فحصها بشكل ثابت، لاستخدامها في التحقق الرسمي.

6. تحقق من التعليمات البرمجية: يشمل أنواع الأمان والتحقق الخطي، لمنع العمليات غير القانونية على أنواع الموارد.

تضمن هذه الميزات معًا أمان لغة Move أثناء مرحلة الترجمة.

2. آلية تشغيل Move

تعمل برامج Move في بيئة افتراضية، ولا يمكنها الوصول إلى الذاكرة النظامية، ويمكن تشغيلها بأمان في بيئات غير موثوقة.

يتم تنفيذ برنامج Move على المكدس، وينقسم التخزين العالمي إلى الذاكرة ( والمكدس ) والمتغيرات العالمية (. لا يمكن للذاكرة تخزين مؤشرات إلى وحدات الذاكرة، بينما تُستخدم المتغيرات العالمية لتخزين مؤشرات إلى وحدات الذاكرة.

تُنفذ تعليمات بايت كود Move في مفسر قائم على المكدس، مما يسهل التنفيذ والتحكم، وهي مناسبة لسيناريوهات blockchain. يمكن تحريك القيم من نوع المورد بطريقة مدمرة فقط.

حالة تشغيل برنامج Move هي رباعي الأبعاد ⟨C، M، G، S⟩، بما في ذلك مكدس الاستدعاء، الذاكرة، المتغيرات العالمية، والعمليات. خلال التنفيذ، يقوم استدعاء الوظائف بإنشاء كائن مكدس استدعاء جديد، وتقوم تعليمات التفرع بإجراء قفزات ثابتة، مما يتجنب التوزيع الديناميكي.

يعمل MoveVM على فصل تخزين البيانات ودفتر الاستدعاءات، وهو مختلف عن تصميم EVM. على الرغم من أن هذا التصميم يضحي بالمرونة، إلا أنه يعزز الأمان وكفاءة التنفيذ.

![تحليل الأمان لـ Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(

3. نقل المبرهن

Move Prover هي أداة للتحقق الرسمي تستند إلى الاستدلال، تستخدم لغة رسمية لوصف سلوك البرنامج، وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات.

هيكل Move Prover كما يلي:

1. استقبال ملف Move المصدر المدخل، بما في ذلك مواصفات البرنامج.
2. يقوم المحلل باستخراج المواصفات، بينما يقوم المترجم بتحويل الشيفرة المصدرية إلى بايت كود.
3. تحويل إلى نموذج كائن المدقق.
4. ترجم إلى لغة Boogie الوسيطة.
5. نظام Boogie يقوم بإنشاء شروط التحقق.
6. يتحقق محلل Z3 من أن صيغة SMT غير قابلة للإرضاء.
7. إنشاء تقرير تشخيصي واستعادته إلى أخطاء مستوى الشيفرة المصدرية.

تستخدم Move لغة المواصفات Move لوصف المعايير، وهي مجموعة فرعية من لغة Move.

Move Prover هي أداة مفيدة تساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات.

![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-372ff914a241634ca57784dc9685a03d.webp(

ملخص

تتميز لغة Move بتصميم أمان ممتاز، حيث تم مراعاة جوانب متعددة من خصائص اللغة، وتنفيذ الآلة الافتراضية، وأدوات الأمان. لقد sacrificed بعض المرونة لتعزيز فحص الأنواع والمنطق الخطي، مما يسهل فحص الترجمة والتحقق الرسمي. تفصل MoveVM الحالة عن المنطق، مما يتماشى بشكل أفضل مع احتياجات إدارة أمان الأصول blockchain.

تتمكن لغة Move من تجنب الثغرات الشائعة في EVM مثل إعادة الدخول، والتجاوز، والحقن، ولكن لا يزال يتعين على المطورين الانتباه لمشاكل مثل التحقق من الهوية، والمنطق، وتجاوز الأعداد الكبيرة. على الرغم من أن Move تأخذ في الاعتبار جوانب الأمان بعناية، إلا أنه يُوصى باستخدام خدمات تدقيق الشركات الأمنية التابعة لجهات خارجية، وتفويض كتابة الشيفرة البرمجية والتحقق منها إلى فرق الأمان المتخصصة.

![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-f7cd11fef1c66709b219e1a1e8d2e4da.webp(