دليل لأدوات أمن العقود الذكية
سوف نستخدم ثلاث تقنيات مميزة للاختبار وتحليل البرامج:
- التحليل الثابت باستخدام سليذر. يتم تقريب جميع مسارات البرنامج وتحليلها في نفس الوقت، من خلال عروض مختلفة للبرنامج (على سبيل المثال، الرسم البياني لتدفق التحكم)
- الاختبار الأعمى (Fuzzing) باستخدام إيكيدنا. يتم تنفيذ النص البرمجي مع توليد شبه عشوائي للمعاملات. سيحاول المُختبِر الأعمى (fuzzer) إيجاد سلسلة من المعاملات لانتهاك خاصية معينة.
- التنفيذ الرمزي باستخدام مانتيكور. تقنية تحقق رسمية، والتي تترجم كل مسار تنفيذ إلى صيغة رياضية، والتي يمكن التحقق من القيود عليها.
لكل تقنية مزايا وعيوب، وستكون مفيدة في حالات محددة:
| التقنية | أدوات | الاستخدام | Speed | الأخطاء التي تم تفويتها | إنذارات كاذبة |
|---|---|---|---|---|---|
| التحليل الثابت | سليذر | واجهة خط الأوامر (CLI) والنصوص البرمجية | seconds | متوسط | منخفض |
| الاختبار الأعمى (Fuzzing) | إيكيدنا | خصائص سوليديتي | minutes | منخفض | لا شيء |
| التنفيذ الرمزي | مانتيكور | خصائص سوليديتي والنصوص البرمجية | hours | لا شيء* | لا شيء |
* إذا تم استكشاف جميع المسارات دون انتهاء المهلة
سليذر يحلل العقود في غضون ثوانٍ، ومع ذلك، قد يؤدي التحليل الثابت إلى إنذارات كاذبة وسيكون أقل ملاءمة لعمليات التحقق المعقدة (على سبيل المثال، عمليات التحقق الحسابية). قم بتشغيل سليذر عبر واجهة برمجة التطبيقات (API) للوصول السهل إلى الكاشفات المدمجة أو عبر واجهة برمجة التطبيقات (API) لعمليات التحقق التي يحددها المستخدم.
إيكيدنا يحتاج إلى التشغيل لعدة دقائق ولن ينتج إلا نتائج إيجابية حقيقية. يتحقق إيكيدنا من خصائص الأمان التي يقدمها المستخدم، والمكتوبة بلغة سوليديتي. قد يفوت بعض الأخطاء لأنه يعتمد على الاستكشاف العشوائي.
يقوم مانتيكور بإجراء التحليل "الأكثر ثقلاً". مثل إيكيدنا، يتحقق مانتيكور من الخصائص التي يقدمها المستخدم. سيحتاج إلى مزيد من الوقت للتشغيل، ولكنه يمكنه إثبات صحة خاصية ما ولن يُبلغ عن إنذارات كاذبة.
سير العمل المقترح
ابدأ بكاشفات سليذر المدمجة للتأكد من عدم وجود أخطاء بسيطة الآن أو سيتم إدخالها لاحقًا. استخدم سليذر للتحقق من الخصائص المتعلقة بالوراثة، وتبعيات المتغيرات، والمشكلات الهيكلية. مع نمو قاعدة التعليمات البرمجية، استخدم إيكيدنا لاختبار خصائص أكثر تعقيدًا للجهاز الرئيسي. أعد استخدام سليذر لتطوير عمليات تحقق مخصصة للحماية غير المتوفرة من سوليديتي، مثل الحماية من تجاوز دالة ما. أخيرًا، استخدم مانتيكور لإجراء تحقق مستهدف لخصائص الأمان الحرجة، على سبيل المثال، العمليات الحسابية.
- استخدم واجهة خط أوامر (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)
- استخدام التأكيدات (opens in a new tab)
المكونات
معرفة ما تريد التحقق منه سيساعدك أيضًا على تحديد الأداة المناسبة.
تشمل المجالات الواسعة ذات الصلة بشكل متكرر للعقود الذكية ما يلي:
-
الجهاز الرئيسي. يمكن تمثيل معظم العقود كجهاز رئيسي. ضع في اعتبارك التحقق من أن (1) لا يمكن الوصول إلى أي حالة غير صالحة، (2) إذا كانت الحالة صالحة فيمكن الوصول إليها، و (3) لا توجد حالة تحصر العقد.
- إيكيدنا و مانتيكور هما الأداتان المفضلتان لاختبار مواصفات الجهاز الرئيسي.
-
ضوابط الوصول. إذا كان نظامك يحتوي على مستخدمين مميزين (على سبيل المثال، مالك، وحدات تحكم، ...) يجب عليك التأكد من أن (1) كل مستخدم يمكنه فقط أداء الإجراءات المصرح بها و (2) لا يمكن لأي مستخدم منع الإجراءات من مستخدم أكثر امتيازًا.
- يمكن لـ سليذر و إيكيدنا و مانتيكور التحقق من ضوابط الوصول الصحيحة. على سبيل المثال، يمكن لـ سليذر التحقق من أن الدوال المدرجة في القائمة البيضاء فقط تفتقر إلى مُعدِّل onlyOwner. إيكيدنا و مانتيكور مفيدان للتحكم في الوصول الأكثر تعقيدًا، مثل إذن يتم منحه فقط إذا وصل العقد إلى حالة معينة.
-
العمليات الحسابية. التحقق من سلامة العمليات الحسابية أمر بالغ الأهمية. يعد استخدام
SafeMathفي كل مكان خطوة جيدة لمنع التجاوز/التدفق السفلي، ومع ذلك، يجب أن تضع في اعتبارك العيوب الحسابية الأخرى، بما في ذلك مشكلات التقريب والعيوب التي تحصر العقد.- مانتيكور هو الخيار الأفضل هنا. يمكن استخدام إيكيدنا إذا كانت الحسابات خارج نطاق محلل SMT.
-
صحة الوراثة. تعتمد عقود سوليديتي بشكل كبير على الوراثة المتعددة. يمكن بسهولة إدخال أخطاء مثل دالة التظليل التي تفتقد إلى استدعاء
superوسوء تفسير ترتيب الخطية c3.- سليذر هي الأداة لضمان الكشف عن هذه المشكلات.
-
التفاعلات الخارجية. تتفاعل العقود مع بعضها البعض، ولا ينبغي الوثوق ببعض العقود الخارجية. على سبيل المثال، إذا كان عقدك يعتمد على أوراكل خارجية، فهل سيبقى آمنًا إذا تم اختراق نصف الأوراكل المتاحة؟
- مانتيكور و إيكيدنا هما الخيار الأفضل لاختبار التفاعلات الخارجية مع عقودك. يحتوي مانتيكور على آلية مدمجة لإنشاء عقود خارجية بديلة.
-
المطابقة القياسية. معايير إيثريوم (على سبيل المثال ERC20) لها تاريخ من العيوب في تصميمها. كن على دراية بقيود المعيار الذي تبني عليه.
- سيساعدك سليذر و إيكيدنا و مانتيكور على اكتشاف الانحرافات عن معيار معين.
ورقة تلخيص اختيار الأداة
| المكون | أدوات | أمثلة |
|---|---|---|
| الجهاز الرئيسي | إيكيدنا, مانتيكور | |
| التحكم بالوصول | سليذر, إيكيدنا, مانتيكور | تمرين سليذر 2 (opens in a new tab), تمرين إيكيدنا 2 (opens in a new tab) |
| العمليات الحسابية | مانتيكور, إيكيدنا | تمرين إيكيدنا 1 (opens in a new tab), تمارين مانتيكور 1 - 3 (opens in a new tab) |
| صحة الوراثة | سليذر | تمرين سليذر 1 (opens in a new tab) |
| التفاعلات الخارجية | مانتيكور, إيكيدنا | |
| المطابقة القياسية | سليذر, إيكيدنا, مانتيكور | slither-erc (opens in a new tab) |
ستحتاج مجالات أخرى إلى التحقق منها اعتمادًا على أهدافك، لكن مجالات التركيز هذه ذات الحبيبات الخشنة هي بداية جيدة لأي نظام عقد ذكي.
تحتوي عمليات التدقيق العامة لدينا على أمثلة للخصائص التي تم التحقق منها أو اختبارها. ضع في اعتبارك قراءة أقسام الاختبار والتحقق الآلي في التقارير التالية لمراجعة خصائص الأمان في العالم الحقيقي:
آخر تحديث للصفحة: 3 مارس 2026
