تحليل أمان لغة Move

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

1. ميزات الأمان في لغة Move

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

إليك مثال بسيط لتنفيذ الرمز المميز:

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

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

بنية Coin تحتوي على مفتاح { القيمة: u64 }
هيكل Info يحتوي على مفتاح { total_supply: u64 }

ثابت للجميع a: عنوان حيث يوجد<coin>(a):
    عالمي<coin>(a).value <=<info>(ADMIN).total_supply عالمي.

initialize(account المرح العام: &signer) {
    assert!(signer::address_of(account) == ADMIN, 0);
    انتقل إلى ( الحساب، المعلومات { إجمالي العرض: 0 } );
}

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

value_mut(coin المرح العام: & Coin): &MUT U64 {
    &MUT coin.value  
}

}

تظهر هذه العينة بعض الميزات المهمة للغة Move:

1. الت modularization: يتم تنظيم الشيفرة في وحدات، ويمكن استيراد الأنواع والدوال من وحدات أخرى.

2. الهيكل: استخدم struct لتعريف بنية البيانات ، يمكنك إضافة علامات القدرة مثل المفتاح.

3. التخزين العالمي: إدارة الحالة العالمية من خلال عمليات مثل move_to و borrow_global_mut.

4. أمان الموارد: ضمان الاستخدام الآمن للموارد من خلال نظام القدرات وأنواع الخطية.

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

تضمن لغة Move الأمان في وقت الترجمة من خلال مدقق بايت كود وفحص الثوابت:

• مُحقق بايت كود: يتحقق من صحة الهيكل، ومنطق العملية، والأخطاء في الربط، وما إلى ذلك.

• فحص الثوابت: التحقق مما إذا كانت حالة البرنامج تستوفي قواعد الثوابت المعرفة مسبقًا.

2. آلية عمل Move

تُنفذ برامج Move في الآلة الافتراضية، وتتكون حالة التشغيل من كومة الاستدعاء، والذاكرة، والمتغيرات العالمية، وكومة العمليات. تشمل الخصائص الرئيسية ما يلي:

1. تنفيذ في بيئة محكومة، لا يمكن الوصول مباشرة إلى ذاكرة النظام.

2. استخدام مفسر قائم على المكدس، مما يسهل التنفيذ والتحكم.

3. الموارد يمكن نقلها فقط، ولا يمكن نسخها.

4. سجل مكدس الاستدعاء سياق التنفيذ ، يدعم الانتقال الثابت.

5. فصل منطق تخزين البيانات واستدعائها، مما يزيد من الأمان وكفاءة التنفيذ.

يمنع هذا التصميم بعض المشكلات الأمنية الشائعة، مثل هجمات إعادة الدخول.

3. نقل المدقق

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

1. استلام كود مصدر Move والمواصفات كمدخل.

2. تحليل المصدر، استخراج المعايير.

3. تحويل الكود والمواصفات إلى نموذج كائن المُحقق.

4. توليد كود لغة Boogie الوسيطة.

5. استخدام مُحلل Z3 SMT للتحقق مما إذا كانت المواصفات صحيحة.

6. إنشاء تقرير تشخيصي، يشير إلى المشكلات المحتملة.

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

ملخص

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