Input Output تستعرض Blaster للتحقق من عقود Cardano الذكية

نشرت Cardano Community عرضاً لـ Blaster، وهي أداة تحقق آلي صُممت للتحقق مما إذا كانت عقود Cardano الذكية تلتزم بالقواعد المحددة. يستعرض مهندسا Input Output Romain Soulat وJean-Frédéric Etienne كيفية فحص الأداة لتلك الخصائص وإمكانها إنتاج مثال مضاد عند العثور على انتهاك. كما يناقشان العمل الجاري على إعادة بناء البراهين وسبل جعل النتائج أسهل في التفقد.

تحديد ما يجب أن يفعله عقد Cardano

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

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

كيف تتحقق Blaster من خصائص العقد

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

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

[NEWSBREAK]

إعادة بناء البرهان قيد التطوير

يمكن للمطورين ترجمة العقود المكتوبة بلغات مثل Plinth وAiken وPlutarch إلى Untyped Plutus Core، وهو التمثيل المستخدم لتنفيذ سكربتات Cardano. وبعد ذلك يمكنهم استيراد الشفرة المترجمة إلى Lean 4 وتحديد الخصائص المطلوب التحقق منها. كانت Input Output قد أصدرت في وقت سابق مكتبتين مفتوحتَي المصدر توفران النماذج الخاصة بـ Cardano لهذا المسار. وفي عرض سابق استخدم الفريق خط الأنابيب على عقد تدريبي من تحدي أمني، مُنشئاً سياق معاملة أظهر كيف يمكن استغلال العقد.

أوضح Etienne أن إعادة بناء البرهان لا تزال قيد التطوير. الهدف هو تمكين Lean من التحقق بشكل مستقل من الأدلة الداعمة لنتيجة صحيحة، إذ إن الأداة الحالية لا تنتج بعد برهان Lean معاد البناء عندما يعيد المحلل تلك النتيجة. كما عرض Soulat خططاً لواجهات أوضح لعرض الأمثلة المضادة، ما يتيح للمطورين تفقد تفاصيل المعاملة وراء خاصية فاشلة.