لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم إنشاؤها مع مراعاة العديد من القضايا الأمنية المتعلقة بالبلوكشين والعقود الذكية، واستوحت بعض تصميماتها الأمنية من لغة RUST. كجيل جديد من لغات العقود الذكية التي تركز على الأمان، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة لآلات العقود الافتراضية مثل EVM وWASM على مستوى اللغة أو من خلال آليات ذات صلة؟ هل توجد بها مشكلات أمان خاصة بها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية، آلية التشغيل، وأدوات التحقق.
1. الميزات الأمنية للغة Move
كتابة الشيفرة الصحيحة أمر صعب، حتى بعد العديد من الاختبارات، لا يمكن ضمان أن الشيفرة خالية تمامًا من الثغرات. يصبح من الأصعب كتابة الشيفرة التي تحافظ على الخصائص الأمنية الأساسية عند التفاعل مع الشيفرة غير الموثوقة. هناك العديد من التقنيات التي يمكن استخدامها لتنفيذ الأمان في وقت التشغيل، مثل الصناديق الرملية، وعزل العمليات، وقفل الكائنات وأنماط البرمجة الأخرى؛ كما يمكن تحديد الأمان الثابت في وقت الترجمة، مثل فرض الأنواع الثابتة أو فحص التأكيد.
أحيانًا يمكن الاستفادة من أدوات التحليل الدلالي والتحليل الثابت لضمان توافق الكود مع قواعد الأمان، حتى عند التفاعل مع كود غير موثوق، يمكن الحفاظ على بعض شروط المنطق القابلة للإثبات.
تبدو هذه الحلول جيدة، حيث يمكن أن تتجنب تكاليف التشغيل وتكتشف المشكلات الأمنية مبكرا. ولكن للأسف، فإن الأمان الذي تحققه لغات البرمجة من خلال هذه الطرق محدود للغاية، وذلك لسببين رئيسيين: أولاً، غالباً ما تحتوي على خصائص تجعل من المستحيل استخدام أدوات التحليل الثابت، مثل التشغيل الديناميكي، والمشاركة المتغيرة، والانعكاس، وغيرها من المنطق غير الخطي، مما ينتهك قواعد الثوابت الأمنية ويوفر للهاكرز مجموعة واسعة من نقاط الضعف. ثانياً، من الصعب على معظم لغات البرمجة أن تتمدد باستخدام أدوات ثابتة تتعلق بالأمان أو لغة معيارية قوية التعبير. على الرغم من أن هذين النوعين من التمديد مهمان، إلا أنه يمكن تحديدهما مسبقاً.
على عكس العديد من لغات البرمجة الحالية، تم تصميم لغة 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, 0);
نقل إلى ( حساب، معلومات { إجمالي العرض: 0 } )
}
public fun mint(account: &signer, amount: u64): معلومات اكتساب العملة {
assert!(signer::address_of(account) == ADMIN, 0);
دع العرض = borrow_global_mut<info>(ADMIN) ؛
supply.total_supply = supply.total_supply + المبلغ ؛
العملة { القيمة: المبلغ }
}
value(coin المرح العام: &Coin): U64 {
قيمة العملة
}
value_mut(coin المرح العام: & Coin): &MUT U64 {
&MUT coin.value
}
}
a) 模块(Module): كل وحدة Move تتكون من سلسلة من أنواع الهيكل والتعريفات العملية. يمكن للوحدة استيراد تعريفات الأنواع واستدعاء العمليات المعلنة في وحدات أخرى. يبدأ الاسم المؤهل بالكامل للوحدة بعنوان حساب 16 بايت الذي يخزن رمز الوحدة. يعمل عنوان الحساب كنطاق لتفريق الوحدات ذات الأسماء المتشابهة.
b) الهيكل(Structs): يحدد هذا الموديل هيكلين Coin و Info. يمثل Coin الرموز المخصصة للمستخدمين، ويسجل Info إجمالي عدد الرموز. تم تعريف الهيكلين كنوع من الموارد، ويمكن تخزينهما في تخزين المفتاح/القيمة العالمي الدائم.
c) العملية(function): الكود يعرف عملية تهيئة، عملية أمان وعملية غير آمنة. يجب استدعاء عملية initialize قبل إنشاء Coin، لتعيين قيمة total_supply من Info singleton إلى صفر. signer هو نوع خاص، يمثل المستخدم الذي تم التحقق منه بواسطة المنطق الخارجي Move. يضمن التأكيد أنه يمكن فقط للحساب الإداري المحدد استدعاء هذه العملية. تسمح عملية mint للمسؤول بإنشاء رموز جديدة، بنفس طريقة التحكم في الوصول. تقبل عملية value_mut مرجع Coin القابل للتغيير، وتعيد مرجعًا قابلًا للتغيير للحقل value.
إن هيكل العقد مشابه للغات العقود الذكية الأخرى، لكن نوع الموارد والتخزين العالمي هما الآليتين الرئيسيتين لحماية التخزين والموارد في لغة Move.
تسمح التخزين العالمي لبرامج Move بتخزين البيانات الدائمة، هذه البيانات يمكن قراءتها وكتابتها برمجيًا فقط من قِبل الوحدة التي تمتلكها، ولكنها مخزنة في دفتر حسابات عام يمكن لمستخدمي وحدات أخرى مشاهدتها. يتكون كل مفتاح في التخزين العالمي من اسم نوع مؤهل بالكامل وعنوان حساب يخزن قيمة هذا النوع. على الرغم من أن التخزين العالمي مشترك بين جميع الوحدات، إلا أن كل وحدة لها حقوق قراءة وكتابة حصرية للمفتاح الذي أعلنته.
يمكن أن تحتوي الوحدة النمطية التي تُعلن عن نوع المورد على:
• نشر القيمة في التخزين العالمي باستخدام أمر move_to
• حذف القيمة من التخزين العالمي باستخدام الأمر move_from
• الحصول على مرجع لقيمة في التخزين العالمي من خلال تعليمات borrow_global_mut
يمكن للوحدات فرض قيود على التخزين العالمي الذي تتحكم فيه. على سبيل المثال، التأكد من أنه يمكن فقط لعنوان حساب ADMIN الاحتفاظ بهيكل نوع Info، من خلال تعريف عملية initialize التي يتم تنفيذها على نوع Info باستخدام move_to، وفرض شروط مسبقة لاستدعاء move_to على عنوان ADMIN.
فيما يلي آليتان لضمان أمان كود الوحدة من خلال الفحص الثابت: تقليل الثوابت ومدقق بايت الكود.
a) فحص الثوابت ( فحص القواعد ): السطر 10 من الوحدة يشير إلى الثابت الذي يتم فحصه بشكل ثابت - يجب أن تكون مجموع قيم جميع كائنات Coin في النظام مساويًا للحقل total_value في كائن Info المخزن في عنوان ADMIN. الثابت هو مصطلح في التحقق الرسمي، يشير إلى الحفاظ على الحالة. هذه الخاصية الحافظة تنطبق على جميع العملاء المحتملين للوحدة.
b) مدقق التعليمات البرمجية: النوع الأمني والتسلسل الخطي هما النطاق الرئيسي للتحقق في مدقق التعليمات البرمجية. على الرغم من أن الوحدات الأخرى لا يمكنها الوصول إلى وحدة التخزين العالمية التي تتحكم بها 0x1::TestCoin::Coin، إلا أنه يمكن استخدامها في إعلانات العمليات والهياكل الخاصة بها.
يحتوي Move على محقق بايت كود ( الذي ينفذ نظام الأنواع على مستوى بايت كود )، مما يسمح لمالك الوحدة بمنع النتائج غير المرغوب فيها. فقط الوحدات التي تعلن عن نوع الهيكل Coin يمكنها:
• إنشاء قيمة من نوع Coin
• "فك حزمة" قيمة نوع Coin إلى حقولها المكونة
• الحصول على مرجع لحقل Coin من خلال الاقتراض المتغير أو غير المتغير بأسلوب rust
تفرض المدقق أيضًا أن تكون الهياكل الافتراضية خطية، لضمان منع النسخ والتدمير خارج الوحدة التي تم إعلان الهيكل فيها بشكل خطي. في الوقت نفسه، سيقوم المدقق أيضًا بإجراء فحوصات إلزامية لبعض أنواع مشاكل الذاكرة الشائعة.
تشمل عملية الكشف ثلاث فئات رئيسية:
فحص صلاحية الهيكل: ضمان سلامة البايت كود، اكتشاف الأخطاء، الاستشهادات غير القانونية، الكيانات المكررة والأنواع غير القانونية للتوقيع وغيرها
الكشف عن دلالات منطق العملية: يشمل أخطاء نوع المعامل، فهرس الحلقة، الفهرس الفارغ وتعريف المتغيرات المكررة وغيرها.
حدث خطأ عند الربط، استدعاء داخلي غير قانوني، أو عدم تطابق في عملية إعلان الربط والتعريف
يقوم المدقق أولاً بإنشاء CFG( لرسم تدفق التحكم )، ثم يتحقق من نطاق وصول المستدعي في المكدس، لضمان عدم قدرة المستدعي للعقد على الوصول إلى مساحة المكدس الخاصة بالمدعو. وفي الوقت نفسه، للتحقق من النوع، يحتفظ كل مكدس قيمة بمكدس نوع مقابله.
التالي هو فحص الموارد وفحص الاقتباسات. يركز فحص الموارد بشكل أساسي على قيود مثل عدم إمكانية الإنفاق المزدوج، وعدم القابلية للتدمير، وضرورة وجود ملكية. يجمع فحص الاقتباسات بين التحليل الديناميكي والثابت، ويستخدم آلية فحص الاقتراض المشابهة لنظام نوع روست.
أخيرًا، هناك فحص للروابط، حيث يجب التحقق مرة أخرى مما إذا كانت كائنات الروابط والبيانات متطابقة، بالإضافة إلى التحكم في الوصول للعملية.
آلية تشغيل Move
أولاً، يعمل برنامج Move في آلة افتراضية، ولا يمكنه الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يسمح لـ Move بالعمل بأمان في بيئات غير موثوقة، دون أن يتم تدميره أو إساءة استخدامه.
ثانيًا، يتم تنفيذ برنامج Move على المكدس. يتم تقسيم التخزين العالمي إلى ذاكرة ( كومة ) ومتغيرات عالمية ( مكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكن لوحداتها تخزين مؤشرات تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، ولكن طريقة الفهرسة تختلف. عند الوصول إلى المتغيرات العالمية، يوفر الكود العنوان والنوع المرتبط بذلك العنوان. تُبسط هذه التقسيمات العمليات، مما يجعل دلالة لغة Move أكثر سهولة في الصياغة.
تُنفذ تعليمات بايت كود Move في المفسر القائم على المكدس. من السهل تنفيذ والتحكم في الآلة الافتراضية القائمة على المكدس، كما أن لديها متطلبات أقل على البيئة المادية، مما يجعلها مناسبة لسيناريوهات blockchain. بالمقارنة مع المفسر القائم على السجلات، فإن المفسر القائم على المكدس يجعل من السهل التحكم في النسخ و النقل بين المتغيرات واكتشافها.
في Move، يمكن أن يتم تدمير القيم المعرفة كموارد فقط من خلال التحريك المدمر ( مما يجعل موقع التخزين الذي تم حفظ تلك القيمة فيه غير صالح )، لكن بعض القيم ( مثل الأعداد الصحيحة ) يمكن نسخها.
عندما يعمل برنامج Move على المكدس، تكون حالته رباعية الأبعاد ⟨C, M, G, S⟩، والتي تتكون من مكدس الاستدعاء (C)، الذاكرة (M)، المتغيرات العالمية (G) وOperands (S). كما يحتفظ المكدس بجدول الدوال ( module نفسه ) لتحليل التعليمات التي تحتوي على جسم الدالة.
تحتوي مكدس الاستدعاء على جميع معلومات السياق وتعليمات تنفيذ العملية. عند تنفيذ تعليمات Call، يتم إنشاء كائن مكدس استدعاء جديد، ويتم تخزين معلمات الاستدعاء في الذاكرة والمتغيرات العالمية، ثم يقوم المفسر بتنفيذ تعليمات العقد الجديد. عند مواجهة تعليمات الفرع، يحدث قفز ثابت داخل هذه العملية. تعتمد العملية داخل الوحدة على عدم وجود حلقات، بالإضافة إلى عدم وجود تخصيص ديناميكي داخل الوحدة، مما يعزز عدم قابلية تغيير استدعاءات الدوال خلال فترة التنفيذ: يجب أن تكون إطارات استدعاء العملية متجاورة، مما يتجنب إمكانية إعادة الدخول. تنتهي عملية الاستدعاء عند تنفيذ return، ويتم وضع قيمة الإرجاع في قمة المكدس.
من خلال دراسة كود MoveVM، يتضح أن MoveVM يفصل بين تخزين البيانات ومنطق عملية استدعاء المكدس (، وهو أكبر اختلاف عن EVM. في EVM، يتطلب تنفيذ توكن ERC20 كتابة المنطق في عقد واحد وتسجيل حالة كل مستخدم، بينما في MoveVM، يتم تخزين حالة المستخدم ) للموارد تحت عنوان الحساب ( بشكل مستقل، ويجب أن يتوافق استدعاء البرنامج مع قواعد الإذن والقواعد الإلزامية المتعلقة بالموارد. على الرغم من أن هذا يتطلب بعض التضحية بالمرونة، إلا أنه يساعد في تحقيق تحسين كبير في الأمان وكفاءة التنفيذ ) لتحقيق تنفيذ متزامن (.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
) 3. نقل المدقق
أخيرًا، دعونا نتعرف على أداة التدقيق الآلي المساعدة التي تقدمها Move، وهي Move prover.
Move Prover هي أداة للتحقق الرسمي المستند إلى الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. باختصار، فإن التحقق الرسمي هو استخدام طرق رياضية لإثبات أن النظام خالٍ من الأخطاء.
تستند خوارزميات التحقق الآلي للبرامج السائدة حاليًا إلى محللات نظرية الإرضاء SMT solver###. في الواقع، SMT solver هو محلل صيغ. تقوم خوارزميات التحقق البرمجي العليا بتقسيم أهداف التحقق إلى صيغ، وتقديمها إلى SMT solver لحلها، بناءً على النتائج، يتم تحليلها بشكل أكبر، وفي النهاية، يتم الإبلاغ عن تحقق الهدف أو اكتشاف ضد المثال.
الخوارزمية الأساسية للتحقق هي التحقق الاستنتاجي (deductive verification)، وهناك خوارزميات تحقق أخرى مثل فحص النماذج المحدودة، طريقة الاستقراء k، التجريد القائم على القضايا والتجريد القائم على المسار وغيرها.
يستخدم Move Prover خوارزمية التحقق الاستدلالي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. وهذا يعني أن Move Prover يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن توافقه مع السلوك المتوقع. وهذا يساعد في ضمان صحة البرنامج وتقليل عبء العمل على الاختبارات اليدوية.
الهيكل العام لـ Move Prover كما يلي:
أولاً، يستقبل Move Prover ملف مصدر Move يحتوي على مواصفات إدخال البرنامج (specification). يقوم Move Parser باستخراج المواصفات من الشيفرة المصدرية. يقوم مترجم Move بترجمة ملف المصدر إلى بايت كود، مع تحويله إلى نموذج كائن المثبت (Prover Object Model).
تمت ترجمة النموذج إلى لغة Boogie الوسيطة. يتم تمرير كود Boogie إلى نظام التحقق من Boogie لإجراء "توليد شروط التحقق". يتم تمرير شروط التحقق إلى حل Z3 (، وهو حل SMT تم تطويره بواسطة Microsoft ).
بعد إدخال VC في Z3، يتحقق المدقق مما إذا كانت شفرة البرنامج SMT المعادلة ( تلبي specification ) أم لا. إذا كان الأمر كذلك، فهذا يعني أن المواصفة صحيحة. خلاف ذلك، يتم إنشاء نموذج يلبي الشروط، وتحويله مرة أخرى إلى تنسيق Boogie لنشر تقرير التشخيص. يتم استعادة تقرير التشخيص إلى أخطاء مستوى الشيفرة المصدرية مشابهة لأخطاء المترجم القياسي.
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تسجيلات الإعجاب 17
أعجبني
17
5
إعادة النشر
مشاركة
تعليق
0/400
SchrodingerAirdrop
· 08-09 21:11
لا تزال الحركة غير آمنة بما فيه الكفاية، ثق بي
شاهد النسخة الأصليةرد0
DataBartender
· 08-07 02:38
مرة أخرى يتحدثون عن الحركة بشكل مبالغ فيه.
شاهد النسخة الأصليةرد0
AirdropHarvester
· 08-07 02:29
حركة؟ يبدو أن الأمر مزعج، من الصعب تعلمه مثل Rust.
شاهد النسخة الأصليةرد0
MoneyBurner
· 08-07 02:28
مرة أخرى تريد خداعي لدخول مركز لرؤية سلسلة الكتل الجديدة، في المرة السابقة خسرت كثيرًا.
شاهد النسخة الأصليةرد0
StableNomad
· 08-07 02:28
همم لغة "آمنة" أخرى... تذكرني بسولانا في عام 2021 بصراحة
تحليل عميق لأمان لغة Move: خصائص اللغة، آلية التشغيل، والتدقيق الآلي
مقدمة
لغة Move هي لغة عقود ذكية يمكن تشغيلها في بيئة blockchain التي تنفذ MoveVM. تم إنشاؤها مع مراعاة العديد من القضايا الأمنية المتعلقة بالبلوكشين والعقود الذكية، واستوحت بعض تصميماتها الأمنية من لغة RUST. كجيل جديد من لغات العقود الذكية التي تركز على الأمان، ما مدى أمان Move؟ هل يمكنها تجنب التهديدات الأمنية الشائعة لآلات العقود الافتراضية مثل EVM وWASM على مستوى اللغة أو من خلال آليات ذات صلة؟ هل توجد بها مشكلات أمان خاصة بها؟
ستتناول هذه المقالة مسألة أمان لغة Move من ثلاثة جوانب: الخصائص اللغوية، آلية التشغيل، وأدوات التحقق.
1. الميزات الأمنية للغة Move
كتابة الشيفرة الصحيحة أمر صعب، حتى بعد العديد من الاختبارات، لا يمكن ضمان أن الشيفرة خالية تمامًا من الثغرات. يصبح من الأصعب كتابة الشيفرة التي تحافظ على الخصائص الأمنية الأساسية عند التفاعل مع الشيفرة غير الموثوقة. هناك العديد من التقنيات التي يمكن استخدامها لتنفيذ الأمان في وقت التشغيل، مثل الصناديق الرملية، وعزل العمليات، وقفل الكائنات وأنماط البرمجة الأخرى؛ كما يمكن تحديد الأمان الثابت في وقت الترجمة، مثل فرض الأنواع الثابتة أو فحص التأكيد.
أحيانًا يمكن الاستفادة من أدوات التحليل الدلالي والتحليل الثابت لضمان توافق الكود مع قواعد الأمان، حتى عند التفاعل مع كود غير موثوق، يمكن الحفاظ على بعض شروط المنطق القابلة للإثبات.
تبدو هذه الحلول جيدة، حيث يمكن أن تتجنب تكاليف التشغيل وتكتشف المشكلات الأمنية مبكرا. ولكن للأسف، فإن الأمان الذي تحققه لغات البرمجة من خلال هذه الطرق محدود للغاية، وذلك لسببين رئيسيين: أولاً، غالباً ما تحتوي على خصائص تجعل من المستحيل استخدام أدوات التحليل الثابت، مثل التشغيل الديناميكي، والمشاركة المتغيرة، والانعكاس، وغيرها من المنطق غير الخطي، مما ينتهك قواعد الثوابت الأمنية ويوفر للهاكرز مجموعة واسعة من نقاط الضعف. ثانياً، من الصعب على معظم لغات البرمجة أن تتمدد باستخدام أدوات ثابتة تتعلق بالأمان أو لغة معيارية قوية التعبير. على الرغم من أن هذين النوعين من التمديد مهمان، إلا أنه يمكن تحديدهما مسبقاً.
على عكس العديد من لغات البرمجة الحالية، تم تصميم لغة Move لدعم كتابة برامج تتفاعل بشكل آمن مع الشفرات غير الموثوقة، كما تدعم التحقق الثابت. تتمتع Move بهذه الخصائص الأمنية لأنها تتخلى عن جميع المنطق غير الخطي المبني على اعتبارات المرونة، ولا تدعم التوزيع الديناميكي، ولا تدعم الاستدعاءات الخارجية التكرارية، بل تستخدم مفاهيم مثل الأنواع العامة، والتخزين العالمي، والموارد لتحقيق بعض أنماط البرمجة البديلة. على سبيل المثال، تتجاهل Move ميزات الجدولة الديناميكية والاستدعاءات التكرارية، وهذه الميزات تسببت في ثغرات إعادة الإدخال المكلفة في لغات العقود الذكية الأخرى.
لفهم ميزات لغة Move بشكل أفضل، دعونا نلقي نظرة على برنامج توضيحي:
تحرك الوحدة 0x1::TestCoin { استخدم 0x1::signer;
}
a) 模块(Module): كل وحدة Move تتكون من سلسلة من أنواع الهيكل والتعريفات العملية. يمكن للوحدة استيراد تعريفات الأنواع واستدعاء العمليات المعلنة في وحدات أخرى. يبدأ الاسم المؤهل بالكامل للوحدة بعنوان حساب 16 بايت الذي يخزن رمز الوحدة. يعمل عنوان الحساب كنطاق لتفريق الوحدات ذات الأسماء المتشابهة.
b) الهيكل(Structs): يحدد هذا الموديل هيكلين Coin و Info. يمثل Coin الرموز المخصصة للمستخدمين، ويسجل Info إجمالي عدد الرموز. تم تعريف الهيكلين كنوع من الموارد، ويمكن تخزينهما في تخزين المفتاح/القيمة العالمي الدائم.
c) العملية(function): الكود يعرف عملية تهيئة، عملية أمان وعملية غير آمنة. يجب استدعاء عملية initialize قبل إنشاء Coin، لتعيين قيمة total_supply من Info singleton إلى صفر. signer هو نوع خاص، يمثل المستخدم الذي تم التحقق منه بواسطة المنطق الخارجي Move. يضمن التأكيد أنه يمكن فقط للحساب الإداري المحدد استدعاء هذه العملية. تسمح عملية mint للمسؤول بإنشاء رموز جديدة، بنفس طريقة التحكم في الوصول. تقبل عملية value_mut مرجع Coin القابل للتغيير، وتعيد مرجعًا قابلًا للتغيير للحقل value.
إن هيكل العقد مشابه للغات العقود الذكية الأخرى، لكن نوع الموارد والتخزين العالمي هما الآليتين الرئيسيتين لحماية التخزين والموارد في لغة Move.
تسمح التخزين العالمي لبرامج Move بتخزين البيانات الدائمة، هذه البيانات يمكن قراءتها وكتابتها برمجيًا فقط من قِبل الوحدة التي تمتلكها، ولكنها مخزنة في دفتر حسابات عام يمكن لمستخدمي وحدات أخرى مشاهدتها. يتكون كل مفتاح في التخزين العالمي من اسم نوع مؤهل بالكامل وعنوان حساب يخزن قيمة هذا النوع. على الرغم من أن التخزين العالمي مشترك بين جميع الوحدات، إلا أن كل وحدة لها حقوق قراءة وكتابة حصرية للمفتاح الذي أعلنته.
يمكن أن تحتوي الوحدة النمطية التي تُعلن عن نوع المورد على: • نشر القيمة في التخزين العالمي باستخدام أمر move_to • حذف القيمة من التخزين العالمي باستخدام الأمر move_from • الحصول على مرجع لقيمة في التخزين العالمي من خلال تعليمات borrow_global_mut
يمكن للوحدات فرض قيود على التخزين العالمي الذي تتحكم فيه. على سبيل المثال، التأكد من أنه يمكن فقط لعنوان حساب ADMIN الاحتفاظ بهيكل نوع Info، من خلال تعريف عملية initialize التي يتم تنفيذها على نوع Info باستخدام move_to، وفرض شروط مسبقة لاستدعاء move_to على عنوان ADMIN.
فيما يلي آليتان لضمان أمان كود الوحدة من خلال الفحص الثابت: تقليل الثوابت ومدقق بايت الكود.
a) فحص الثوابت ( فحص القواعد ): السطر 10 من الوحدة يشير إلى الثابت الذي يتم فحصه بشكل ثابت - يجب أن تكون مجموع قيم جميع كائنات Coin في النظام مساويًا للحقل total_value في كائن Info المخزن في عنوان ADMIN. الثابت هو مصطلح في التحقق الرسمي، يشير إلى الحفاظ على الحالة. هذه الخاصية الحافظة تنطبق على جميع العملاء المحتملين للوحدة.
b) مدقق التعليمات البرمجية: النوع الأمني والتسلسل الخطي هما النطاق الرئيسي للتحقق في مدقق التعليمات البرمجية. على الرغم من أن الوحدات الأخرى لا يمكنها الوصول إلى وحدة التخزين العالمية التي تتحكم بها 0x1::TestCoin::Coin، إلا أنه يمكن استخدامها في إعلانات العمليات والهياكل الخاصة بها.
يحتوي Move على محقق بايت كود ( الذي ينفذ نظام الأنواع على مستوى بايت كود )، مما يسمح لمالك الوحدة بمنع النتائج غير المرغوب فيها. فقط الوحدات التي تعلن عن نوع الهيكل Coin يمكنها: • إنشاء قيمة من نوع Coin • "فك حزمة" قيمة نوع Coin إلى حقولها المكونة • الحصول على مرجع لحقل Coin من خلال الاقتراض المتغير أو غير المتغير بأسلوب rust
تفرض المدقق أيضًا أن تكون الهياكل الافتراضية خطية، لضمان منع النسخ والتدمير خارج الوحدة التي تم إعلان الهيكل فيها بشكل خطي. في الوقت نفسه، سيقوم المدقق أيضًا بإجراء فحوصات إلزامية لبعض أنواع مشاكل الذاكرة الشائعة.
تشمل عملية الكشف ثلاث فئات رئيسية:
يقوم المدقق أولاً بإنشاء CFG( لرسم تدفق التحكم )، ثم يتحقق من نطاق وصول المستدعي في المكدس، لضمان عدم قدرة المستدعي للعقد على الوصول إلى مساحة المكدس الخاصة بالمدعو. وفي الوقت نفسه، للتحقق من النوع، يحتفظ كل مكدس قيمة بمكدس نوع مقابله.
التالي هو فحص الموارد وفحص الاقتباسات. يركز فحص الموارد بشكل أساسي على قيود مثل عدم إمكانية الإنفاق المزدوج، وعدم القابلية للتدمير، وضرورة وجود ملكية. يجمع فحص الاقتباسات بين التحليل الديناميكي والثابت، ويستخدم آلية فحص الاقتراض المشابهة لنظام نوع روست.
أخيرًا، هناك فحص للروابط، حيث يجب التحقق مرة أخرى مما إذا كانت كائنات الروابط والبيانات متطابقة، بالإضافة إلى التحكم في الوصول للعملية.
آلية تشغيل Move
أولاً، يعمل برنامج Move في آلة افتراضية، ولا يمكنه الوصول إلى ذاكرة النظام أثناء التشغيل. وهذا يسمح لـ Move بالعمل بأمان في بيئات غير موثوقة، دون أن يتم تدميره أو إساءة استخدامه.
ثانيًا، يتم تنفيذ برنامج Move على المكدس. يتم تقسيم التخزين العالمي إلى ذاكرة ( كومة ) ومتغيرات عالمية ( مكدس ). الذاكرة هي تخزين من الدرجة الأولى، ولا يمكن لوحداتها تخزين مؤشرات تشير إلى وحدات الذاكرة. تُستخدم المتغيرات العالمية لتخزين مؤشرات تشير إلى وحدات الذاكرة، ولكن طريقة الفهرسة تختلف. عند الوصول إلى المتغيرات العالمية، يوفر الكود العنوان والنوع المرتبط بذلك العنوان. تُبسط هذه التقسيمات العمليات، مما يجعل دلالة لغة Move أكثر سهولة في الصياغة.
تُنفذ تعليمات بايت كود Move في المفسر القائم على المكدس. من السهل تنفيذ والتحكم في الآلة الافتراضية القائمة على المكدس، كما أن لديها متطلبات أقل على البيئة المادية، مما يجعلها مناسبة لسيناريوهات blockchain. بالمقارنة مع المفسر القائم على السجلات، فإن المفسر القائم على المكدس يجعل من السهل التحكم في النسخ و النقل بين المتغيرات واكتشافها.
في Move، يمكن أن يتم تدمير القيم المعرفة كموارد فقط من خلال التحريك المدمر ( مما يجعل موقع التخزين الذي تم حفظ تلك القيمة فيه غير صالح )، لكن بعض القيم ( مثل الأعداد الصحيحة ) يمكن نسخها.
عندما يعمل برنامج Move على المكدس، تكون حالته رباعية الأبعاد ⟨C, M, G, S⟩، والتي تتكون من مكدس الاستدعاء (C)، الذاكرة (M)، المتغيرات العالمية (G) وOperands (S). كما يحتفظ المكدس بجدول الدوال ( module نفسه ) لتحليل التعليمات التي تحتوي على جسم الدالة.
تحتوي مكدس الاستدعاء على جميع معلومات السياق وتعليمات تنفيذ العملية. عند تنفيذ تعليمات Call، يتم إنشاء كائن مكدس استدعاء جديد، ويتم تخزين معلمات الاستدعاء في الذاكرة والمتغيرات العالمية، ثم يقوم المفسر بتنفيذ تعليمات العقد الجديد. عند مواجهة تعليمات الفرع، يحدث قفز ثابت داخل هذه العملية. تعتمد العملية داخل الوحدة على عدم وجود حلقات، بالإضافة إلى عدم وجود تخصيص ديناميكي داخل الوحدة، مما يعزز عدم قابلية تغيير استدعاءات الدوال خلال فترة التنفيذ: يجب أن تكون إطارات استدعاء العملية متجاورة، مما يتجنب إمكانية إعادة الدخول. تنتهي عملية الاستدعاء عند تنفيذ return، ويتم وضع قيمة الإرجاع في قمة المكدس.
من خلال دراسة كود MoveVM، يتضح أن MoveVM يفصل بين تخزين البيانات ومنطق عملية استدعاء المكدس (، وهو أكبر اختلاف عن EVM. في EVM، يتطلب تنفيذ توكن ERC20 كتابة المنطق في عقد واحد وتسجيل حالة كل مستخدم، بينما في MoveVM، يتم تخزين حالة المستخدم ) للموارد تحت عنوان الحساب ( بشكل مستقل، ويجب أن يتوافق استدعاء البرنامج مع قواعد الإذن والقواعد الإلزامية المتعلقة بالموارد. على الرغم من أن هذا يتطلب بعض التضحية بالمرونة، إلا أنه يساعد في تحقيق تحسين كبير في الأمان وكفاءة التنفيذ ) لتحقيق تنفيذ متزامن (.
![تحليل أمان Move: تغيير قواعد اللعبة في لغة العقود الذكية])https://img-cdn.gateio.im/webp-social/moments-69101617731b12c40620802eecf76caf.webp(
) 3. نقل المدقق
أخيرًا، دعونا نتعرف على أداة التدقيق الآلي المساعدة التي تقدمها Move، وهي Move prover.
Move Prover هي أداة للتحقق الرسمي المستند إلى الاستدلال. تستخدم لغة رسمية لوصف سلوك البرنامج وتستخدم خوارزميات الاستدلال للتحقق مما إذا كان البرنامج يتوافق مع التوقعات، مما يساعد المطورين على ضمان صحة العقود الذكية وتقليل مخاطر المعاملات. باختصار، فإن التحقق الرسمي هو استخدام طرق رياضية لإثبات أن النظام خالٍ من الأخطاء.
تستند خوارزميات التحقق الآلي للبرامج السائدة حاليًا إلى محللات نظرية الإرضاء SMT solver###. في الواقع، SMT solver هو محلل صيغ. تقوم خوارزميات التحقق البرمجي العليا بتقسيم أهداف التحقق إلى صيغ، وتقديمها إلى SMT solver لحلها، بناءً على النتائج، يتم تحليلها بشكل أكبر، وفي النهاية، يتم الإبلاغ عن تحقق الهدف أو اكتشاف ضد المثال.
الخوارزمية الأساسية للتحقق هي التحقق الاستنتاجي (deductive verification)، وهناك خوارزميات تحقق أخرى مثل فحص النماذج المحدودة، طريقة الاستقراء k، التجريد القائم على القضايا والتجريد القائم على المسار وغيرها.
يستخدم Move Prover خوارزمية التحقق الاستدلالي للتحقق مما إذا كان البرنامج يتوافق مع التوقعات. وهذا يعني أن Move Prover يمكنه استنتاج سلوك البرنامج بناءً على المعلومات المعروفة، مما يضمن توافقه مع السلوك المتوقع. وهذا يساعد في ضمان صحة البرنامج وتقليل عبء العمل على الاختبارات اليدوية.
الهيكل العام لـ Move Prover كما يلي:
أولاً، يستقبل Move Prover ملف مصدر Move يحتوي على مواصفات إدخال البرنامج (specification). يقوم Move Parser باستخراج المواصفات من الشيفرة المصدرية. يقوم مترجم Move بترجمة ملف المصدر إلى بايت كود، مع تحويله إلى نموذج كائن المثبت (Prover Object Model).
تمت ترجمة النموذج إلى لغة Boogie الوسيطة. يتم تمرير كود Boogie إلى نظام التحقق من Boogie لإجراء "توليد شروط التحقق". يتم تمرير شروط التحقق إلى حل Z3 (، وهو حل SMT تم تطويره بواسطة Microsoft ).
بعد إدخال VC في Z3، يتحقق المدقق مما إذا كانت شفرة البرنامج SMT المعادلة ( تلبي specification ) أم لا. إذا كان الأمر كذلك، فهذا يعني أن المواصفة صحيحة. خلاف ذلك، يتم إنشاء نموذج يلبي الشروط، وتحويله مرة أخرى إلى تنسيق Boogie لنشر تقرير التشخيص. يتم استعادة تقرير التشخيص إلى أخطاء مستوى الشيفرة المصدرية مشابهة لأخطاء المترجم القياسي.
! [MoveAnn.]