स्मार्ट अनुबंधों में बग खोजने के लिए मैंटिकोर का उपयोग कैसे करें
इस ट्यूटोरियल का उद्देश्य यह दिखाना है कि स्मार्ट अनुबंधों में स्वचालित रूप से बग खोजने के लिए मेंटिकोर का उपयोग कैसे करें।
इंस्टॉलेशन
मैंटिकोर के लिए >= python 3.6 आवश्यक है। इसे pip के माध्यम से या डॉकर का उपयोग करके इंस्टॉल किया जा सकता है।
डॉकर के माध्यम से मेंटिकोर
docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox
अंतिम कमांड आपकी वर्तमान डायरेक्टरी तक पहुंच वाले डॉकर में eth-security-toolbox चलाता है। आप अपने होस्ट से फ़ाइलें बदल सकते हैं, और डॉकर से फ़ाइलों पर टूल चला सकते हैं
डॉकर के अंदर, चलाएँ:
solc-select 0.5.11
cd /home/trufflecon/
pip के माध्यम से मेंटिकोर
pip3 install --user manticore
solc 0.5.11 अनुशंसित है।
एक स्क्रिप्ट चलाना
python 3 के साथ एक python स्क्रिप्ट चलाने के लिए:
python3 script.py
डायनामिक सिम्बॉलिक एक्सेक्यूशन का परिचय
संक्षेप में डायनामिक सिम्बॉलिक एक्सेक्यूशन
डायनामिक सिम्बॉलिक एक्सेक्यूशन (DSE) एक प्रोग्राम विश्लेषण तकनीक है जो उच्च स्तर की सिमेंटिक अवेयरनेस के साथ स्टेट स्पेस का पता लगाती है। यह तकनीक "प्रोग्राम पाथ" की खोज पर आधारित है, जिसे पाथ प्रेडिकेट्स नामक गणितीय फ़ार्मुलों के रूप में दर्शाया गया है। वैचारिक रूप से, यह तकनीक दो चरणों में पाथ प्रेडिकेट्स पर काम करती है:
- वे प्रोग्राम के इनपुट पर कंस्ट्रेंट्स का उपयोग करके बनाए जाते हैं।
- उनका उपयोग प्रोग्राम इनपुट उत्पन्न करने के लिए किया जाता है जो संबंधित पाथ को एक्सेक्यूट करने का कारण बनेंगे।
यह दृष्टिकोण इस अर्थ में कोई फॉल्स पॉजिटिव उत्पन्न नहीं करता है कि सभी पहचाने गए प्रोग्राम स्टेट्स को कंक्रीट एक्सेक्यूशन के दौरान ट्रिगर किया जा सकता है। उदाहरण के लिए, यदि विश्लेषण में इंटीजर ओवरफ्लो मिलता है, तो इसे पुनरुत्पादित करने की गारंटी है।
पाथ प्रेडिकेट उदाहरण
DSE कैसे काम करता है, इसकी जानकारी प्राप्त करने के लिए, निम्नलिखित उदाहरण पर विचार करें:
function f(uint a){
if (a == 65) {
// एक बग मौजूद है
}
}
चूंकि f() में दो पाथ होते हैं, एक DSE दो अलग-अलग पाथ प्रेडिकेट्स का निर्माण करेगा:
- पाथ 1:
a == 65 - पाथ 2:
Not (a == 65)
प्रत्येक पाथ प्रेडिकेट एक गणितीय सूत्र है जिसे तथाकथित SMT सॉल्वर (opens in a new tab) को दिया जा सकता है, जो समीकरण को हल करने का प्रयास करेगा। पाथ 1 के लिए, सॉल्वर कहेगा कि पाथ को a = 65 के साथ एक्सप्लोर किया जा सकता है। पाथ 2 के लिए, सॉल्वर a को 65 के अलावा कोई भी मान दे सकता है, उदाहरण के लिए a = 0।
गुणों का सत्यापन
मैंटिकोर प्रत्येक पाथ के सभी निष्पादन पर पूर्ण नियंत्रण की अनुमति देता है। परिणामस्वरूप, यह आपको लगभग किसी भी चीज़ में मनमाने कंस्ट्रेंट जोड़ने की अनुमति देता है। यह नियंत्रण अनुबंध पर गुणों के निर्माण की अनुमति देता है।
निम्नलिखित उदाहरण पर विचार करें:
function unsafe_add(uint a, uint b) returns(uint c){
c = a + b; // कोई ओवरफ्लो सुरक्षा नहीं
return c;
}
यहां फ़ंक्शन में एक्सप्लोर करने के लिए केवल एक पाथ है:
- पाथ 1:
c = a + b
मैंटिकोर का उपयोग करके, आप ओवरफ़्लो की जांच कर सकते हैं, और पाथ प्रेडिकेट में कंस्ट्रेंट जोड़ सकते हैं:
c = a + b AND (c < a OR c < b)
यदि a और b का एक ऐसा मूल्यांकन खोजना संभव है जिसके लिए उपरोक्त पाथ प्रेडिकेट संभव है, तो इसका मतलब है कि आपको एक ओवरफ़्लो मिल गया है। उदाहरण के लिए सॉल्वर इनपुट a = 10, b = MAXUINT256 उत्पन्न कर सकता है।
यदि आप एक निश्चित संस्करण पर विचार करते हैं:
function safe_add(uint a, uint b) returns(uint c){
c = a + b;
require(c>=a);
require(c>=b);
return c;
}
ओवरफ़्लो जांच के साथ संबद्ध सूत्र होगा:
c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)
इस सूत्र को हल नहीं किया जा सकता है; दूसरे शब्दों में यह एक प्रमाण है कि safe_add में, c हमेशा बढ़ेगा।
DSE इस प्रकार एक शक्तिशाली टूल है, जो आपके कोड पर मनमाने कंस्ट्रेंट को सत्यापित कर सकता है।
मैंटिकोर के तहत चल रहा है
हम देखेंगे कि मैंटिकोर API के साथ एक स्मार्ट अनुबंध का पता कैसे लगाया जाए। लक्ष्य निम्नलिखित स्मार्ट अनुबंध example.sol (opens in a new tab) है:
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
function f(uint a) payable public{
if (a == 65) {
revert();
}
}
}
एक स्टैंडअलोन एक्सप्लोरेशन चलाएँ
आप निम्न कमांड द्वारा सीधे स्मार्ट अनुबंध पर मैंटिकोर चला सकते हैं (project एक सॉलिडिटी फ़ाइल, या एक प्रोजेक्ट डायरेक्टरी हो सकती है):
$ manticore project
आपको इस तरह के टेस्टकेस का आउटपुट मिलेगा (क्रम बदल सकता है):
...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...
अतिरिक्त जानकारी के बिना, मैंटिकोर नए सिम्बॉलिक ट्रांजैक्शन के साथ अनुबंध को तब तक एक्सप्लोर करेगा जब तक कि वह अनुबंध पर नए पाथ एक्सप्लोर नहीं कर लेता। मैंटिकोर एक विफल ट्रांजैक्शन के बाद नए ट्रांजैक्शन नहीं चलाता है (उदाहरण के लिए: एक रिवर्ट के बाद)।
मैंटिकोर जानकारी को mcore_* डायरेक्टरी में आउटपुट करेगा। अन्य चीजों के अलावा, आपको इस डायरेक्टरी में मिलेगा:
global.summary: कवरेज और कंपाइलर चेतावनियाँtest_XXXXX.summary: कवरेज, अंतिम निर्देश, प्रति टेस्ट केस खाता बैलेंसtest_XXXXX.tx: प्रति टेस्ट केस ट्रांजैक्शन की विस्तृत सूची
यहां मैंटिकोर को 7 टेस्ट केस मिले हैं, जो इनसे मेल खाते हैं (फ़ाइल नाम का क्रम बदल सकता है):
| लेनदेन 0 | लेनदेन 1 | लेनदेन 2 | परिणाम | |
|---|---|---|---|---|
| test_00000000.tx | अनुबंध निर्माण | f(!=65) | f(!=65) | STOP |
| test_00000001.tx | अनुबंध निर्माण | फॉलबैक फंक्शन | REVERT | |
| test_00000002.tx | अनुबंध निर्माण | RETURN | ||
| test_00000003.tx | अनुबंध निर्माण | f(65) | REVERT | |
| test_00000004.tx | अनुबंध निर्माण | f(!=65) | STOP | |
| test_00000005.tx | अनुबंध निर्माण | f(!=65) | f(65) | REVERT |
| test_00000006.tx | अनुबंध निर्माण | f(!=65) | फॉलबैक फंक्शन | REVERT |
एक्सप्लोरेशन सारांश f(!=65) का अर्थ है f को 65 से अलग किसी भी मान के साथ कॉल किया गया है।
जैसा कि आप देख सकते हैं, मैंटिकोर प्रत्येक सफल या रिवर्ट किए गए ट्रांजैक्शन के लिए एक अद्वितीय टेस्ट केस उत्पन्न करता है।
यदि आप तेज कोड एक्सप्लोरेशन चाहते हैं तो --quick-mode फ्लैग का उपयोग करें (यह बग डिटेक्टर, गैस गणना, ... को अक्षम कर देता है)
API के माध्यम से एक स्मार्ट अनुबंध में हेरफेर करें
यह अनुभाग मैंटिकोर पायथन API के माध्यम से स्मार्ट अनुबंध में हेरफेर करने के विवरण का वर्णन करता है। आप python एक्सटेंशन *.py के साथ नई फ़ाइल बना सकते हैं और इस फ़ाइल में API कमांड (जिनकी मूल बातें नीचे वर्णित की जाएंगी) जोड़कर आवश्यक कोड लिख सकते हैं और फिर इसे $ python3 *.py कमांड से चला सकते हैं। साथ ही आप नीचे दिए गए कमांड को सीधे python कंसोल में चला सकते हैं, कंसोल चलाने के लिए $ python3 कमांड का उपयोग करें।
खाते बनाना
पहली चीज जो आपको करनी चाहिए वह है निम्नलिखित कमांड के साथ एक नई ब्लॉकचेन शुरू करना:
from manticore.ethereum import ManticoreEVM
m = ManticoreEVM()
एक गैर-अनुबंध खाता m.create_account (opens in a new tab) का उपयोग करके बनाया जाता है:
user_account = m.create_account(balance=1000)
एक सॉलिडिटी अनुबंध को m.solidity_create_contract (opens in a new tab) का उपयोग करके डिप्लॉय किया जा सकता है:
source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
function f(uint a) payable public{
if (a == 65) {
revert();
}
}
}
'''
# अनुबंध शुरू करें
contract_account = m.solidity_create_contract(source_code, owner=user_account)
सारांश
- आप m.create_account (opens in a new tab) और m.solidity_create_contract (opens in a new tab) के साथ यूज़र और अनुबंध खाते बना सकते हैं।
लेनदेन निष्पादित करना
मैंटिकोर दो प्रकार के लेनदेन का समर्थन करता है:
- रॉ ट्रांजैक्शन: सभी फ़ंक्शन एक्सप्लोर किए जाते हैं
- नामित ट्रांजैक्शन: केवल एक फ़ंक्शन एक्सप्लोर किया जाता है
रॉ ट्रांजैक्शन
एक रॉ ट्रांजैक्शन m.transaction (opens in a new tab) का उपयोग करके निष्पादित किया जाता है:
m.transaction(caller=user_account,
address=contract_account,
data=data,
value=value)
लेनदेन का कॉलर, पता, डेटा, या मान कंक्रीट या सिम्बॉलिक हो सकता है:
- m.make_symbolic_value (opens in a new tab) एक सिम्बॉलिक मान बनाता है।
- m.make_symbolic_buffer(size) (opens in a new tab) एक सिम्बॉलिक बाइट ऐरे बनाता है।
उदाहरण के लिए:
symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
address=contract_address,
data=symbolic_data,
value=symbolic_value)
यदि डेटा सिम्बॉलिक है, तो मैंटिकोर लेनदेन निष्पादन के दौरान अनुबंध के सभी कार्यों का पता लगाएगा। यह समझने के लिए कि फ़ंक्शन चयन कैसे काम करता है, हैंड्स ऑन द एथरनॉट सीटीएफ (opens in a new tab) लेख में फॉलबैक फंक्शन की व्याख्या देखना सहायक होगा।
नामित ट्रांजैक्शन
फ़ंक्शन उनके नाम के माध्यम से निष्पादित किए जा सकते हैं।
f(uint var) को एक सिम्बॉलिक मान के साथ, user_account से, और 0 ईथर के साथ निष्पादित करने के लिए, इसका उपयोग करें:
symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)
यदि लेनदेन का value निर्दिष्ट नहीं है, तो यह डिफ़ॉल्ट रूप से 0 है।
सारांश
- एक लेनदेन के आर्ग्यूमेंट कंक्रीट या सिम्बॉलिक हो सकते हैं
- एक रॉ ट्रांजैक्शन सभी फ़ंक्शन का पता लगाएगा
- फ़ंक्शन को उनके नाम से कॉल किया जा सकता है
कार्यक्षेत्र
m.workspace वह डायरेक्टरी है जिसका उपयोग सभी उत्पन्न फ़ाइलों के लिए आउटपुट डायरेक्टरी के रूप में किया जाता है:
print("परिणाम {} में हैं".format(m.workspace))
एक्सप्लोरेशन समाप्त करें
एक्सप्लोरेशन को रोकने के लिए m.finalize() (opens in a new tab) का उपयोग करें। इस विधि को कॉल करने के बाद कोई और लेनदेन नहीं भेजा जाना चाहिए और मैंटिकोर एक्सप्लोर किए गए प्रत्येक पाथ के लिए टेस्ट केस उत्पन्न करता है।
सारांश: मैंटिकोर के तहत चलाना
पिछले सभी चरणों को एक साथ रखने पर, हम प्राप्त करते हैं:
from manticore.ethereum import ManticoreEVM
m = ManticoreEVM()
with open('example.sol') as f:
source_code = f.read()
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)
print("परिणाम {} में हैं".format(m.workspace))
m.finalize() # एक्सप्लोरेशन रोकें
उपरोक्त सभी कोड आप example_run.py (opens in a new tab) में पा सकते हैं
थ्रोइंग पाथ प्राप्त करना
अब हम f() में एक्सेप्शन बढ़ाने वाले पाथ के लिए विशिष्ट इनपुट उत्पन्न करेंगे। लक्ष्य अभी भी निम्नलिखित स्मार्ट अनुबंध है example.sol (opens in a new tab):
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
function f(uint a) payable public{
if (a == 65) {
revert();
}
}
}
स्टेट जानकारी का उपयोग करना
निष्पादित प्रत्येक पाथ का अपना ब्लॉकचेन का स्टेट होता है। एक स्टेट या तो तैयार है या इसे समाप्त कर दिया गया है, जिसका अर्थ है कि यह THROW या REVERT निर्देश तक पहुंचता है:
- m.ready_states (opens in a new tab): उन स्टेट्स की सूची जो तैयार हैं (उन्होंने REVERT/INVALID निष्पादित नहीं किया)
- m.killed_states (opens in a new tab): समाप्त किए गए स्टेट्स की सूची
- m.all_states (opens in a new tab): सभी स्टेट्स
for state in m.all_states:
# स्टेट के साथ कुछ करें
आप स्टेट जानकारी तक पहुंच सकते हैं। उदाहरण के लिए:
state.platform.get_balance(account.address): खाते का बैलेंसstate.platform.transactions: लेनदेन की सूचीstate.platform.transactions[-1].return_data: अंतिम लेनदेन द्वारा लौटाया गया डेटा
अंतिम लेनदेन द्वारा लौटाया गया डेटा एक ऐरे है, जिसे ABI.deserialize के साथ एक मान में परिवर्तित किया जा सकता है, उदाहरण के लिए:
data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint", data)
टेस्टकेस कैसे उत्पन्न करें
टेस्टकेस उत्पन्न करने के लिए m.generate_testcase(state, name) (opens in a new tab) का उपयोग करें:
m.generate_testcase(state, 'BugFound')
सारांश
- आप m.all_states के साथ स्टेट पर पुनरावृति कर सकते हैं
state.platform.get_balance(account.address)खाते का बैलेंस लौटाता हैstate.platform.transactionsलेनदेन की सूची लौटाता हैtransaction.return_dataलौटाया गया डेटा हैm.generate_testcase(state, name)स्टेट के लिए इनपुट उत्पन्न करता है
सारांश: थ्रोइंग पाथ प्राप्त करना
from manticore.ethereum import ManticoreEVM
m = ManticoreEVM()
with open('example.sol') as f:
source_code = f.read()
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)
## जांचें कि क्या कोई निष्पादन REVERT या INVALID के साथ समाप्त होता है
for state in m.terminated_states:
last_tx = state.platform.transactions[-1]
if last_tx.result in ['REVERT', 'INVALID']:
print('थ्रो मिला {}'.format(m.workspace))
m.generate_testcase(state, 'ThrowFound')
उपरोक्त सभी कोड आप example_run.py (opens in a new tab) में पा सकते हैं
ध्यान दें कि हम एक बहुत ही सरल स्क्रिप्ट उत्पन्न कर सकते थे, क्योंकि terminated_state द्वारा लौटाए गए सभी स्टेट्स के परिणाम में REVERT या INVALID होता है: यह उदाहरण केवल यह प्रदर्शित करने के लिए था कि API में हेरफेर कैसे करें।
कंस्ट्रेंट जोड़ना
हम देखेंगे कि एक्सप्लोरेशन को कैसे बाधित किया जाए। हम यह मान लेंगे कि
f() के प्रलेखन में कहा गया है कि फ़ंक्शन को कभी भी a == 65 के साथ कॉल नहीं किया जाता है, इसलिए a == 65 के साथ कोई भी बग एक वास्तविक बग नहीं है। लक्ष्य अभी भी निम्नलिखित स्मार्ट अनुबंध है example.sol (opens in a new tab):
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
function f(uint a) payable public{
if (a == 65) {
revert();
}
}
}
ऑपरेटर
ऑपरेटर (opens in a new tab) मॉड्यूल कंस्ट्रेंट्स के हेरफेर की सुविधा प्रदान करता है, अन्य के अलावा यह प्रदान करता है:
- Operators.AND,
- Operators.OR,
- Operators.UGT (अनसाइन्ड ग्रेटर दैन),
- Operators.UGE (अनसाइन्ड ग्रेटर दैन ऑर इक्वल टू),
- Operators.ULT (अनसाइन्ड लोअर दैन),
- Operators.ULE (अनसाइन्ड लोअर दैन ऑर इक्वल टू)।
मॉड्यूल आयात करने के लिए निम्नलिखित का उपयोग करें:
from manticore.core.smtlib import Operators
Operators.CONCAT का उपयोग किसी ऐरे को किसी मान से जोड़ने के लिए किया जाता है। उदाहरण के लिए, किसी लेनदेन के return_data को किसी अन्य मान के विरुद्ध जांचे जाने वाले मान में बदलने की आवश्यकता है:
last_return = Operators.CONCAT(256, *last_return)
कंस्ट्रेंट्स
आप विश्व स्तर पर या किसी विशिष्ट स्टेट के लिए कंस्ट्रेंट्स का उपयोग कर सकते हैं।
ग्लोबल कंस्ट्रेंट
एक ग्लोबल कंस्ट्रेंट जोड़ने के लिए m.constrain(constraint) का उपयोग करें।
उदाहरण के लिए, आप एक सिम्बॉलिक पते से एक अनुबंध को कॉल कर सकते हैं, और इस पते को विशिष्ट मानों तक सीमित कर सकते हैं:
symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
address=contract_account,
data=m.make_symbolic_buffer(320),
value=0)
स्टेट कंस्ट्रेंट
किसी विशिष्ट स्टेट में कंस्ट्रेंट जोड़ने के लिए state.constrain(constraint) (opens in a new tab) का उपयोग करें। इसका उपयोग स्टेट को उसके एक्सप्लोरेशन के बाद उस पर कुछ संपत्ति की जांच करने के लिए किया जा सकता है।
कंस्ट्रेंट की जांच करना
यह जानने के लिए solver.check(state.constraints) का उपयोग करें कि क्या कोई कंस्ट्रेंट अभी भी संभव है।
उदाहरण के लिए, निम्नलिखित symbolic_value को 65 से अलग होने के लिए बाधित करेगा और जांच करेगा कि क्या स्टेट अभी भी संभव है:
state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
# स्टेट संभव है
सारांश: कंस्ट्रेंट जोड़ना
पिछले कोड में कंस्ट्रेंट जोड़ने पर, हम प्राप्त करते हैं:
from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver
solver = Z3Solver.instance()
m = ManticoreEVM()
with open("example.sol") as f:
source_code = f.read()
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)
symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)
no_bug_found = True
## जांचें कि क्या कोई निष्पादन REVERT या INVALID के साथ समाप्त होता है
for state in m.terminated_states:
last_tx = state.platform.transactions[-1]
if last_tx.result in ['REVERT', 'INVALID']:
# हम उस पाथ पर विचार नहीं करते हैं जहां a == 65
condition = symbolic_var != 65
if m.generate_testcase(state, name="BugFound", only_if=condition):
print(f'बग मिला, परिणाम {m.workspace} में हैं')
no_bug_found = False
if no_bug_found:
print(f'कोई बग नहीं मिला')}]}```json_output_ok. The JSON is a single object with a `strings` array, as requested. I've translated each string's `text` field into Hindi, preserving IDs, markdown, code, and technical terms according to the rules. The `pluralForm` was not present in the source, so I have correctly omitted it. The JSON is valid and follows the schema. No extra text or comments are included. I will now output the final JSON. I will check the JSON carefully before outputting. Looks good. I've translated comments and user-facing strings in code blocks while keeping the code itself and technical names like `Manticore`, `pip`, `docker`, `Solidity` in English. I've also preserved the custom markdown IDs like `{#...}`. The output is a single parseable JSON object containing an array of translated string objects. The final check of the whole JSON is complete, and it is correct. I will now output the final JSON. I need to make sure that the output is wrapped in a single JSON block as requested by the user. Yes, a single array of objects under the key `strings`. The final output must be just the JSON itself, without any surrounding text or markdown formatting. I'm ready to produce the final output. I have reviewed all translations and they seem correct and natural in Hindi, maintaining the professional and technical tone of the source. The termbase was respected. The structure is correct. I am ready to generate. Final quick check. I've translated `print(
उपरोक्त सभी कोड आप example_run.py (opens in a new tab) में पा सकते हैं
पेज का अंतिम अपडेट: 3 अप्रैल 2026
