Echidna: مُختبِر عقود ذكية سريع

Echidna مخلوق غريب يأكل الأخطاء وشديد الحساسية للكهرباء (مع الاعتذار لجاكوب ستانلي)

بشكل أكثر جدية، Echidna هو برنامج بلغة Haskell مصمم لاختبار التشويش/الاختبار القائم على الخصائص لعقود إيثيريوم الذكية. يستخدم حملات تشويش متطورة قائمة على القواعد النحوية بناءً على واجهة ثنائية للعقد (contract ABI) لدحض المسندات المعرّفة من قبل المستخدم أو تأكيدات Solidity. صممنا Echidna مع مراعاة المعيارية، بحيث يمكن توسيعه بسهولة ليشمل طفرات جديدة أو لاختبار عقود محددة في حالات معينة.

الميزات

• يولّد مدخلات مصممة خصيصًا لشفرتك الفعلية
• جمع اختياري لمجموعة المدخلات، وتوجيه الطفرات والتغطية للعثور على أخطاء أعمق
• مدعوم بـ Slither لاستخراج معلومات مفيدة قبل حملة التشويش
• تكامل مع الشفرة المصدرية لتحديد الأسطر التي تمت تغطيتها بعد حملة التشويش
• واجهة طرفية تفاعلية، أو إخراج نصي فقط أو بصيغة JSON
• تصغير تلقائي لحالات الاختبار لفرز سريع
• تكامل سلس في سير عمل التطوير

.. وشعار جميل بدقة عالية مصنوع يدويًا.

الاستخدام

تنفيذ مشغّل الاختبار

تتمثل الوظيفة الأساسية لـ Echidna في ملف تنفيذي يُسمى echidna، يأخذ عقدًا وقائمة من الثوابت (الخصائص التي يجب أن تظل صحيحة دائمًا) كمدخل. لكل ثابت، يولّد تسلسلات عشوائية من الاستدعاءات للعقد ويتحقق مما إذا كان الثابت صحيحًا. إذا تمكن من إيجاد طريقة لدحض الثابت، فإنه يطبع تسلسل الاستدعاءات الذي يفعل ذلك. وإذا لم يتمكن، فلديك بعض الطمأنينة بأن العقد آمن.

كتابة الثوابت

يتم التعبير عن الثوابت كدوال Solidity بأسماء تبدأ بـ echidna_، ولا تأخذ وسائط، وتعيد قيمة منطقية. على سبيل المثال، إذا كان لديك متغير balance يجب ألا ينخفض أبدًا عن 20، يمكنك كتابة دالة إضافية في عقدك مثل هذه:```solidity function echidna_check_balance() public returns (bool) { return(balance >= 20); }

للتحقق من هذه الثوابت، شغّل:```sh
$ echidna myContract.sol

يمكن العثور على مثال لعقد مع اختبارات في tests/solidity/basic/flags.sol. لتشغيله، يجب عليك تنفيذ:```sh $ echidna tests/solidity/basic/flags.sol

يجب أن يجد Echidna تسلسل استدعاء يزيّف `echidna_sometimesfalse` ويجب ألا يتمكن من إيجاد مدخل مزيّف لـ `echidna_alwaystrue`.

### أوضاع الاختبار

يستخدم المثال أعلاه الوضع الافتراضي **property**، لكن Echidna يدعم عدة أوضاع اختبار، تُضبط عبر `testMode` في ملف الإعدادات أو `--test-mode` على سطر الأوامر:

* **`property`** (افتراضي): اختبار الدوال التي تبدأ بـ `echidna_` والتي تُرجع `bool`.
* **`assertion`**: كشف إخفاقات التأكيد من `assert()` ومساعدات `assertX` الخاصة بـ Foundry (`assertTrue`، `assertEq`، إلخ).
* **`foundry`**: تشغيل اختبارات بنمط Foundry، باتباع اصطلاحات التسمية الخاصة به: اختبارات الوحدة والاختبارات العشوائية التي تبدأ بـ `test` (يُتوقع أن تُرجع التي تبدأ بـ `testFail`) والثوابت الحالية التي تبدأ بـ `invariant` أو `statefulFuzz`. الدوال التي تبدأ بـ `check` و `prove` هي نقاط دخول رمزية، لكن بما أن هذا الوضع هو حملة اختبار عشوائي، فإنها تُختبر عشوائياً مثل أي دالة اختبار أخرى.
* **`verification`**: التحقق رمزياً من كل دالة في العقد باستخدام معاملة واحدة. تُستخدم الدوال التي تبدأ بـ `check` و `prove` دائماً كنقاط دخول.
* **`overflow`**: كشف تجاوزات/نقصان الأعداد الصحيحة (Solidity >= 0.8.0).
* **`optimization`**: تعظيم القيمة المُرجعة للدوال التي تبدأ بـ `echidna_` والتي تُرجع `int256` (يستخدم نفس البادئة القابلة للضبط كما في وضع property).
* **`exploration`**: جمع التغطية دون التحقق من الخصائص.

### جمع التغطية وتصوّرها

بعد إنهاء حملة، يمكن لـ Echidna حفظ **corpus** يعظّم التغطية في دليل خاص يُحدد بخيار الإعدادات `corpusDir`. سيحتوي هذا الدليل على مدخلين: (1) دليل باسم `coverage` يحتوي على ملفات JSON يمكن لـ Echidna إعادة تشغيلها و(2) ملف نصي عادي باسم `covered.txt`، وهو نسخة من الشيفرة المصدرية مع تعليقات التغطية.

إذا شغّلت مثال `tests/solidity/basic/flags.sol`، فسيحفظ Echidna بضعة ملفات معاملات مُسلسلة في دليل `coverage` وملف `covered.$(date +%s).txt` بالأسطر التالية:```text
*r  |  function set0(int val) public returns (bool){
*   |    if (val % 100 == 0)
*   |      flag0 = false;
  }

*r  |  function set1(int val) public returns (bool){
*   |    if (val % 10 == 0 && !flag0)
*   |      flag1 = false;
  }

تقوم أداتنا بتمييز كل أثر تنفيذ في المجموعة بعلامة "سطر" التالية:

• * إذا انتهى التنفيذ بـ STOP
• r إذا انتهى التنفيذ بـ REVERT
• o إذا انتهى التنفيذ بخطأ نفاد الغاز
• e إذا انتهى التنفيذ بأي خطأ آخر (قسمة على صفر، فشل تأكيد، إلخ)

دعم أنظمة بناء العقود الذكية

يمكن لـ Echidna اختبار العقود المُجمَّعة باستخدام أنظمة بناء العقود الذكية المختلفة، بما في ذلك Foundry، وHardhat، وTruffle، باستخدام crytic-compile. لاستدعاء Echidna مع إطار التجميع الحالي، استخدم echidna ..

بالإضافة إلى ذلك، تدعم Echidna وضعين لاختبار العقود المعقدة. أولاً، يمكن للمرء الاستفادة من حالة الشبكة الموجودة واستخدامها كحالة أساسية لـ Echidna. ثانياً، يمكن لـ Echidna استدعاء أي عقد بواجهة ABI معروفة عن طريق تمرير مصدر Solidity المقابل في سطر الأوامر. استخدم allContracts: true في إعداداتك لتفعيل هذا.

دورة مكثفة عن Echidna

يحتوي مستودعنا Building Secure Smart Contracts على دورة مكثفة عن Echidna، بما في ذلك أمثلة ودروس وتمارين.

استخدام Echidna في سير عمل GitHub Actions

هناك إجراء Echidna يمكن استخدامه لتشغيل echidna كجزء من سير عمل GitHub Actions. يرجى الرجوع إلى مستودع crytic/echidna-action للحصول على تعليمات الاستخدام والأمثلة.

خيارات الإعدادات

يمكن استخدام واجهة سطر أوامر Echidna لاختيار العقد المراد اختباره وتحميل ملف الإعدادات.```sh $ echidna contract.sol --contract TEST --config config.yaml

يسمح ملف التكوين للمستخدمين باختيار معاملات EVM وتوليد الاختبارات. يمكن العثور على مثال لملف تكوين كامل ومُعلّق مع الخيارات الافتراضية في
[tests/solidity/basic/default.yaml](https://github.com/crytic/echidna/blob/master/tests/solidity/basic/default.yaml).
راجع [التوثيق](https://secure-contracts.com/program-analysis/echidna/configuration.html)
للحصول على معلومات أكثر تفصيلاً حول خيارات التكوين المتاحة.

يدعم Echidna ثلاثة برامج تشغيل مختلفة للإخراج. هناك برنامج التشغيل الافتراضي `text`،
وبرنامج التشغيل `json`، وبرنامج التشغيل `none`، الذي ينبغي أن يمنع كل
إخراج `stdout`. يُبلّغ برنامج تشغيل JSON عن الحملة الإجمالية على النحو التالي.```
Campaign = {
  "success"      : bool,
  "error"        : string?,
  "tests"        : [Test],
  "seed"         : number,
  "coverage"     : Coverage
}
Test = {
  "contract"     : string,
  "name"         : string,
  "status"       : string,
  "error"        : string?,
  "testType"     : string,
  "transactions" : [Transaction]?
}
Transaction = {
  "contract"     : string,
  "function"     : string,
  "arguments"    : [string]?,
  "gas"          : number,
  "gasprice"     : number
}

Coverage هو dict يصف بعض الاستدعاءات التي تزيد التغطية. هذه الواجهات قابلة للتغيير لتكون أكثر ملاءمة للمستخدم قليلاً في تاريخ لاحق. ستكون testType واحدة من property، assertion، optimization، exploration، أو call، و status تأخذ دائمًا إما fuzzing، shrinking، solved، passed، أو error.

تصحيح مشاكل الأداء