ما هو مفهوم التحقق الرسمي من العقود الذكية؟

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

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

يمكن أن يكون للثغرات الأمنية في رمز العقد الذكي عواقب وخيمة، بما في ذلك سرقة جميع الأصول التي يحتفظ بها العقد الذكي. في عام 2021، سرق صانع السوق الآلي (AMM) Uranium Finance 50 مليون دولار بسبب خطأ مطبعي واحد في عقد ذكي، أيضا في عام 2021، قدمت Compound Finance 80 مليون دولار من المكافآت غير المكتسبة بسبب خطأ في حرف واحد. في عام 2022، سرق 320 مليون دولار من جسر الثقب الدودي بسبب خلل في أحد عقوده الذكية.

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

اقرأ أيضاً:ما هي أكثر خمس أسئلة حول العملات المشفرة بحثا على غوغل؟

كيف يعمل التحقق من العقد الذكي؟

يعمل التحقق الرسمي من العقود الذكية من خلال تقديم المنطق والسلوك المطلوب للعقود الذكية كبيانات رياضية. ثم يستخدم المدققون أدوات آلية للتحقق مما إذا كانت هذه البيانات صحيحة.

تتضمن العملية:

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

لماذا التحقق من العقد الذكي مهم للغاية

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

فيما يلي بعض الأمثلة على كيفية مساعدة التحقق من العقود الذكية في منع الخسارة المالية الكبيرة والنتائج الكارثية الأخرى.

Uniswap

Uniswap هو AMM معروف. عندما تم تطوير العقد الذكي Uniswap V1، تم التحقق منه رسميا. قبل إصداره، وجد هذا التحقق الرسمي وإصلاح أخطاء التقريب التي كان من الممكن أن تؤدي إلى استنزاف أموال Uniswap V1.

Balancer V2

Balancer V2 هو أيضا AMM تم التحقق منه رسميا. وجد التحقق الرسمي وأصلح الحساب رسوم غير صحيحة ويتضمن وظيفة قرض الفلاش في العقد الذكي، مما كان يمكن أن يجعل البورصة عرضة للسرقة.

SafeMoon

احتوى SafeMoon V1 على خطأ دقيق تم العثور عليه عن طريق التحقق الرسمي بعد نشره. ومن الممكن للمالك أن يتخلى عن ملكية العقد ثم يستعيده إذا تمت عمليات معينة قبل التخلي عن الملكية.

تم تجاهل هذا الخطأ في معظم عمليات التدقيق اليدوية لشوكات SafeMoon V1 لأن العثور عليه يتطلب تحليل مجموعات محددة من قيم متغيرات البرنامج. هذا شيء يسهل على المستخدمين تجاهله، ويسهل على الآلة التقاطه.

كيف يعمل التحقق الرسمي والتدقيق اليدوي معا

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

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

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

اقرأ أيضاً:ما هي العقود الذكية وما هي المشاكل التي تحلها؟