شرح تفصيلي للتحقق الرسمي من الوحدات القياسية Cosmos SDK

في هذه المقالة، سنقدم الخطوات المحددة للتحقق رسميًا من وحدة Cosmos SDK Bank، بالإضافة إلى بعض نتائج التحقق.

/ مجموعة برامج Web3 الكاملة للتحقق الرسمي المتقدم /

نشرت CertiK مؤخرًا تقرير تحقق رسمي متقدم حول وحدة Cosmos SDK Bank، والتي على حد علمنا هي أول محاولة ناجحة للتحقق الرسمي من Cosmos SDK. التحقق الرسمي هو أسلوب يستخدم المنطق الرياضي للتأكد من أن النظام يتوافق مع المواصفات بحيث يتصرف كما هو متوقع في ظل جميع المدخلات والظروف الممكنة. في هذه المقالة، سنقدم الخطوات المحددة للتحقق رسميًا من وحدة Cosmos SDK Bank، بالإضافة إلى بعض نتائج التحقق.

ما هو Cosmos SDK؟

تعد مجموعة أدوات تطوير البرمجيات Cosmos (SDK للاختصار) إطارًا يسمح للمطورين ببناء تطبيقات blockchain مخصصة. باستخدام Cosmos SDK، يمكن للمطورين بسهولة إطلاق blockchain من الطبقة الأولى الخاصة بهم دون الحاجة إلى القلق بشأن التصميم والتنفيذ من طبقة الإجماع إلى طبقة التطبيق. توفر Cosmos SDK وحدات أساسية قياسية يمكن استيرادها مباشرة واستخدامها بواسطة أي سلسلة، مثل وحدات التوقيع المساحي والمصادقة والحكومة والنعناع.

مصدر:

وحدة البنك

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

تتكون الوحدة البنكية لـ SDK من عدة وحدات فرعية، بما في ذلك الحارس والأنواع، وهي المكونات الأساسية التي تحدد سلوك الوحدة وأنواع البيانات. سنركز على وحدة keeper الفرعية لأنها تغطي الوظائف والميزات الرئيسية للوحدة.

تحتوي الوحدة الفرعية keeper على مكونين رئيسيين: العرض والإرسال. يكون حارس العرض مسؤولاً عن إدارة الحسابات والأرصدة، بينما يكون حارس الإرسال مسؤولاً عن تغيير أرصدة الحسابات، مثل نقل الرموز المميزة المقفلة أو غير المؤمّنة وتخزينها. يوضح الشكل أدناه تدفق وحدة البنك، حيث تشير الأسهم إلى الاتجاه من المكونات إلى الوظائف أو Keepers.

مصدر:

طريقة المصادقة

كما ذكرنا سابقًا، يقتصر نطاق هذا التحقق على وحدة البنك. قبل أن يبدأ التحقق، نقوم أولاً بصياغة المواصفات الرسمية لأنواع البيانات في وحدة البنك. على سبيل المثال، توجد بنية بيانات رمزية في وحدة البنك، والتي تحتوي على فئة نوع السلسلة ومقدار نوع big.Int، والذي تم تعريفه في الكود المصدري على النحو التالي:

هذا الهيكل بسيط للغاية، نستخدم Coq (لغة النمذجة والتحقق الرسمية الخاصة بنا) لتعريفه على النحو التالي:

بناءً على هذا التعريف، قمنا أولاً بإثبات بعض الخصائص حول العمليات الأساسية للعملة المعدنية لوضع الأساس للسلامة الوظيفية لوحدة البنك، لأنها تتطلب تعديلاً وتلاعبًا متكررًا بنوع العملة. على سبيل المثال:

تثبت هذه الفكرة ثباتًا أساسيًا: طرح عملتين معدنيتين لا يغير من قيمتهما، ولا يسبب توازنًا سلبيًا.

على غرار المثال السابق، تم تصميم المكونات الأساسية لكل انتقال حالة في Coq. تتضمن هذه المكونات KV Store وGasMeter ومعالجة الأخطاء والسياق.

للحصول على المواصفات التفصيلية لأنواع البيانات والتحقق منها، يرجى الاطلاع على:

نموذج الحارس

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

يعد View keeper مسؤولاً عن التعامل مع حق الوصول للقراءة فقط إلى أرصدة الحسابات ويحتوي على أربع وظائف لحساب أرصدة الحسابات:

1. GetBalance: الاستعلام عن رصيد الحساب لفئة معينة من خلال العنوان. يأخذ في الاعتبار حالتين: تسلسل من البايتات الفارغة وتسلسل من البايتات غير الفارغة. يضمن التحقق الرسمي أن وظيفة GetBalance تنتج نتائج صحيحة في كلتا الحالتين.

2. LockedCoins: إرجاع جميع الرموز المميزة غير القابلة للإنفاق في الحساب المطابق للعنوان. نظرًا لضيق الوقت، قمنا بوضع افتراضات حول بعض التطبيقات من وحدة المصادقة.

3. GetAllBalances: إرجاع كافة أرصدة الحسابات تحت العنوان المحدد.

4. GetAccountsBalances: إرجاع كافة أرصدة الحسابات من التخزين، مع حقول BAddress وBCoins كسجلات.

يتولى مدير الإرسال عمليات نقل الرمز المميز وتوريده. أثناء عملية النقل، فإنه يحافظ على توريد العملات بحيث لا يتم سك أي رموز جديدة.

1.SetBalance: قم بتعيين رصيد الرمز المميز للحساب من خلال العنوان. تأخذ هذه الوظيفة في الاعتبار حالتين: توازن مضبوط على صفر ورصيد مضبوط على غير صفر. وفي كلتا الحالتين، تم إثبات صحة SetBalance.

2.subUnlockedCoin: خصم المبلغ المحدد (الرمز المميز) من العنوان. تقوم الوظيفة العودية subUnlockedCoins بتنفيذ نفس العملية على مجموعة من العملات المعدنية. تعتبر الخصائص ذات الصلة لهذه الوظائف افتراضات بديهية.

3. addCoin: أضف المبلغ المحدد (الرموز المميزة) إلى العنوان. تقوم الوظيفة العودية addCoins بتنفيذ نفس العملية على مجموعة من العملات المعدنية. تعتبر الخصائص ذات الصلة لهذه الوظائف افتراضات بديهية.

4. SendCoins: أرسل المبلغ من عنوان حساب واحد إلى عنوان حساب آخر حتى يتم تحديث أموال كلا العنوانين. في حالة عدم وجود المستلم، سيتم إنشاء حساب جديد له.

باستخدام النموذج أعلاه للمكونات الأساسية، يمكننا البدء في التحقق.

عملية التحقق

يتم التحقق من خلال الوصف الرسمي للخصائص الثابتة لهذه الوظائف وإثباتها في نظام إثبات مساعد، مع التركيز بشكل أساسي على الوظيفة الأساسية لـ "View Keeper" و"Send Keeper".

على سبيل المثال، تثبت المواصفات وlemma setBalance_ok صحة وظيفة setBalance الخاصة بوحدة BaseSendKeeper، وتثبت على وجه التحديد الخصائص التالية:

1. عندما يعود send.setBalance إلى حالة "موافق"، يكون هناك newMultiStore، وفي هذا الوقت، يتم اشتقاق البيئة المحدثة uctx من البيئة القديمة الأصلية ctx عن طريق تحديث newMultiStore.

2. الرصيد الذي يتم تعيينه هو رمز مميز صالح (يحتوي على الخصائص المطلوبة للرمز المميز في النظام).

3. يتم الحفاظ على علاقة setBalance_prop للتأكد من أن الوظيفة تقوم بتحديث الرصيد في newMultiStore بطريقة متوقعة وتقوم بإنشاء البيئة المحدثة uctx.

4. بعد اكتمال إعداد الرصيد، استخدم عنوان الحساب ورصيد الفئة (Denom) للاتصال بـ view.GetBalance على البيئة المحدثة uctx، وسيتم إرجاع نفس الرصيد الذي تم تعيينه بواسطة send.setBalance.

يتم وصف هذه الخصائص في لغة مواصفات Coq على النحو التالي:

للحصول على كود Coq ذي الطبيعة الأخرى، قم بزيارة:

مهنة المستقبل

ويرتكز أساس هذا التحقق على عدة افتراضات وبديهيات، يمكننا التحقق منها بشكل أعمق لتوسيع نطاق التحقق. ويركز العمل المستقبلي على المجالات التالية:

1. التحقق من الافتراضات: يعتمد التحقق الحالي على سلسلة من الافتراضات كأساس للإثبات. ويمكن اختبار هذه الافتراضات في المستقبل للتأكد من أنها تعكس بدقة السلوك والخصائص المقصودة للنظام.

2. التحقق من وحدة المصادقة: هذه الوحدة مسؤولة عن إدارة بيانات الحساب وآلية التوقيع، وهي المكون الأساسي لـ Cosmos SDK. في المستقبل، يمكن التحقق منها رسميًا بالكامل للتأكد من دقة تنفيذ الوحدة والتفاعل مع الوحدات الأخرى.

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

4. توسيع البنية التحتية لـ Cosmos SDK بالكامل: تركز أعمال التحقق الحالية بشكل أساسي على وحدة البنك والمكونات المرتبطة بها. في المستقبل، يمكن توسيع عملية التحقق الرسمية لتشمل البنية التحتية لـ Cosmos SDK بأكملها، وبالتالي تعزيز الدقة الشاملة والأمن والاستقرار للنظام الأساسي وتزويد المطورين والمستخدمين ببيئة أكثر استقرارًا وموثوقية.

5. التكامل مع الوحدات الأخرى: نظرًا لأن Cosmos SDK تتضمن مجموعة متنوعة من الوحدات المترابطة، فمن المفيد جدًا استكشاف التفاعلات والتبعيات بينها. ويتطلب ذلك التحقق من صحة التفاعلات بين الوحدات والتأكد من أن أي تغييرات يتم إجراؤها على وحدة واحدة لا تؤثر سلبًا على الوحدات الأخرى.

6. نمذجة آليات الحوافز والتحقق منها: تدمج Cosmos SDK أيضًا آليات الحوافز مثل التوقيع المساحي وتوزيع المكافآت. سوف تقوم الأبحاث المستقبلية بصياغة هذه الآليات والتحقق من صحتها للتأكد من صحتها واتساقها مع الحوافز الاقتصادية المتوقعة.

توضح هذه المقالة أول حالة ناجحة للتحقق الرسمي المتقدم من وحدة Cosmos SDKbank، مما يؤدي إلى عمل فعال لبناء أساس الأمان والموثوقية للنظام البيئي blockchain. سوف يتوسع العمل المستقبلي في هذا الإنجاز من خلال التحقق من صحة الافتراضات، والتحقق من الوحدات الأخرى، وتغطية البنية التحتية لـ Cosmos SDK بالكامل، مما يؤدي في النهاية إلى بناء منصة أكثر صلابة وجديرة بالثقة للمطورين والمستخدمين.