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

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

مقدمة

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

إذا كان هناك ثغرة أمنية في رمز العقد الذكي، فقد يؤدي ذلك إلى عواقب مدمرة، مثل سرقة جميع الأصول التي يمتلكها. في عام 2021، تم سرقة 50 مليون دولار من منصة (AMM)Uranium Finance بسبب خطأ إملائي في عقد ذكي.

أيضًا في عام 2021، بسبب خطأ في رمز واحد، أصدرت منصة Compound Finance مكافآت بقيمة 80 مليون دولار بشكل خاطئ. وفي عام 2022، بسبب خطأ في عقد ذكي، تم سرقة 3.2 مليار دولار من جسر Wormhole.

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

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

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

تشمل العملية:

• تعريف مواصفات وخصائص العقد باستخدام لغة رسمية.

• تحويل رمز العقد إلى بيانات رسمية، مثل نماذج رياضية أو منطقية.

• استخدام أدوات إثبات نظريات آلية أو فحص نماذج للتحقق من صحة المواصفات والخصائص.

• تكرار عملية التحقق للكشف عن أي أخطاء أو انحرافات عن السلوك المتوقع وإصلاحها.

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

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

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

Uniswap

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

Balancer

أيضًا، تم التحقق من منصة Balancer V2. اكتشفت عملية التحقق خطأ في حساب رسوم ميزة القروض السريعة، والذي كان قد يجعل المنصة عرضة للسرقة.

SafeMoon

بعد نشر SafeMoon V1، تم اكتشاف خطأ دقيق جدًا من خلال التحقق الرسمي. إذا لم يُكتشف هذا الخطأ، فقد يتمكن مالك العقد من استعادة السيطرة على العقد بعد التخلي عن الملكية، إذا قام ببعض العمليات قبل التخلي عنها.

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

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

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

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

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

الخاتمة

لضمان أمان العقود الذكية، من الضروري الجمع بين التحقق الرسمي والتدقيق اليدوي، لضمان تقييم شامل ودقيق للوضع الأمني للعقد.

على الرغم من أن التحقق الرسمي يتطلب موارد عالية، إلا أنه استثمار يستحق العناء للعقود ذات القيمة العالية أو المخاطر الكبيرة. في النهاية، الأمان هو الأولوية القصوى، ويجب أن يُعطى الأولوية للسلامة لضمان أن العقود الذكية خالية من الأخطاء والثغرات والسلوكيات غير المرغوب فيها. **$BNT **$BROCCOLI