تخطٍ إلى المحتوى الرئيسي

كيفية استخدام إيكيدنا لاختبار العقود الذكية

Solidity
العقود الذكيه
الأمن
الاختبار
التشويش
إعدادات متقدمة
Trailofbits
10 أبريل 2020
12 دقيقة قراءة

التثبيت

يمكن تثبيت إيكيدنا من خلال docker أو باستخدام الملف الثنائي المترجم مسبقًا.

إيكيدنا من خلال docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

الأمر الأخير يشغل eth-security-toolbox في حاوية docker لديها صلاحية الوصول إلى دليلك الحالي. يمكنك تغيير الملفات من مضيفك، وتشغيل الأدوات على الملفات من حاوية docker

داخل docker، قم بتشغيل:

solc-select 0.5.11
cd /home/training

ثنائي

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

مقدمة عن التشويش القائم على الخصائص

إيكيدنا هي أداة تشويش قائمة على الخصائص، كما وصفنا في منشورات مدونتنا السابقة (1 (opens in a new tab)، 2 (opens in a new tab)، 3 (opens in a new tab)).

التشويش

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

إلى جانب التوليد العشوائي البحت للمدخلات، هناك العديد من التقنيات والاستراتيجيات لتوليد مدخلات جيدة، بما في ذلك:

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

التشويش القائم على الخصائص

تنتمي إيكيدنا إلى عائلة معينة من أدوات التشويش: التشويش القائم على الخصائص المستوحى بشكل كبير من QuickCheck (opens in a new tab). على عكس أداة التشويش الكلاسيكية التي ستحاول العثور على أعطال، ستحاول إيكيدنا كسر الثوابت المحددة من قبل المستخدم.

في العقود الذكية، الثوابت هي وظائف سوليديتي، والتي يمكن أن تمثل أي حالة غير صحيحة أو غير صالحة يمكن أن يصل إليها العقد، بما في ذلك:

  • تحكم غير صحيح في الوصول: أصبح المهاجم مالك العقد.
  • آلة حالة غير صحيحة: يمكن نقل الرموز أثناء إيقاف العقد مؤقتًا.
  • عملية حسابية غير صحيحة: يمكن للمستخدم أن يتسبب في تدفق سفلي لرصيده ويحصل على رموز مجانية غير محدودة.

اختبار خاصية باستخدام إيكيدنا

سنرى كيفية اختبار عقد ذكي باستخدام إيكيدنا. الهدف هو العقد الذكي التالي token.sol (opens in a new tab):

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}

سنفترض أن هذا الرمز يجب أن يتمتع بالخصائص التالية:

  • يمكن لأي شخص امتلاك 1000 رمز كحد أقصى
  • لا يمكن نقل الرمز (إنه ليس رمز ERC20)

كتابة خاصية

خصائص إيكيدنا هي وظائف سوليديتي. يجب أن تستوفي الخاصية ما يلي:

  • ألا تحتوي على وسيطة
  • إرجاع true إذا كانت ناجحة
  • أن يبدأ اسمها بـ echidna

ستقوم إيكيدنا بما يلي:

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

تتحقق الخاصية التالية من أن المتصل لا يملك أكثر من 1000 رمز:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}

استخدم الوراثة لفصل عقدك عن خصائصك:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }

token.sol (opens in a new tab) ينفذ الخاصية ويرث من الرمز.

تهيئة عقد

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

هناك بعض العناوين المحددة في إيكيدنا:

  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 الذي يستدعي دالة البناء.
  • 0x10000 و 0x20000 و 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 التي تستدعي الوظائف الأخرى بشكل عشوائي.

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

تشغيل إيكيدنا

يتم تشغيل إيكيدنا باستخدام:

echidna-test contract.sol

إذا كان contract.sol يحتوي على عقود متعددة، يمكنك تحديد الهدف:

echidna-test contract.sol --contract MyContract

ملخص: اختبار خاصية

يلخص ما يلي تشغيل echidna على مثالنا:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
echidna-test testtoken.sol --contract TestToken
...


echidna_balance_under_1000: فشلت!💥
  تسلسل الاستدعاء، التقليص (1205/5000):
    airdrop()
    backdoor()


...

وجدت إيكيدنا أن الخاصية تُنتهك إذا تم استدعاء backdoor.

تصفية الوظائف التي سيتم استدعاؤها أثناء حملة التشويش

سنرى كيفية تصفية الوظائف التي سيتم تشويشها. الهدف هو العقد الذكي التالي:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6

7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11

12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17

18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23

24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28

29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35

36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42

43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}

يجبر هذا المثال الصغير إيكيدنا على العثور على تسلسل معين من المعاملات لتغيير متغير الحالة. هذا صعب على أداة التشويش (يوصى باستخدام أداة تنفيذ رمزي مثل مانتيكور (opens in a new tab)). يمكننا تشغيل إيكيدنا للتحقق من هذا:

echidna-test multi.sol
...
echidna_state4: نجحت! 🎉
Seed: -3684648582249875403

تصفية الوظائف

تواجه إيكيدنا صعوبة في العثور على التسلسل الصحيح لاختبار هذا العقد لأن وظيفتي إعادة الضبط (reset1 و reset2) ستعينان جميع متغيرات الحالة على false. ومع ذلك، يمكننا استخدام ميزة إيكيدنا خاصة إما لوضع وظيفة إعادة الضبط في القائمة السوداء أو لوضع وظائف f و g و h و i فقط في القائمة البيضاء.

لوضع الوظائف في القائمة السوداء، يمكننا استخدام ملف التكوين هذا:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

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

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]
  • filterBlacklist هي true بشكل افتراضي.
  • سيتم إجراء التصفية بالاسم فقط (بدون معلمات). إذا كان لديك f() و f(uint256)، فإن المرشح "f" سيطابق كلتا الوظيفتين.

تشغيل إيكيدنا

لتشغيل إيكيدنا باستخدام ملف تكوين blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: فشلت!💥
  تسلسل الاستدعاء:
    f(12)
    g(8)
    h(42)
    i()

ستجد إيكيدنا تسلسل المعاملات لتكذيب الخاصية على الفور تقريبًا.

ملخص: تصفية الوظائف

يمكن لـ إيكيدنا إما وضع وظائف في القائمة السوداء أو في القائمة البيضاء لاستدعائها أثناء حملة التشويش باستخدام:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]
echidna-test contract.sol --config config.yaml
...

تبدأ إيكيدنا حملة تشويش إما بوضع f1 و f2 و f3 في القائمة السوداء أو باستدعاء هذه الوظائف فقط، وفقًا لقيمة filterBlacklist المنطقية.

كيفية اختبار تأكيد سوليديتي باستخدام إيكيدنا

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

1contract Incrementor {
2  uint private counter = 2**200;
3

4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp أصغر من أو يساوي counter
8    return (counter - tmp);
9  }
10}

كتابة تأكيد

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

1contract Incrementor {
2  uint private counter = 2**200;
3

4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}

تشغيل إيكيدنا

لتمكين اختبار فشل التأكيد، قم بإنشاء ملف تكوين إيكيدنا (opens in a new tab) config.yaml:

1checkAsserts: true

عندما نقوم بتشغيل هذا العقد في إيكيدنا، نحصل على النتائج المتوقعة:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: فشل!💥
  تسلسل الاستدعاء، التقليص (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)


Seed: 1806480648350826486

كما ترى، تبلغ إيكيدنا عن بعض حالات فشل التأكيد في وظيفة inc. إضافة أكثر من تأكيد واحد لكل وظيفة أمر ممكن، لكن إيكيدنا لا تستطيع تحديد أي تأكيد فشل.

متى وكيف تستخدم التأكيدات

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

1function f(..) public {
2    // بعض التعليمات البرمجية المعقدة
3    ...
4    assert (condition);
5    ...
6}
7

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

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}

ومع ذلك، هناك بعض المشاكل:

  • يفشل إذا تم الإعلان عن f على أنها internal أو external.
  • من غير الواضح ما هي الوسيطات التي يجب استخدامها لاستدعاء f.
  • إذا تم عكس f، فستفشل الخاصية.

بشكل عام، نوصي باتباع توصية جون ريجير (opens in a new tab) حول كيفية استخدام التأكيدات:

  • لا تفرض أي تأثير جانبي أثناء فحص التأكيد. على سبيل المثال: assert(ChangeStateAndReturn() == 1)
  • لا تؤكد العبارات الواضحة. على سبيل المثال assert(var >= 0) حيث يتم الإعلان عن var كـ uint.

أخيرًا، يرجى عدم استخدام require بدلاً من assert، لأن إيكيدنا لن تتمكن من اكتشافه (لكن العقد سيعود على أي حال).

ملخص: فحص التأكيد

يلخص ما يلي تشغيل echidna على مثالنا:

1contract Incrementor {
2  uint private counter = 2**200;
3

4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: فشل!💥
  تسلسل الاستدعاء، التقليص (2596/5000):
    inc(21711016731996786641919559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)


Seed: 1806480648350826486

وجدت إيكيدنا أن التأكيد في inc يمكن أن يفشل إذا تم استدعاء هذه الوظيفة عدة مرات بوسيطات كبيرة.

جمع وتعديل مجموعة بيانات إيكيدنا

سنرى كيفية جمع واستخدام مجموعة بيانات من المعاملات مع إيكيدنا. الهدف هو العقد الذكي التالي magic.sol (opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10

11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14

15}

يجبر هذا المثال الصغير إيكيدنا على العثور على قيم معينة لتغيير متغير الحالة. هذا صعب على أداة التشويش (يوصى باستخدام أداة تنفيذ رمزي مثل مانتيكور (opens in a new tab)). يمكننا تشغيل إيكيدنا للتحقق من هذا:

echidna-test magic.sol
...


echidna_magic_values: نجحت! 🎉


Seed: 2221503356319272685

ومع ذلك، لا يزال بإمكاننا استخدام إيكيدنا لجمع مجموعة بيانات عند تشغيل حملة التشويش هذه.

جمع مجموعة بيانات

لتمكين جمع مجموعة البيانات، قم بإنشاء دليل مجموعة البيانات:

mkdir corpus-magic

وملف تكوين إيكيدنا إيكيدنا configuration file (opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

الآن يمكننا تشغيل أداتنا والتحقق من مجموعة البيانات التي تم جمعها:

echidna-test magic.sol --config config.yaml

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

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]

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

تلقيم مجموعة بيانات

تحتاج إيكيدنا إلى بعض المساعدة للتعامل مع وظيفة magic. سنقوم بنسخ وتعديل المدخلات لاستخدام معلمات مناسبة لها:

cp corpus/2712688662897926208.txt corpus/new.txt

سنقوم بتعديل new.txt لاستدعاء magic(42,129,333,0). الآن، يمكننا إعادة تشغيل إيكيدنا:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: فشلت!💥
  تسلسل الاستدعاء:
    magic(42,129,333,0)


Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537

هذه المرة، وجدت أن الخاصية قد انتهكت على الفور.

العثور على المعاملات ذات الاستهلاك العالي للغاز

سنرى كيفية العثور على المعاملات ذات الاستهلاك العالي للغاز باستخدام إيكيدنا. الهدف هو العقد الذكي التالي:

1contract C {
2  uint state;
3

4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8

9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15

16  function echidna_test() public returns (bool) {
17    return true;
18  }
19

20}

هنا يمكن أن يكون لـ expensive استهلاك كبير للغاز.

حاليًا، تحتاج إيكيدنا دائمًا إلى خاصية لاختبارها: هنا echidna_test تُرجع دائمًا true. يمكننا تشغيل إيكيدنا للتحقق من هذا:

1echidna-test gas.sol
2...
3echidna_test: نجحت! 🎉
4

5Seed: 2320549945714142710

قياس استهلاك الغاز

لتمكين استهلاك الغاز مع إيكيدنا، قم بإنشاء ملف تكوين config.yaml:

1estimateGas: true

في هذا المثال، سنقوم أيضًا بتقليل حجم تسلسل المعاملات لجعل النتائج أسهل في الفهم:

1seqLen: 2
2estimateGas: true

تشغيل إيكيدنا

بمجرد إنشاء ملف التكوين، يمكننا تشغيل إيكيدنا على هذا النحو:

echidna-test gas.sol --config config.yaml
...
echidna_test: نجحت! 🎉


f استخدمت حدًا أقصى من الغاز يبلغ 1333608
  تسلسل الاستدعاء:
    f(42,123,249) سعر الغاز: 0x10d5733f0a تأخير زمني: 0x495e5 تأخير الكتلة: 0x88b2


Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325

تصفية استدعاءات خفض الغاز

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

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}

إذا تمكنت إيكيدنا من استدعاء جميع الوظائف، فلن تجد بسهولة المعاملات ذات تكلفة الغاز المرتفعة:

1echidna-test pushpop.sol --config config.yaml
2...
3pop استخدمت حدًا أقصى من الغاز يبلغ 10746
4...
5check استخدمت حدًا أقصى من الغاز يبلغ 23730
6...
7clear استخدمت حدًا أقصى من الغاز يبلغ 35916
8...
9push استخدمت حدًا أقصى من الغاز يبلغ 40839

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

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]
1echidna-test pushpop.sol --config config.yaml
2...
3push استخدمت حدًا أقصى من الغاز يبلغ 40839
4...
5check استخدمت حدًا أقصى من الغاز يبلغ 1484472

ملخص: العثور على المعاملات ذات الاستهلاك العالي للغاز

يمكن لـ إيكيدنا العثور على معاملات ذات استهلاك عالٍ للغاز باستخدام خيار التكوين estimateGas:

1estimateGas: true
echidna-test contract.sol --config config.yaml
...

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

آخر تحديث للصفحة: 3 مارس 2026

myelinated-wackerowm (opens in a new tab)
pete-vielhaberp (opens in a new tab)
nhszn (opens in a new tab)
+10

هل كانت تعليمات الاستخدام هذه مفيدة؟