मुख्य सामग्री पर जाएं

स्मार्ट अनुबंधों का परीक्षण करने के लिए एकिड्ना (Echidna) का उपयोग कैसे करें

Solidity
स्मार्ट अनुबंध
सुरक्षा
परीक्षण
फ़ज़िंग
उन्नत
Trailofbits
10 अप्रैल 2020
15 मिनट पढ़ें

इंस्टॉलेशन

एकिड्ना को Docker के माध्यम से या पूर्व-संकलित (pre-compiled) बाइनरी का उपयोग करके इंस्टॉल किया जा सकता है।

Docker के माध्यम से एकिड्ना

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

अंतिम कमांड एक Docker में eth-security-toolbox चलाता है जिसकी पहुंच आपकी वर्तमान डायरेक्टरी तक होती है। आप अपने होस्ट से फ़ाइलें बदल सकते हैं, और 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) एक प्रसिद्ध तकनीक है। इसमें प्रोग्राम में बग खोजने के लिए ऐसे इनपुट उत्पन्न करना शामिल है जो कमोबेश यादृच्छिक (random) होते हैं। पारंपरिक सॉफ़्टवेयर के लिए फ़ज़र (जैसे AFL (opens in a new tab) या LibFuzzer (opens in a new tab)) बग खोजने के लिए कुशल टूल माने जाते हैं।

इनपुट के विशुद्ध रूप से यादृच्छिक निर्माण के अलावा, अच्छे इनपुट उत्पन्न करने के लिए कई तकनीकें और रणनीतियां हैं, जिनमें शामिल हैं:

  • प्रत्येक निष्पादन (execution) से फीडबैक प्राप्त करना और उसका उपयोग करके निर्माण का मार्गदर्शन करना। उदाहरण के लिए, यदि कोई नया उत्पन्न इनपुट किसी नए पथ की खोज की ओर ले जाता है, तो उसके करीब नए इनपुट उत्पन्न करना समझदारी हो सकती है।
  • संरचनात्मक बाधा (structural constraint) का सम्मान करते हुए इनपुट उत्पन्न करना। उदाहरण के लिए, यदि आपके इनपुट में चेकसम के साथ एक हेडर है, तो फ़ज़र को चेकसम को मान्य करने वाला इनपुट उत्पन्न करने देना उचित होगा।
  • नए इनपुट उत्पन्न करने के लिए ज्ञात इनपुट का उपयोग करना: यदि आपके पास मान्य इनपुट के एक बड़े डेटासेट तक पहुंच है, तो आपका फ़ज़र शुरुआत से निर्माण करने के बजाय उनसे नए इनपुट उत्पन्न कर सकता है। इन्हें आमतौर पर सीड्स (seeds) कहा जाता है।

प्रॉपर्टी-आधारित फ़ज़िंग

एकिड्ना फ़ज़र के एक विशिष्ट परिवार से संबंधित है: प्रॉपर्टी-आधारित फ़ज़िंग जो QuickCheck (opens in a new tab) से काफी प्रेरित है। क्लासिक फ़ज़र के विपरीत जो क्रैश खोजने का प्रयास करेगा, एकिड्ना उपयोगकर्ता-परिभाषित इनवेरिएंट्स (invariants) को तोड़ने का प्रयास करेगा।

स्मार्ट अनुबंधों में, इनवेरिएंट्स Solidity फ़ंक्शन होते हैं, जो किसी भी गलत या अमान्य स्थिति का प्रतिनिधित्व कर सकते हैं जहां अनुबंध पहुंच सकता है, जिनमें शामिल हैं:

  • गलत एक्सेस कंट्रोल: हमलावर अनुबंध का मालिक बन गया।
  • गलत स्थिति मशीन: अनुबंध के रुके (paused) होने पर भी टोकन ट्रांसफर किए जा सकते हैं।
  • गलत अंकगणित: उपयोगकर्ता अपने बैलेंस को अंडरफ़्लो कर सकता है और असीमित मुफ्त टोकन प्राप्त कर सकता है।

एकिड्ना के साथ प्रॉपर्टी का परीक्षण करना

हम देखेंगे कि एकिड्ना के साथ स्मार्ट अनुबंध का परीक्षण कैसे करें। लक्ष्य निम्नलिखित स्मार्ट अनुबंध token.sol (opens in a new tab) है:

हम यह मानकर चलेंगे कि इस टोकन में निम्नलिखित प्रॉपर्टीज़ होनी चाहिए:

  • किसी के पास भी अधिकतम 1000 टोकन हो सकते हैं
  • टोकन को ट्रांसफर नहीं किया जा सकता (यह ERC-20 टोकन नहीं है)

एक प्रॉपर्टी लिखें

एकिड्ना प्रॉपर्टीज़ Solidity फ़ंक्शन हैं। एक प्रॉपर्टी में यह होना चाहिए:

  • कोई तर्क (argument) न हो
  • यदि यह सफल होता है तो true लौटाएं
  • इसका नाम echidna से शुरू होना चाहिए

एकिड्ना करेगा:

  • प्रॉपर्टी का परीक्षण करने के लिए स्वचालित रूप से मनमाने लेन-देन उत्पन्न करेगा।
  • किसी भी ऐसे लेन-देन की रिपोर्ट करेगा जिसके कारण प्रॉपर्टी false लौटाती है या कोई त्रुटि (error) फेंकती है।
  • प्रॉपर्टी को कॉल करते समय साइड-इफेक्ट को छोड़ देगा (यानी, यदि प्रॉपर्टी किसी स्थिति चर (state variable) को बदलती है, तो परीक्षण के बाद इसे छोड़ दिया जाता है)

निम्नलिखित प्रॉपर्टी जांचती है कि कॉलर के पास 1000 से अधिक टोकन नहीं हैं:

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

अपने अनुबंध को अपनी प्रॉपर्टीज़ से अलग करने के लिए इनहेरिटेंस (inheritance) का उपयोग करें:

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

token.sol (opens in a new tab) प्रॉपर्टी को लागू करता है और टोकन से इनहेरिट करता है।

अनुबंध प्रारंभ करें

एकिड्ना को बिना तर्क वाले कंस्ट्रक्टर की आवश्यकता होती है। यदि आपके अनुबंध को एक विशिष्ट इनिशियलाइज़ेशन की आवश्यकता है, तो आपको इसे कंस्ट्रक्टर में करना होगा।

एकिड्ना में कुछ विशिष्ट पते (addresses) हैं:

  • 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 जो कंस्ट्रक्टर को कॉल करता है।
  • 0x10000, 0x20000, और 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 जो यादृच्छिक रूप से अन्य फ़ंक्शंस को कॉल करते हैं।

हमें अपने वर्तमान उदाहरण में किसी विशेष इनिशियलाइज़ेशन की आवश्यकता नहीं है, परिणामस्वरूप हमारा कंस्ट्रक्टर खाली है।

एकिड्ना चलाएं

एकिड्ना को इसके साथ लॉन्च किया जाता है:

echidna-test contract.sol

यदि contract.sol में कई अनुबंध हैं, तो आप लक्ष्य निर्दिष्ट कर सकते हैं:

echidna-test contract.sol --contract MyContract

सारांश: प्रॉपर्टी का परीक्षण

निम्नलिखित हमारे उदाहरण पर एकिड्ना के रन का सारांश देता है:

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

एकिड्ना ने पाया कि यदि backdoor को कॉल किया जाता है तो प्रॉपर्टी का उल्लंघन होता है।

फ़ज़िंग अभियान के दौरान कॉल करने के लिए फ़ंक्शंस को फ़िल्टर करना

हम देखेंगे कि फ़ज़ किए जाने वाले फ़ंक्शंस को कैसे फ़िल्टर किया जाए। लक्ष्य निम्नलिखित स्मार्ट अनुबंध है:

यह छोटा उदाहरण एकिड्ना को स्थिति चर को बदलने के लिए लेन-देन का एक निश्चित क्रम खोजने के लिए मजबूर करता है। यह एक फ़ज़र के लिए कठिन है (यह अनुशंसा की जाती है कि मैन्टिकोर (opens in a new tab) जैसे सिम्बोलिक निष्पादन टूल का उपयोग करें)। हम इसे सत्यापित करने के लिए एकिड्ना चला सकते हैं:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

फ़ंक्शंस को फ़िल्टर करना

एकिड्ना को इस अनुबंध का परीक्षण करने के लिए सही क्रम खोजने में परेशानी होती है क्योंकि दो रीसेट फ़ंक्शन (reset1 और reset2) सभी स्थिति चरों को false पर सेट कर देंगे। हालाँकि, हम रीसेट फ़ंक्शन को ब्लैकलिस्ट करने या केवल f, g, h और i फ़ंक्शंस को व्हाइटलिस्ट करने के लिए एक विशेष एकिड्ना सुविधा का उपयोग कर सकते हैं।

फ़ंक्शंस को ब्लैकलिस्ट करने के लिए, हम इस कॉन्फ़िगरेशन फ़ाइल का उपयोग कर सकते हैं:

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

फ़ंक्शंस को फ़िल्टर करने का एक अन्य तरीका व्हाइटलिस्ट किए गए फ़ंक्शंस को सूचीबद्ध करना है। ऐसा करने के लिए, हम इस कॉन्फ़िगरेशन फ़ाइल का उपयोग कर सकते हैं:

filterBlacklist: false
filterFunctions: ["f", "g", "h", "i"]
  • filterBlacklist डिफ़ॉल्ट रूप से true है।
  • फ़िल्टरिंग केवल नाम से (बिना पैरामीटर के) की जाएगी। यदि आपके पास f() और f(uint256) हैं, तो फ़िल्टर "f" दोनों फ़ंक्शंस से मेल खाएगा।

एकिड्ना चलाएं

कॉन्फ़िगरेशन फ़ाइल blacklist.yaml के साथ एकिड्ना चलाने के लिए:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

एकिड्ना लगभग तुरंत ही प्रॉपर्टी को गलत साबित करने के लिए लेन-देन का क्रम खोज लेगा।

सारांश: फ़ंक्शंस को फ़िल्टर करना

एकिड्ना फ़ज़िंग अभियान के दौरान कॉल करने के लिए फ़ंक्शंस को ब्लैकलिस्ट या व्हाइटलिस्ट कर सकता है, इसका उपयोग करके:

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

एकिड्ना filterBlacklist बूलियन के मान के अनुसार, या तो f1, f2 और f3 को ब्लैकलिस्ट करके या केवल इन्हें कॉल करके फ़ज़िंग अभियान शुरू करता है।

एकिड्ना के साथ Solidity के दावे (assert) का परीक्षण कैसे करें

इस छोटे ट्यूटोरियल में, हम यह दिखाने जा रहे हैं कि अनुबंधों में दावा (assertion) जांच का परीक्षण करने के लिए एकिड्ना का उपयोग कैसे करें। मान लीजिए कि हमारे पास इस तरह का एक अनुबंध है:

एक दावा (assertion) लिखें

हम यह सुनिश्चित करना चाहते हैं कि इसका अंतर लौटाने के बाद tmp, counter से कम या उसके बराबर हो। हम एक एकिड्ना प्रॉपर्टी लिख सकते हैं, लेकिन हमें tmp मान को कहीं स्टोर करने की आवश्यकता होगी। इसके बजाय, हम इस तरह के दावे का उपयोग कर सकते हैं:

एकिड्ना चलाएं

दावा विफलता परीक्षण को सक्षम करने के लिए, एक एकिड्ना कॉन्फ़िगरेशन फ़ाइल (opens in a new tab) config.yaml बनाएं:

checkAsserts: true

जब हम इस अनुबंध को एकिड्ना में चलाते हैं, तो हमें अपेक्षित परिणाम प्राप्त होते हैं:

जैसा कि आप देख सकते हैं, एकिड्ना inc फ़ंक्शन में कुछ दावा विफलता की रिपोर्ट करता है। प्रति फ़ंक्शन एक से अधिक दावे जोड़ना संभव है, लेकिन एकिड्ना यह नहीं बता सकता कि कौन सा दावा विफल रहा।

दावों का उपयोग कब और कैसे करें

दावों का उपयोग स्पष्ट प्रॉपर्टीज़ के विकल्प के रूप में किया जा सकता है, विशेष रूप से यदि जांच की जाने वाली शर्तें सीधे किसी ऑपरेशन f के सही उपयोग से संबंधित हैं। कुछ कोड के बाद दावे जोड़ने से यह लागू होगा कि इसके निष्पादित होने के तुरंत बाद जांच होगी:

function f(..) public {
    // कुछ जटिल कोड
    ...
    assert (condition);
    ...
}

इसके विपरीत, एक स्पष्ट एकिड्ना प्रॉपर्टी का उपयोग करने से लेन-देन यादृच्छिक रूप से निष्पादित होंगे और यह लागू करने का कोई आसान तरीका नहीं है कि इसकी जांच कब की जाएगी। यह वर्कअराउंड करना अभी भी संभव है:

function echidna_assert_after_f() public returns (bool) {
    f(..);
    return(condition);
}

हालाँकि, कुछ समस्याएं हैं:

  • यह विफल हो जाता है यदि f को internal या external के रूप划 में घोषित किया गया है।
  • यह स्पष्ट नहीं है कि f को कॉल करने के लिए किन तर्कों का उपयोग किया जाना चाहिए।
  • यदि f रिवर्ट होता है, तो प्रॉपर्टी विफल हो जाएगी।

सामान्य तौर पर, हम दावों का उपयोग करने के तरीके पर John Regehr की अनुशंसा (opens in a new tab) का पालन करने की सलाह देते हैं:

  • दावा जांच के दौरान किसी भी साइड इफेक्ट को मजबूर न करें। उदाहरण के लिए: assert(ChangeStateAndReturn() == 1)
  • स्पष्ट कथनों का दावा न करें। उदाहरण के लिए assert(var >= 0) जहां var को uint के रूप में घोषित किया गया है।

अंत में, कृपया assert के बजाय require का उपयोग न करें, क्योंकि एकिड्ना इसका पता लगाने में सक्षम नहीं होगा (लेकिन अनुबंध वैसे भी रिवर्ट हो जाएगा)।

सारांश: दावा जांच

निम्नलिखित हमारे उदाहरण पर एकिड्ना के रन का सारांश देता है:

एकिड्ना ने पाया कि inc में दावा विफल हो सकता है यदि इस फ़ंक्शन को बड़े तर्कों के साथ कई बार कॉल किया जाता है।

एकिड्ना कॉर्पस (corpus) एकत्र करना और संशोधित करना

हम देखेंगे कि एकिड्ना के साथ लेन-देन का कॉर्पस कैसे एकत्र करें और उसका उपयोग कैसे करें। लक्ष्य निम्नलिखित स्मार्ट अनुबंध magic.sol (opens in a new tab) है:

यह छोटा उदाहरण एकिड्ना को स्थिति चर को बदलने के लिए कुछ मान खोजने के लिए मजबूर करता है। यह एक फ़ज़र के लिए कठिन है (यह अनुशंसा की जाती है कि मैन्टिकोर (opens in a new tab) जैसे सिम्बोलिक निष्पादन टूल का उपयोग करें)। हम इसे सत्यापित करने के लिए एकिड्ना चला सकते हैं:

echidna-test magic.sol
...

echidna_magic_values: passed! 🎉

Seed: 2221503356319272685

हालाँकि, हम अभी भी इस फ़ज़िंग अभियान को चलाते समय कॉर्पस एकत्र करने के लिए एकिड्ना का उपयोग कर सकते हैं।

कॉर्पस एकत्र करना

कॉर्पस संग्रह को सक्षम करने के लिए, एक कॉर्पस डायरेक्टरी बनाएं:

mkdir corpus-magic

और एक एकिड्ना कॉन्फ़िगरेशन फ़ाइल (opens in a new tab) config.yaml:

coverage: true
corpusDir: "corpus-magic"

अब हम अपना टूल चला सकते हैं और एकत्र किए गए कॉर्पस की जांच कर सकते हैं:

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

एकिड्ना अभी भी सही मैजिक मान नहीं खोज सकता है, लेकिन हम इसके द्वारा एकत्र किए गए कॉर्पस पर एक नज़र डाल सकते हैं। उदाहरण के लिए, इनमें से एक फ़ाइल थी:

स्पष्ट रूप से, यह इनपुट हमारी प्रॉपर्टी में विफलता को ट्रिगर नहीं करेगा। हालाँकि, अगले चरण में, हम देखेंगे कि इसके लिए इसे कैसे संशोधित किया जाए।

कॉर्पस को सीड (seed) करना

एकिड्ना को magic फ़ंक्शन से निपटने के लिए कुछ मदद की आवश्यकता है। हम इसके लिए उपयुक्त मापदंडों का उपयोग करने के लिए इनपुट को कॉपी और संशोधित करने जा रहे हैं:

cp corpus/2712688662897926208.txt corpus/new.txt

हम magic(42,129,333,0) को कॉल करने के लिए new.txt को संशोधित करेंगे। अब, हम एकिड्ना को फिर से चला सकते हैं:

इस बार, इसने पाया कि प्रॉपर्टी का तुरंत उल्लंघन हो गया है।

उच्च गैस खपत वाले लेन-देन खोजना

हम देखेंगे कि एकिड्ना के साथ उच्च गैस खपत वाले लेन-देन कैसे खोजें। लक्ष्य निम्नलिखित स्मार्ट अनुबंध है:

यहां expensive में गैस की खपत अधिक हो सकती है।

वर्तमान में, एकिड्ना को परीक्षण के लिए हमेशा एक प्रॉपर्टी की आवश्यकता होती है: यहां echidna_test हमेशा true लौटाता है। हम इसे सत्यापित करने के लिए एकिड्ना चला सकते हैं:

echidna-test gas.sol
...
echidna_test: passed! 🎉

Seed: 2320549945714142710

गैस खपत मापना

एकिड्ना के साथ गैस खपत को सक्षम करने के लिए, एक कॉन्फ़िगरेशन फ़ाइल config.yaml बनाएं:

estimateGas: true

इस उदाहरण में, हम परिणामों को समझने में आसान बनाने के लिए लेन-देन अनुक्रम के आकार को भी कम करेंगे:

seqLen: 2
estimateGas: true

एकिड्ना चलाएं

एक बार जब हम कॉन्फ़िगरेशन फ़ाइल बना लेते हैं, तो हम एकिड्ना को इस तरह चला सकते हैं:

  • दिखाई गई गैस HEVM (opens in a new tab) द्वारा प्रदान किया गया एक अनुमान है।

गैस कम करने वाले कॉल्स को फ़िल्टर करना

ऊपर फ़ज़िंग अभियान के दौरान कॉल करने के लिए फ़ंक्शंस को फ़िल्टर करना पर ट्यूटोरियल दिखाता है कि आपके परीक्षण से कुछ फ़ंक्शंस को कैसे हटाया जाए।
सटीक गैस अनुमान प्राप्त करने के लिए यह महत्वपूर्ण हो सकता है। निम्नलिखित उदाहरण पर विचार करें:

यदि एकिड्ना सभी फ़ंक्शंस को कॉल कर सकता है, तो यह आसानी से उच्च गैस लागत वाले लेन-देन नहीं खोज पाएगा:

ऐसा इसलिए है क्योंकि लागत addrs के आकार पर निर्भर करती है और यादृच्छिक कॉल्स एरे (array) को लगभग खाली छोड़ देते हैं। हालाँकि, pop और clear को ब्लैकलिस्ट करने से हमें बहुत बेहतर परिणाम मिलते हैं:

filterBlacklist: true
filterFunctions: ["pop", "clear"]
echidna-test pushpop.sol --config config.yaml
...
push used a maximum of 40839 gas
...
check used a maximum of 1484472 gas

सारांश: उच्च गैस खपत वाले लेन-देन खोजना

एकिड्ना estimateGas कॉन्फ़िगरेशन विकल्प का उपयोग करके उच्च गैस खपत वाले लेन-देन खोज सकता है:

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

फ़ज़िंग अभियान समाप्त होने के बाद, एकिड्ना प्रत्येक फ़ंक्शन के लिए अधिकतम गैस खपत वाले अनुक्रम की रिपोर्ट करेगा।