دليل لأدوات أمان العقود الذكية

سنستخدم ثلاث تقنيات مميزة للاختبار وتحليل البرامج:

• التحليل الثابت باستخدام سليذر. يتم تقريب جميع مسارات البرنامج وتحليلها في نفس الوقت، من خلال عروض تقديمية مختلفة للبرنامج (مثل رسم بياني لتدفق التحكم).
• الاختبار العشوائي (Fuzzing) باستخدام إيكيدنا. يتم تنفيذ الكود مع توليد شبه عشوائي للمعاملات. سيحاول المُختبِر العشوائي العثور على تسلسل من المعاملات لانتهاك خاصية معينة.
• التنفيذ الرمزي باستخدام مانتيكور. تقنية تحقق شكلي، تترجم كل مسار تنفيذ إلى صيغة رياضية، والتي يمكن التحقق من القيود بناءً عليها.

لكل تقنية مزايا وعيوب، وستكون مفيدة في حالات محددة:

* إذا تم استكشاف جميع المسارات دون انتهاء المهلة

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

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

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

سير العمل المقترح

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

• استخدم CLI الخاص بسليذر لاكتشاف المشكلات الشائعة
• استخدم إيكيدنا لاختبار خصائص الأمان عالية المستوى لعقدك
• استخدم سليذر لكتابة عمليات تحقق ثابتة مخصصة
• استخدم مانتيكور بمجرد أن ترغب في ضمان متعمق لخصائص الأمان الحرجة

ملاحظة حول اختبارات الوحدة. اختبارات الوحدة ضرورية لبناء برمجيات عالية الجودة. ومع ذلك، فإن هذه التقنيات ليست الأنسب للعثور على الثغرات الأمنية. تُستخدم عادةً لاختبار السلوكيات الإيجابية للكود (أي أن الكود يعمل كما هو متوقع في السياق الطبيعي)، بينما تميل الثغرات الأمنية إلى التواجد في الحالات الطرفية التي لم يأخذها المطورون في الاعتبار. في دراستنا لعشرات المراجعات الأمنية للعقود الذكية، لم يكن لتغطية اختبار الوحدة أي تأثير على عدد أو شدة الثغرات الأمنية (opens in a new tab) التي وجدناها في كود عملائنا.

تحديد خصائص الأمان

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

• التقييمات السريعة للمخاطر (opens in a new tab) (نهجنا المفضل عندما يكون الوقت قصيرًا)
• دليل نمذجة تهديدات النظام المتمحور حول البيانات (opens in a new tab) (المعروف أيضًا باسم NIST 800-154)
• نمذجة تهديدات Shostack (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• استخدام التأكيدات (Assertions) (opens in a new tab)

المكونات

معرفة ما تريد التحقق منه سيساعدك أيضًا في اختيار الأداة المناسبة.

تشمل المجالات الواسعة ذات الصلة المتكررة بالعقود الذكية ما يلي:

• آلة الحالة. يمكن تمثيل معظم العقود كآلة حالة. ضع في اعتبارك التحقق من (1) عدم إمكانية الوصول إلى حالة غير صالحة، (2) إذا كانت الحالة صالحة يمكن الوصول إليها، و(3) لا توجد حالة تُوقع العقد في فخ.

  • إيكيدنا ومانتيكور هما الأداتان المفضلان لاختبار مواصفات آلة الحالة.

• عناصر التحكم في الوصول. إذا كان نظامك يحتوي على مستخدمين ذوي امتيازات (مثل المالك، المتحكمين، ...)، يجب عليك التأكد من أن (1) كل مستخدم يمكنه فقط تنفيذ الإجراءات المصرح بها و(2) لا يمكن لأي مستخدم حظر إجراءات من مستخدم ذي امتيازات أعلى.

  • يمكن لسليذر وإيكيدنا ومانتيكور التحقق من صحة عناصر التحكم في الوصول. على سبيل المثال، يمكن لسليذر التحقق من أن الدوال المدرجة في القائمة البيضاء فقط هي التي تفتقر إلى المُعدِّل onlyOwner. إيكيدنا ومانتيكور مفيدان للتحكم في الوصول الأكثر تعقيدًا، مثل الإذن الممنوح فقط إذا وصل العقد إلى حالة معينة.

• العمليات الحسابية. التحقق من سلامة العمليات الحسابية أمر بالغ الأهمية. يعد استخدام SafeMath في كل مكان خطوة جيدة لمنع تجاوز السعة (overflow/underflow)، ومع ذلك، يجب عليك الاستمرار في النظر في العيوب الحسابية الأخرى، بما في ذلك مشكلات التقريب والعيوب التي تُوقع العقد في فخ.

  • مانتيكور هو الخيار الأفضل هنا. يمكن استخدام إيكيدنا إذا كانت العمليات الحسابية خارج نطاق مُحِلّ SMT.

• صحة الوراثة. تعتمد عقود Solidity بشكل كبير على الوراثة المتعددة. يمكن بسهولة إدخال أخطاء مثل دالة مُظلِّلة تفتقر إلى استدعاء super وسوء تفسير ترتيب التسلسل c3.

  • سليذر هو الأداة لضمان اكتشاف هذه المشكلات.

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

  • مانتيكور وإيكيدنا هما الخيار الأفضل لاختبار التفاعلات الخارجية مع عقودك. يحتوي مانتيكور على آلية مدمجة لاستبدال (stub) العقود الخارجية.

• التوافق مع المعايير. معايير إيثيريوم (مثل ERC-20) لها تاريخ من العيوب في تصميمها. كن على دراية بقيود المعيار الذي تبني عليه.

  • سيساعدك سليذر وإيكيدنا ومانتيكور على اكتشاف الانحرافات عن معيار معين.

ورقة مرجعية لاختيار الأداة

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

تحتوي عمليات التدقيق العامة لدينا على أمثلة للخصائص التي تم التحقق منها أو اختبارها. فكر في قراءة أقسام Automated Testing and Verification من التقارير التالية لمراجعة خصائص الأمان في العالم الحقيقي:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)