मुख्य आशयावर जा

स्मार्ट कॉन्ट्रॅक्ट्सची चाचणी करण्यासाठी एकिडना कसे वापरावे

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 (नवीन टॅबमध्ये उघडते)

प्रॉपर्टी-आधारित फझिंगची ओळख

एकिडना हा एक प्रॉपर्टी-आधारित फझर आहे, ज्याचे वर्णन आम्ही आमच्या मागील ब्लॉगपोस्ट्समध्ये केले आहे (1 (नवीन टॅबमध्ये उघडते), 2 (नवीन टॅबमध्ये उघडते), 3 (नवीन टॅबमध्ये उघडते)).

फझिंग

फझिंग (नवीन टॅबमध्ये उघडते) हे सुरक्षा समुदायातील एक सुप्रसिद्ध तंत्र आहे. प्रोग्राममधील बग्स शोधण्यासाठी कमी-अधिक प्रमाणात यादृच्छिक (random) इनपुट्स तयार करणे यात समाविष्ट असते. पारंपारिक सॉफ्टवेअरसाठीचे फझर्स (जसे की AFL (नवीन टॅबमध्ये उघडते) किंवा LibFuzzer (नवीन टॅबमध्ये उघडते)) बग्स शोधण्यासाठी कार्यक्षम टूल्स म्हणून ओळखले जातात.

केवळ यादृच्छिक इनपुट्स तयार करण्यापलीकडे, चांगले इनपुट्स तयार करण्यासाठी अनेक तंत्रे आणि धोरणे आहेत, ज्यामध्ये खालील गोष्टींचा समावेश आहे:

  • प्रत्येक अंमलबजावणीतून फीडबॅक मिळवणे आणि त्याचा वापर करून निर्मितीला मार्गदर्शन करणे. उदाहरणार्थ, जर नव्याने तयार केलेल्या इनपुटमुळे नवीन मार्गाचा शोध लागला, तर त्याच्या जवळचे नवीन इनपुट्स तयार करणे अर्थपूर्ण ठरू शकते.
  • संरचनात्मक मर्यादांचे पालन करून इनपुट तयार करणे. उदाहरणार्थ, जर तुमच्या इनपुटमध्ये चेकसमसह हेडर असेल, तर फझरला चेकसम प्रमाणित करणारे इनपुट तयार करू देणे अर्थपूर्ण ठरेल.
  • नवीन इनपुट्स तयार करण्यासाठी ज्ञात इनपुट्स वापरणे: जर तुमच्याकडे वैध इनपुटच्या मोठ्या डेटासेटचा अ‍ॅक्सेस असेल, तर तुमचा फझर शून्यापासून सुरुवात करण्याऐवजी त्यातून नवीन इनपुट्स तयार करू शकतो. यांना सहसा सीड्स (seeds) म्हटले जाते.

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

एकिडना फझरच्या एका विशिष्ट कुटुंबातील आहे: प्रॉपर्टी-आधारित फझिंग जे QuickCheck (नवीन टॅबमध्ये उघडते) द्वारे मोठ्या प्रमाणावर प्रेरित आहे. क्रॅश शोधण्याचा प्रयत्न करणाऱ्या क्लासिक फझरच्या विपरीत, एकिडना वापरकर्त्याने परिभाषित केलेले इनव्हेरियंट्स (invariants) खंडित करण्याचा प्रयत्न करेल.

स्मार्ट कॉन्ट्रॅक्ट्समध्ये, इनव्हेरियंट्स हे Solidity फंक्शन्स असतात, जे कॉन्ट्रॅक्ट पोहोचू शकणाऱ्या कोणत्याही चुकीच्या किंवा अवैध स्थितीचे प्रतिनिधित्व करू शकतात, ज्यामध्ये खालील गोष्टींचा समावेश आहे:

  • चुकीचे अ‍ॅक्सेस नियंत्रण: हल्लेखोर कॉन्ट्रॅक्टचा मालक बनला.
  • चुकीची स्थिती मशीन: कॉन्ट्रॅक्ट थांबवलेले असताना टोकन ट्रान्सफर केले जाऊ शकतात.
  • चुकीचे अंकगणित: वापरकर्ता त्याच्या बॅलन्सला अंडरफ्लो करू शकतो आणि अमर्यादित मोफत टोकन मिळवू शकतो.

एकिडनासह प्रॉपर्टीची चाचणी करणे

एकिडनासह स्मार्ट कॉन्ट्रॅक्टची चाचणी कशी करायची ते आपण पाहू. खालील स्मार्ट कॉन्ट्रॅक्ट हे लक्ष्य आहे token.sol (नवीन टॅबमध्ये उघडते):

आम्ही असे गृहीत धरू की या टोकनमध्ये खालील प्रॉपर्टीज असणे आवश्यक आहे:

  • कोणाकडेही जास्तीत जास्त 1000 टोकन असू शकतात
  • टोकन ट्रान्सफर केले जाऊ शकत नाही (हे ERC-20 टोकन नाही)

प्रॉपर्टी लिहा

एकिडना प्रॉपर्टीज हे Solidity फंक्शन्स आहेत. प्रॉपर्टीमध्ये हे असणे आवश्यक आहे:

  • कोणतेही आर्ग्युमेंट नसावे
  • जर ते यशस्वी झाले तर true रिटर्न करावे
  • त्याचे नाव echidna ने सुरू व्हावे

एकिडना हे करेल:

  • प्रॉपर्टीची चाचणी करण्यासाठी स्वयंचलितपणे अनियंत्रित व्यवहार तयार करेल.
  • प्रॉपर्टीला false रिटर्न करण्यास किंवा एरर थ्रो करण्यास कारणीभूत ठरणाऱ्या कोणत्याही व्यवहारांची तक्रार करेल.
  • प्रॉपर्टी कॉल करताना साइड-इफेक्ट काढून टाकेल (म्हणजेच, जर प्रॉपर्टीने स्थिती व्हेरिएबल बदलले, तर ते चाचणीनंतर काढून टाकले जाते)

खालील प्रॉपर्टी तपासते की कॉलरकडे 1000 पेक्षा जास्त टोकन नाहीत:

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

तुमचे कॉन्ट्रॅक्ट तुमच्या प्रॉपर्टीजपासून वेगळे करण्यासाठी इनहेरिटन्स वापरा:

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

token.sol (नवीन टॅबमध्ये उघडते) प्रॉपर्टी लागू करते आणि टोकनमधून इनहेरिट करते.

कॉन्ट्रॅक्ट सुरू करा

एकिडनाला आर्ग्युमेंट नसलेला कन्स्ट्रक्टर आवश्यक आहे. जर तुमच्या कॉन्ट्रॅक्टला विशिष्ट इनिशिएलायझेशनची आवश्यकता असेल, तर तुम्हाला ते कन्स्ट्रक्टरमध्ये करावे लागेल.

एकिडनामध्ये काही विशिष्ट पत्ते आहेत:

  • 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 कॉल केले तर प्रॉपर्टीचे उल्लंघन होते.

फझिंग मोहिमेदरम्यान कॉल करण्यासाठी फंक्शन्स फिल्टर करणे

फझ करायच्या फंक्शन्सना कसे फिल्टर करायचे ते आपण पाहू. खालील स्मार्ट कॉन्ट्रॅक्ट हे लक्ष्य आहे:

हे छोटे उदाहरण एकिडनाला स्थिती व्हेरिएबल बदलण्यासाठी व्यवहारांचा एक विशिष्ट क्रम शोधण्यास भाग पाडते. हे फझरसाठी कठीण आहे (मॅन्टिकोर (नवीन टॅबमध्ये उघडते) सारखे सिम्बॉलिक एक्झिक्यूशन टूल वापरण्याची शिफारस केली जाते). याची पडताळणी करण्यासाठी आपण एकिडना चालवू शकतो:

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) चाचणी कशी करावी

या छोट्या ट्युटोरियलमध्ये, आम्ही कॉन्ट्रॅक्ट्समधील दृढकथन तपासणीची चाचणी करण्यासाठी एकिडना कसे वापरावे हे दाखवणार आहोत. समजा आपल्याकडे यासारखे एक कॉन्ट्रॅक्ट आहे:

दृढकथन लिहा

आपल्याला हे सुनिश्चित करायचे आहे की tmp त्याचा फरक रिटर्न केल्यानंतर counter पेक्षा कमी किंवा समान आहे. आपण एकिडना प्रॉपर्टी लिहू शकतो, परंतु आपल्याला tmp मूल्य कुठेतरी स्टोअर करावे लागेल. त्याऐवजी, आपण यासारखे दृढकथन वापरू शकतो:

एकिडना चालवा

दृढकथन अपयश चाचणी सक्षम करण्यासाठी, एक एकिडना कॉन्फिगरेशन फाइल (नवीन टॅबमध्ये उघडते) 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 पूर्ववत (revert) झाले, तर प्रॉपर्टी अयशस्वी होईल.

सर्वसाधारणपणे, दृढकथने कशी वापरावीत यावर आम्ही जॉन रेगेहर यांच्या शिफारसीचे (नवीन टॅबमध्ये उघडते) पालन करण्याची शिफारस करतो:

  • दृढकथन तपासणीदरम्यान कोणत्याही साइड इफेक्टची सक्ती करू नका. उदाहरणार्थ: assert(ChangeStateAndReturn() == 1)
  • स्पष्ट विधानांचे दृढकथन करू नका. उदाहरणार्थ assert(var >= 0) जिथे var ला uint म्हणून घोषित केले आहे.

शेवटी, कृपया assert ऐवजी require वापरू नका, कारण एकिडना ते शोधू शकणार नाही (परंतु कॉन्ट्रॅक्ट तरीही पूर्ववत होईल).

सारांश: दृढकथन तपासणी

खालीलप्रमाणे आपल्या उदाहरणावरील एकिडनाच्या रनचा सारांश आहे:

एकिडनाला आढळले की जर हे फंक्शन मोठ्या आर्ग्युमेंट्ससह अनेक वेळा कॉल केले तर inc मधील दृढकथन अयशस्वी होऊ शकते.

एकिडना कॉर्पस गोळा करणे आणि सुधारित करणे

एकिडनासह व्यवहारांचा कॉर्पस कसा गोळा करायचा आणि वापरायचा ते आपण पाहू. खालील स्मार्ट कॉन्ट्रॅक्ट हे लक्ष्य आहे magic.sol (नवीन टॅबमध्ये उघडते):

हे छोटे उदाहरण एकिडनाला स्थिती व्हेरिएबल बदलण्यासाठी विशिष्ट मूल्ये शोधण्यास भाग पाडते. हे फझरसाठी कठीण आहे (मॅन्टिकोर (नवीन टॅबमध्ये उघडते) सारखे सिम्बॉलिक एक्झिक्यूशन टूल वापरण्याची शिफारस केली जाते). याची पडताळणी करण्यासाठी आपण एकिडना चालवू शकतो:

echidna-test magic.sol
...

echidna_magic_values: passed! 🎉

Seed: 2221503356319272685

तथापि, ही फझिंग मोहीम चालवताना आपण कॉर्पस गोळा करण्यासाठी तरीही एकिडना वापरू शकतो.

कॉर्पस गोळा करणे

कॉर्पस संकलन सक्षम करण्यासाठी, एक कॉर्पस डिरेक्टरी तयार करा:

mkdir corpus-magic

आणि एक एकिडना कॉन्फिगरेशन फाइल (नवीन टॅबमध्ये उघडते) config.yaml:

coverage: true
corpusDir: "corpus-magic"

आता आपण आपले टूल चालवू शकतो आणि गोळा केलेला कॉर्पस तपासू शकतो:

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

एकिडनाला अद्याप योग्य मॅजिक मूल्ये सापडत नाहीत, परंतु आपण त्याने गोळा केलेल्या कॉर्पसवर एक नजर टाकू शकतो. उदाहरणार्थ, यापैकी एक फाइल होती:

स्पष्टपणे, हे इनपुट आपल्या प्रॉपर्टीमध्ये अपयश ट्रिगर करणार नाही. तथापि, पुढील चरणात, आपण त्यासाठी ते कसे सुधारायचे ते पाहू.

कॉर्पस सीड करणे

एकिडनाला 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: उत्तीर्ण! 🎉

सीड: 2320549945714142710

गॅस वापराचे मोजमाप करणे

एकिडनासह गॅस वापर सक्षम करण्यासाठी, एक कॉन्फिगरेशन फाइल config.yaml तयार करा:

estimateGas: true

या उदाहरणात, परिणाम समजण्यास सोपे करण्यासाठी आपण व्यवहारांच्या क्रमाचा आकार देखील कमी करू:

seqLen: 2
estimateGas: true

एकिडना चालवा

एकदा आपण कॉन्फिगरेशन फाइल तयार केली की, आपण एकिडना याप्रमाणे चालवू शकतो:

गॅस कमी करणारे कॉल्स फिल्टर करणे

वरील फझिंग मोहिमेदरम्यान कॉल करण्यासाठी फंक्शन्स फिल्टर करणे यावरील ट्युटोरियल तुमच्या चाचणीमधून काही फंक्शन्स कसे काढायचे हे दाखवते.
अचूक गॅस अंदाज मिळवण्यासाठी हे महत्त्वपूर्ण असू शकते. खालील उदाहरणाचा विचार करा:

जर एकिडना सर्व फंक्शन्सना कॉल करू शकत असेल, तर त्याला जास्त गॅस खर्च असलेले व्यवहार सहज सापडणार नाहीत:

याचे कारण असे की खर्च addrs च्या आकारावर अवलंबून असतो आणि यादृच्छिक कॉल्स अ‍ॅरे जवळजवळ रिकामा ठेवतात. तथापि, pop आणि clear ला ब्लॅकलिस्ट केल्याने आपल्याला बरेच चांगले परिणाम मिळतात:

filterBlacklist: true
filterFunctions: ["pop", "clear"]
echidna-test pushpop.sol --config config.yaml
...
push ने जास्तीत जास्त 40839 गॅस वापरला
...
check ने जास्तीत जास्त 1484472 गॅस वापरला

सारांश: जास्त गॅस वापरणारे व्यवहार शोधणे

एकिडना estimateGas कॉन्फिगरेशन पर्याय वापरून जास्त गॅस वापरणारे व्यवहार शोधू शकते:

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

एकदा फझिंग मोहीम संपली की, एकिडना प्रत्येक फंक्शनसाठी जास्तीत जास्त गॅस वापर असलेल्या क्रमाची तक्रार करेल.