/ مجموعة برامج Web3 الكاملة للتحقق الرسمي المتقدم /
أصدرت CertiK مؤخرًا تقرير تحقق رسمي متقدم حول وحدة Cosmos SDK Bank، والتي، على حد علمنا، هي أول محاولة ناجحة للتحقق الرسمي من Cosmos SDK. التحقق الرسمي هو أسلوب يستخدم المنطق الرياضي للتأكد من أن النظام يتوافق مع المواصفات بحيث يتصرف كما هو متوقع في ظل جميع المدخلات والظروف الممكنة. في هذه المقالة، سنقدم الخطوات المحددة للتحقق رسميًا من وحدة Cosmos SDK Bank، بالإضافة إلى بعض نتائج التحقق.
ما هو Cosmos SDK؟
تعد مجموعة تطوير البرمجيات Cosmos Software Development Kit (SDK) بمثابة إطار عمل يمكّن المطورين من إنشاء تطبيقات blockchain مخصصة. باستخدام Cosmos SDK، يمكن للمطورين بسهولة بدء تشغيل blockchain الخاص بهم من الطبقة الأولى دون القلق بشأن التصميم والتنفيذ من طبقة الإجماع إلى طبقة التطبيق. توفر Cosmos SDK وحدات أساسية قياسية يمكن استيرادها مباشرة واستخدامها بواسطة أي سلسلة، مثل وحدات التوقيع المساحي والمصادقة والحكومة والنعناع.
مصدر:
وحدة البنك
وحدة البنك في Cosmos SDK مسؤولة عن جميع الوظائف المتعلقة بإدارة الرمز المميز، مثل نقل الرموز المميزة الأصلية. يحتاج إرسال الرموز المميزة إلى تلبية العديد من القيود والشروط، مثل وجود عدد كافٍ من الرموز المميزة في الحساب، باستثناء تلك التي تم رهنها أو قفلها أو التي تم إلغاء ربطها. بدعم من وحدات مثل التوقيع المساحي والمصادقة، تدير وحدة البنك عملية إرسال الرمز المميز بالكامل. على الرغم من أن وحدة البنك تعتمد على عدة وحدات أخرى، نظرًا لأنها خارج نطاق هذا التحقق الرسمي، فإننا نضع بعض الافتراضات حول وظائفها لتبسيط العملية.
تتكون الوحدة البنكية لـ SDK من عدة وحدات فرعية، بما في ذلك الحارس والأنواع، وهي المكونات الأساسية التي تحدد سلوك الوحدة وأنواع البيانات. سنركز على وحدة keeper الفرعية لأنها تغطي الوظائف والميزات الرئيسية للوحدة.
تحتوي الوحدة الفرعية keeper على مكونين رئيسيين: العرض والإرسال. يكون حارس العرض مسؤولاً عن إدارة الحسابات والأرصدة، بينما يكون حارس الإرسال مسؤولاً عن تغيير أرصدة الحسابات، مثل نقل الرموز المميزة المقفلة أو غير المؤمّنة وتخزينها. يوضح الشكل أدناه تدفق وحدة البنك، حيث تشير الأسهم إلى الاتجاه من المكونات إلى الوظائف أو Keepers.
مصدر:
طريقة المصادقة
كما ذكرنا سابقًا، يقتصر نطاق هذا التحقق على وحدة البنك. قبل أن يبدأ التحقق، نقوم أولاً بصياغة مواصفات رسمية لأنواع البيانات في وحدة البنك. على سبيل المثال، توجد بنية بيانات رمزية في وحدة البنك، والتي تحتوي على فئة النوع string ومقدار النوع big.Int، والذي تم تعريفه في الكود المصدري على النحو التالي:
هذا الهيكل بسيط للغاية، ونحن نستخدم Coq (لغة النمذجة والتحقق الرسمية الخاصة بنا) لتعريفه على النحو التالي:
بناءً على هذا التعريف، قمنا أولاً بإثبات بعض الخصائص حول العمليات الأساسية للعملة المعدنية لوضع الأساس للسلامة الوظيفية لوحدة البنك، لأنها تتطلب تعديلاً وتلاعبًا متكررًا بنوع العملة. على سبيل المثال:
تثبت هذه الفكرة ثباتًا أساسيًا: إن طرح عملتين معدنيتين لا يغير فئاتهما، ولا يؤدي إلى توازن سلبي.
على غرار المثال السابق، تم تصميم المكونات الأساسية لكل انتقال حالة في Coq. تتضمن هذه المكونات KV Store وGasMeter ومعالجة الأخطاء والسياق.
للحصول على المواصفات التفصيلية لأنواع البيانات والتحقق منها، يرجى الاطلاع على:
نموذج الحارس
بعد الانتهاء من نمذجة المكونات الأساسية، يمكننا نمذجة الحارس الأساسي لوحدة البنك لوصف وظيفة الوحدة. يمتلك حارس البنك واجهتين، واحدة للوصول للقراءة فقط إلى بيانات الرمز المميز والأخرى لنقل الرمز المميز وصيانة العرض.
يعد View keeper مسؤولاً عن التعامل مع حق الوصول للقراءة فقط إلى أرصدة الحسابات ويحتوي على أربع وظائف لحساب أرصدة الحسابات:
GetBalance: الاستعلام عن رصيد الحساب لفئة معينة من خلال العنوان. يأخذ في الاعتبار حالتين: تسلسل من البايتات الفارغة وتسلسل من البايتات غير الفارغة. يضمن التحقق الرسمي أن وظيفة GetBalance تنتج نتائج صحيحة في كلتا الحالتين.
LockedCoins: إرجاع جميع الرموز المميزة غير القابلة للاستهلاك للحساب المطابق للعنوان. نظرًا لضيق الوقت، قمنا بوضع افتراضات حول بعض التطبيقات من وحدة المصادقة.
GetAllBalances: إرجاع كافة أرصدة الحسابات تحت العنوان المحدد.
GetAccountsBalances: إرجاع كافة أرصدة الحسابات من التخزين، مع حقول BAddress وBCoins كسجلات.
يتولى مدير الإرسال عمليات نقل الرمز المميز وتوريده. أثناء عملية النقل، فإنه يحافظ على توريد العملات بحيث لا يتم سك أي رموز جديدة.
1.SetBalance: قم بتعيين رصيد الرمز المميز للحساب من خلال العنوان. تأخذ هذه الوظيفة في الاعتبار حالتين: أرصدة مضبوطة على صفر وأرصدة مضبوطة على غير صفر. وفي كلتا الحالتين، تم إثبات صحة SetBalance.
2.subUnlockedCoin: خصم المبلغ المحدد (الرمز المميز) من العنوان. تقوم الوظيفة العودية subUnlockedCoins بنفس الشيء بالنسبة لمجموعة من الرموز المميزة. يتم التعامل مع الخصائص ذات الصلة لهذه الوظائف كافتراضات بديهية.
addCoin: أضف مبلغًا محددًا (رمزًا مميزًا) إلى العنوان. تقوم الوظيفة العودية addCoins بتنفيذ نفس العملية على مجموعة من الرموز المميزة. يتم التعامل مع الخصائص ذات الصلة لهذه الوظائف كافتراضات بديهية.
SendCoins: أرسل الأموال من عنوان حساب واحد إلى عنوان حساب آخر، بحيث يتم تحديث الذهب الموجود في كلا العنوانين. في حالة عدم وجود المستلم، سيتم إنشاء حساب جديد له.
باستخدام النموذج أعلاه للمكونات الأساسية، يمكننا البدء في التحقق.
عملية التحقق
يتم التحقق من خلال الوصف الرسمي للخصائص الثابتة لهذه الوظائف وإثباتها في نظام إثبات مساعد، مع التركيز بشكل أساسي على الوظيفة الأساسية لـ "View Keeper" و"Send Keeper".
على سبيل المثال، تثبت المواصفات وlemma setBalance_ok صحة وظيفة setBalance الخاصة بوحدة BaseSendKeeper، وتثبت على وجه التحديد الخصائص التالية:
عندما يُرجع send.setBalance الحالة "موافق"، يكون هناك newMultiStore، وفي هذا الوقت، يتم اشتقاق البيئة المحدثة uctx من البيئة القديمة الأصلية ctx عن طريق تحديث newMultiStore.
الرصيد الذي يتم تعيينه هو رمز مميز صالح (يحتوي على الخصائص المطلوبة للرمز المميز في النظام).
يتم الحفاظ على علاقة setBalance_prop للتأكد من أن الوظيفة تقوم بتحديث الرصيد في newMultiStore بالطريقة المتوقعة، وتنشئ البيئة المحدثة uctx.
بعد اكتمال إعداد الرصيد، استخدم عنوان الحساب ورصيد الفئة (Denom) للاتصال بـ view.GetBalance على البيئة المحدثة uctx، وسيتم إرجاع نفس الرصيد الذي تم تعيينه بواسطة send.setBalance.
يتم وصف هذه الخصائص في لغة مواصفات Coq على النحو التالي:
للحصول على رموز Coq للعقارات الأخرى، قم بزيارة:
مهنة المستقبل
ويرتكز أساس هذا التحقق على عدة افتراضات وبديهيات، يمكننا التحقق منها بشكل أعمق لتوسيع نطاق التحقق. وتشمل أولويات العمل المستقبلي المجالات التالية:
التحقق من الافتراضات: يعتمد التحقق الحالي على سلسلة من الافتراضات كأساس للإثبات. ويمكن اختبار هذه الافتراضات في المستقبل للتأكد من أنها تعكس بدقة السلوك والخصائص المقصودة للنظام.
التحقق من وحدة المصادقة: هذه الوحدة مسؤولة عن إدارة بيانات الحساب وآلية التوقيع، وهي المكون الأساسي لـ Cosmos SDK. في المستقبل، يمكن التحقق منها رسميًا بالكامل للتأكد من دقة تنفيذ الوحدة والتفاعل مع الوحدات الأخرى.
المزيد من النظريات حول التكليف وسك وبيع العملات: إن توسيع نطاق التحقق وإدخال المزيد من النظريات حول التكليف وسك وبيع العملات سيساعد على فهم آلية تشغيل النظام بشكل أكثر شمولاً. يمكن دمج هذه النظريات مع التحقق من وحدة المصادقة لضمان الاتساق العام وصحة النظام.
توسيع البنية التحتية لـ Cosmos SDK بالكامل: تركز أعمال التحقق في هذه المرحلة بشكل أساسي على وحدة البنك والمكونات المرتبطة بها. في المستقبل، يمكن توسيع عملية التحقق الرسمية لتشمل البنية التحتية لـ Cosmos SDK بأكملها، وبالتالي تعزيز الدقة الشاملة والأمن والاستقرار للنظام الأساسي وتزويد المطورين والمستخدمين ببيئة أكثر استقرارًا وموثوقية.
التكامل مع الوحدات الأخرى: نظرًا لأن Cosmos SDK تتضمن مجموعة متنوعة من الوحدات المترابطة، فمن المفيد جدًا استكشاف التفاعلات والتبعيات بينها. ويتطلب ذلك التحقق من صحة التفاعلات بين الوحدات والتأكد من أن أي تغييرات يتم إجراؤها على وحدة واحدة لا تؤثر سلبًا على الوحدات الأخرى.
نمذجة آليات الحوافز والتحقق منها: تدمج Cosmos SDK أيضًا آليات الحوافز مثل التوقيع المساحي وتوزيع المكافآت. سوف تقوم الأبحاث المستقبلية بصياغة هذه الآليات والتحقق من صحتها للتأكد من صحتها واتساقها مع الحوافز الاقتصادية المتوقعة.
توضح هذه المقالة أول حالة ناجحة للتحقق الرسمي المتقدم من وحدة Cosmos SDKbank، مما يؤدي إلى عمل فعال لبناء أساس الأمان والموثوقية للنظام البيئي blockchain. سوف يتوسع العمل المستقبلي في هذا الإنجاز من خلال التحقق من صحة الافتراضات، والتحقق من الوحدات الأخرى، وتغطية البنية التحتية لـ Cosmos SDK بالكامل، مما يؤدي في النهاية إلى بناء منصة أكثر صلابة وجديرة بالثقة للمطورين والمستخدمين.
شاهد النسخة الأصلية
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
اشرح بالتفصيل التحقق الرسمي من الوحدات القياسية لـ Cosmos SDK
/ مجموعة برامج Web3 الكاملة للتحقق الرسمي المتقدم /
أصدرت CertiK مؤخرًا تقرير تحقق رسمي متقدم حول وحدة Cosmos SDK Bank، والتي، على حد علمنا، هي أول محاولة ناجحة للتحقق الرسمي من Cosmos SDK. التحقق الرسمي هو أسلوب يستخدم المنطق الرياضي للتأكد من أن النظام يتوافق مع المواصفات بحيث يتصرف كما هو متوقع في ظل جميع المدخلات والظروف الممكنة. في هذه المقالة، سنقدم الخطوات المحددة للتحقق رسميًا من وحدة Cosmos SDK Bank، بالإضافة إلى بعض نتائج التحقق.
ما هو Cosmos SDK؟
تعد مجموعة تطوير البرمجيات Cosmos Software Development Kit (SDK) بمثابة إطار عمل يمكّن المطورين من إنشاء تطبيقات blockchain مخصصة. باستخدام Cosmos SDK، يمكن للمطورين بسهولة بدء تشغيل blockchain الخاص بهم من الطبقة الأولى دون القلق بشأن التصميم والتنفيذ من طبقة الإجماع إلى طبقة التطبيق. توفر Cosmos SDK وحدات أساسية قياسية يمكن استيرادها مباشرة واستخدامها بواسطة أي سلسلة، مثل وحدات التوقيع المساحي والمصادقة والحكومة والنعناع.
مصدر:
وحدة البنك
وحدة البنك في Cosmos SDK مسؤولة عن جميع الوظائف المتعلقة بإدارة الرمز المميز، مثل نقل الرموز المميزة الأصلية. يحتاج إرسال الرموز المميزة إلى تلبية العديد من القيود والشروط، مثل وجود عدد كافٍ من الرموز المميزة في الحساب، باستثناء تلك التي تم رهنها أو قفلها أو التي تم إلغاء ربطها. بدعم من وحدات مثل التوقيع المساحي والمصادقة، تدير وحدة البنك عملية إرسال الرمز المميز بالكامل. على الرغم من أن وحدة البنك تعتمد على عدة وحدات أخرى، نظرًا لأنها خارج نطاق هذا التحقق الرسمي، فإننا نضع بعض الافتراضات حول وظائفها لتبسيط العملية.
تتكون الوحدة البنكية لـ SDK من عدة وحدات فرعية، بما في ذلك الحارس والأنواع، وهي المكونات الأساسية التي تحدد سلوك الوحدة وأنواع البيانات. سنركز على وحدة keeper الفرعية لأنها تغطي الوظائف والميزات الرئيسية للوحدة.
تحتوي الوحدة الفرعية keeper على مكونين رئيسيين: العرض والإرسال. يكون حارس العرض مسؤولاً عن إدارة الحسابات والأرصدة، بينما يكون حارس الإرسال مسؤولاً عن تغيير أرصدة الحسابات، مثل نقل الرموز المميزة المقفلة أو غير المؤمّنة وتخزينها. يوضح الشكل أدناه تدفق وحدة البنك، حيث تشير الأسهم إلى الاتجاه من المكونات إلى الوظائف أو Keepers.
مصدر:
طريقة المصادقة
كما ذكرنا سابقًا، يقتصر نطاق هذا التحقق على وحدة البنك. قبل أن يبدأ التحقق، نقوم أولاً بصياغة مواصفات رسمية لأنواع البيانات في وحدة البنك. على سبيل المثال، توجد بنية بيانات رمزية في وحدة البنك، والتي تحتوي على فئة النوع string ومقدار النوع big.Int، والذي تم تعريفه في الكود المصدري على النحو التالي:
هذا الهيكل بسيط للغاية، ونحن نستخدم Coq (لغة النمذجة والتحقق الرسمية الخاصة بنا) لتعريفه على النحو التالي:
بناءً على هذا التعريف، قمنا أولاً بإثبات بعض الخصائص حول العمليات الأساسية للعملة المعدنية لوضع الأساس للسلامة الوظيفية لوحدة البنك، لأنها تتطلب تعديلاً وتلاعبًا متكررًا بنوع العملة. على سبيل المثال:
تثبت هذه الفكرة ثباتًا أساسيًا: إن طرح عملتين معدنيتين لا يغير فئاتهما، ولا يؤدي إلى توازن سلبي.
على غرار المثال السابق، تم تصميم المكونات الأساسية لكل انتقال حالة في Coq. تتضمن هذه المكونات KV Store وGasMeter ومعالجة الأخطاء والسياق.
للحصول على المواصفات التفصيلية لأنواع البيانات والتحقق منها، يرجى الاطلاع على:
نموذج الحارس
بعد الانتهاء من نمذجة المكونات الأساسية، يمكننا نمذجة الحارس الأساسي لوحدة البنك لوصف وظيفة الوحدة. يمتلك حارس البنك واجهتين، واحدة للوصول للقراءة فقط إلى بيانات الرمز المميز والأخرى لنقل الرمز المميز وصيانة العرض.
يعد View keeper مسؤولاً عن التعامل مع حق الوصول للقراءة فقط إلى أرصدة الحسابات ويحتوي على أربع وظائف لحساب أرصدة الحسابات:
GetBalance: الاستعلام عن رصيد الحساب لفئة معينة من خلال العنوان. يأخذ في الاعتبار حالتين: تسلسل من البايتات الفارغة وتسلسل من البايتات غير الفارغة. يضمن التحقق الرسمي أن وظيفة GetBalance تنتج نتائج صحيحة في كلتا الحالتين.
LockedCoins: إرجاع جميع الرموز المميزة غير القابلة للاستهلاك للحساب المطابق للعنوان. نظرًا لضيق الوقت، قمنا بوضع افتراضات حول بعض التطبيقات من وحدة المصادقة.
GetAllBalances: إرجاع كافة أرصدة الحسابات تحت العنوان المحدد.
GetAccountsBalances: إرجاع كافة أرصدة الحسابات من التخزين، مع حقول BAddress وBCoins كسجلات.
يتولى مدير الإرسال عمليات نقل الرمز المميز وتوريده. أثناء عملية النقل، فإنه يحافظ على توريد العملات بحيث لا يتم سك أي رموز جديدة.
1.SetBalance: قم بتعيين رصيد الرمز المميز للحساب من خلال العنوان. تأخذ هذه الوظيفة في الاعتبار حالتين: أرصدة مضبوطة على صفر وأرصدة مضبوطة على غير صفر. وفي كلتا الحالتين، تم إثبات صحة SetBalance.
2.subUnlockedCoin: خصم المبلغ المحدد (الرمز المميز) من العنوان. تقوم الوظيفة العودية subUnlockedCoins بنفس الشيء بالنسبة لمجموعة من الرموز المميزة. يتم التعامل مع الخصائص ذات الصلة لهذه الوظائف كافتراضات بديهية.
addCoin: أضف مبلغًا محددًا (رمزًا مميزًا) إلى العنوان. تقوم الوظيفة العودية addCoins بتنفيذ نفس العملية على مجموعة من الرموز المميزة. يتم التعامل مع الخصائص ذات الصلة لهذه الوظائف كافتراضات بديهية.
SendCoins: أرسل الأموال من عنوان حساب واحد إلى عنوان حساب آخر، بحيث يتم تحديث الذهب الموجود في كلا العنوانين. في حالة عدم وجود المستلم، سيتم إنشاء حساب جديد له.
باستخدام النموذج أعلاه للمكونات الأساسية، يمكننا البدء في التحقق.
عملية التحقق
يتم التحقق من خلال الوصف الرسمي للخصائص الثابتة لهذه الوظائف وإثباتها في نظام إثبات مساعد، مع التركيز بشكل أساسي على الوظيفة الأساسية لـ "View Keeper" و"Send Keeper".
على سبيل المثال، تثبت المواصفات وlemma setBalance_ok صحة وظيفة setBalance الخاصة بوحدة BaseSendKeeper، وتثبت على وجه التحديد الخصائص التالية:
عندما يُرجع send.setBalance الحالة "موافق"، يكون هناك newMultiStore، وفي هذا الوقت، يتم اشتقاق البيئة المحدثة uctx من البيئة القديمة الأصلية ctx عن طريق تحديث newMultiStore.
الرصيد الذي يتم تعيينه هو رمز مميز صالح (يحتوي على الخصائص المطلوبة للرمز المميز في النظام).
يتم الحفاظ على علاقة setBalance_prop للتأكد من أن الوظيفة تقوم بتحديث الرصيد في newMultiStore بالطريقة المتوقعة، وتنشئ البيئة المحدثة uctx.
بعد اكتمال إعداد الرصيد، استخدم عنوان الحساب ورصيد الفئة (Denom) للاتصال بـ view.GetBalance على البيئة المحدثة uctx، وسيتم إرجاع نفس الرصيد الذي تم تعيينه بواسطة send.setBalance.
يتم وصف هذه الخصائص في لغة مواصفات Coq على النحو التالي:
للحصول على رموز Coq للعقارات الأخرى، قم بزيارة:
مهنة المستقبل
ويرتكز أساس هذا التحقق على عدة افتراضات وبديهيات، يمكننا التحقق منها بشكل أعمق لتوسيع نطاق التحقق. وتشمل أولويات العمل المستقبلي المجالات التالية:
التحقق من الافتراضات: يعتمد التحقق الحالي على سلسلة من الافتراضات كأساس للإثبات. ويمكن اختبار هذه الافتراضات في المستقبل للتأكد من أنها تعكس بدقة السلوك والخصائص المقصودة للنظام.
التحقق من وحدة المصادقة: هذه الوحدة مسؤولة عن إدارة بيانات الحساب وآلية التوقيع، وهي المكون الأساسي لـ Cosmos SDK. في المستقبل، يمكن التحقق منها رسميًا بالكامل للتأكد من دقة تنفيذ الوحدة والتفاعل مع الوحدات الأخرى.
المزيد من النظريات حول التكليف وسك وبيع العملات: إن توسيع نطاق التحقق وإدخال المزيد من النظريات حول التكليف وسك وبيع العملات سيساعد على فهم آلية تشغيل النظام بشكل أكثر شمولاً. يمكن دمج هذه النظريات مع التحقق من وحدة المصادقة لضمان الاتساق العام وصحة النظام.
توسيع البنية التحتية لـ Cosmos SDK بالكامل: تركز أعمال التحقق في هذه المرحلة بشكل أساسي على وحدة البنك والمكونات المرتبطة بها. في المستقبل، يمكن توسيع عملية التحقق الرسمية لتشمل البنية التحتية لـ Cosmos SDK بأكملها، وبالتالي تعزيز الدقة الشاملة والأمن والاستقرار للنظام الأساسي وتزويد المطورين والمستخدمين ببيئة أكثر استقرارًا وموثوقية.
التكامل مع الوحدات الأخرى: نظرًا لأن Cosmos SDK تتضمن مجموعة متنوعة من الوحدات المترابطة، فمن المفيد جدًا استكشاف التفاعلات والتبعيات بينها. ويتطلب ذلك التحقق من صحة التفاعلات بين الوحدات والتأكد من أن أي تغييرات يتم إجراؤها على وحدة واحدة لا تؤثر سلبًا على الوحدات الأخرى.
نمذجة آليات الحوافز والتحقق منها: تدمج Cosmos SDK أيضًا آليات الحوافز مثل التوقيع المساحي وتوزيع المكافآت. سوف تقوم الأبحاث المستقبلية بصياغة هذه الآليات والتحقق من صحتها للتأكد من صحتها واتساقها مع الحوافز الاقتصادية المتوقعة.
توضح هذه المقالة أول حالة ناجحة للتحقق الرسمي المتقدم من وحدة Cosmos SDKbank، مما يؤدي إلى عمل فعال لبناء أساس الأمان والموثوقية للنظام البيئي blockchain. سوف يتوسع العمل المستقبلي في هذا الإنجاز من خلال التحقق من صحة الافتراضات، والتحقق من الوحدات الأخرى، وتغطية البنية التحتية لـ Cosmos SDK بالكامل، مما يؤدي في النهاية إلى بناء منصة أكثر صلابة وجديرة بالثقة للمطورين والمستخدمين.