سمارٹ کنٹریکٹس میں بگز تلاش کرنے کے لیے مینٹیکور کا استعمال کیسے کریں

اس ٹیوٹوریل کا مقصد یہ دکھانا ہے کہ سمارٹ کنٹریکٹس میں خودکار طور پر بگز تلاش کرنے کے لیے مینٹیکور کا استعمال کیسے کیا جائے۔

انسٹالیشن

مینٹیکور کے لیے = python 3.6 درکار ہے۔ اسے pip کے ذریعے یا Docker کا استعمال کرتے ہوئے انسٹال کیا جا سکتا ہے۔

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/trufflecon/

pip کے ذریعے مینٹیکور

pip3 install --user manticore

solc 0.5.11 تجویز کیا جاتا ہے۔

سکرپٹ چلانا

Python 3 کے ساتھ Python سکرپٹ چلانے کے لیے:

python3 script.py

ڈائنامک سمبولک ایگزیکیوشن کا تعارف

ڈائنامک سمبولک ایگزیکیوشن کا مختصر جائزہ

ڈائنامک سمبولک ایگزیکیوشن (DSE) ایک پروگرام تجزیہ کی تکنیک ہے جو اعلی درجے کی معنوی آگاہی کے ساتھ حالت کی جگہ (state space) کو دریافت کرتی ہے۔ یہ تکنیک "پروگرام پاتھس" کی دریافت پر مبنی ہے، جنہیں ریاضیاتی فارمولوں کے طور پر پیش کیا جاتا ہے جنہیں path predicates کہا جاتا ہے۔ تصوراتی طور پر، یہ تکنیک پاتھ پریڈیکیٹس پر دو مراحل میں کام کرتی ہے:

1. انہیں پروگرام کے ان پٹ پر پابندیوں (constraints) کا استعمال کرتے ہوئے بنایا جاتا ہے۔
2. انہیں پروگرام کے ان پٹس بنانے کے لیے استعمال کیا جاتا ہے جو متعلقہ پاتھس کو چلانے کا سبب بنیں گے۔

یہ نقطہ نظر اس لحاظ سے کوئی غلط مثبت (false positives) پیدا نہیں کرتا کہ تمام شناخت شدہ پروگرام کی حالتوں کو ٹھوس ایگزیکیوشن کے دوران متحرک کیا جا سکتا ہے۔ مثال کے طور پر، اگر تجزیہ میں کوئی انٹیجر اوور فلو ملتا ہے، تو اس کے دوبارہ پیدا ہونے کی ضمانت دی جاتی ہے۔

پاتھ پریڈیکیٹ کی مثال

DSE کیسے کام کرتا ہے اس کی بصیرت حاصل کرنے کے لیے، درج ذیل مثال پر غور کریں:

function f(uint a){

  if (a == 65) {
      // ایک بگ موجود ہے
  }

}

چونکہ f() میں دو پاتھس شامل ہیں، ایک DSE دو مختلف پاتھ پریڈیکیٹس بنائے گا:

• پاتھ 1: a == 65
• پاتھ 2: Not (a == 65)

ہر پاتھ پریڈیکیٹ ایک ریاضیاتی فارمولہ ہے جو ایک نام نہاد SMT حل کنندہ (opens in a new tab) کو دیا جا سکتا ہے، جو مساوات کو حل کرنے کی کوشش کرے گا۔ Path 1 کے لیے، حل کنندہ کہے گا کہ پاتھ کو a = 65 کے ساتھ دریافت کیا جا سکتا ہے۔ Path 2 کے لیے، حل کنندہ a کو 65 کے علاوہ کوئی بھی قدر دے سکتا ہے، مثال کے طور پر a = 0۔

خصوصیات کی تصدیق

مینٹیکور ہر پاتھ کی تمام ایگزیکیوشن پر مکمل کنٹرول کی اجازت دیتا ہے۔ نتیجے کے طور پر، یہ آپ کو تقریباً کسی بھی چیز میں صوابدیدی پابندیاں (arbitrary constraints) شامل کرنے کی اجازت دیتا ہے۔ یہ کنٹرول کنٹریکٹ پر خصوصیات بنانے کی اجازت دیتا ہے۔

درج ذیل مثال پر غور کریں:

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 ایک Solidity فائل، یا پروجیکٹ ڈائریکٹری ہو سکتی ہے):

$ 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 ٹیسٹ کیسز ملتے ہیں، جو اس سے مطابقت رکھتے ہیں (فائل کے نام کی ترتیب تبدیل ہو سکتی ہے):

دریافت کا خلاصہ f(!=65) ظاہر کرتا ہے کہ f کو 65 کے علاوہ کسی بھی قدر کے ساتھ کال کیا گیا ہے۔

جیسا کہ آپ دیکھ سکتے ہیں، مینٹیکور ہر کامیاب یا ریورٹ ہونے والی ٹرانزیکشن کے لیے ایک منفرد ٹیسٹ کیس بناتا ہے۔

اگر آپ تیز کوڈ کی دریافت چاہتے ہیں تو --quick-mode فلیگ استعمال کریں (یہ بگ ڈیٹیکٹرز، گیس کے حساب کتاب وغیرہ کو غیر فعال کر دیتا ہے)

API کے ذریعے سمارٹ کنٹریکٹ کو مینیپولیٹ کریں

یہ سیکشن تفصیلات بیان کرتا ہے کہ مینٹیکور Python 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)

ایک Solidity کنٹریکٹ کو 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();
        }
    }
}
'''
# Initiate the contract
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) کے ساتھ صارف اور کنٹریکٹ اکاؤنٹس بنا سکتے ہیں۔

ٹرانزیکشنز کو انجام دینا

مینٹیکور دو قسم کی ٹرانزیکشنز کو سپورٹ کرتا ہے:

• خام (Raw) ٹرانزیکشن: تمام فنکشنز دریافت کیے جاتے ہیں
• نامزد (Named) ٹرانزیکشن: صرف ایک فنکشن دریافت کیا جاتا ہے

خام ٹرانزیکشن

ایک خام ٹرانزیکشن m.transaction (opens in a new tab) کا استعمال کرتے ہوئے انجام دی جاتی ہے:

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

کالر، پتہ، ڈیٹا، یا ٹرانزیکشن کی قدر یا تو ٹھوس (concrete) یا علامتی (symbolic) ہو سکتی ہے:

• 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)

اگر ڈیٹا علامتی ہے، تو مینٹیکور ٹرانزیکشن کی ایگزیکیوشن کے دوران کنٹریکٹ کے تمام فنکشنز کو دریافت کرے گا۔ فنکشن کا انتخاب کیسے کام کرتا ہے یہ سمجھنے کے لیے Hands on the Ethernaut CTF (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 ہوتی ہے۔

خلاصہ

• ٹرانزیکشن کے دلائل (arguments) ٹھوس یا علامتی ہو سکتے ہیں
• ایک خام ٹرانزیکشن تمام فنکشنز کو دریافت کرے گی
• فنکشن کو ان کے نام سے کال کیا جا سکتا ہے

ورک اسپیس

m.workspace وہ ڈائریکٹری ہے جو تیار کردہ تمام فائلوں کے لیے آؤٹ پٹ ڈائریکٹری کے طور پر استعمال ہوتی ہے:

print("Results are in {}".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("Results are in {}".format(m.workspace))
m.finalize() # کھوج کو روکیں

اوپر دیا گیا تمام کوڈ آپ کو example_run.py (opens in a new tab) میں مل سکتا ہے

تھروئنگ پاتھس (Throwing paths) حاصل کرنا

اب ہم f() میں ایکسیپشن (exception) پیدا کرنے والے پاتھس کے لیے مخصوص ان پٹس بنائیں گے۔ ہدف اب بھی درج ذیل سمارٹ کنٹریکٹ 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();
        }
    }
}

حالت کی معلومات کا استعمال

ہر ایگزیکیوٹ ہونے والے پاتھ کی بلاک چین کی اپنی حالت ہوتی ہے۔ ایک حالت یا تو تیار (ready) ہوتی ہے یا اسے ختم (killed) کر دیا جاتا ہے، جس کا مطلب ہے کہ یہ 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 کے ساتھ حالت پر اعادہ (iterate) کر سکتے ہیں
• 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)

## چیک کریں کہ کیا عمل درآمد ریورٹ یا INVALID پر ختم ہوتا ہے
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.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();
        }
    }
}

آپریٹرز

Operators (opens in a new tab) ماڈیول پابندیوں کی مینیپولیشن میں سہولت فراہم کرتا ہے، دیگر چیزوں کے علاوہ یہ فراہم کرتا ہے:

• Operators.AND،
• Operators.OR،
• Operators.UGT (unsigned greater than)،
• Operators.UGE (unsigned greater than or equal to)،
• Operators.ULT (unsigned lower than)،
• Operators.ULE (unsigned lower than or equal to)۔

ماڈیول امپورٹ کرنے کے لیے درج ذیل کا استعمال کریں:

from manticore.core.smtlib import Operators

Operators.CONCAT کا استعمال ایک ایرے کو ایک قدر کے ساتھ جوڑنے (concatenate) کے لیے کیا جاتا ہے۔ مثال کے طور پر، کسی ٹرانزیکشن کے return_data کو کسی دوسری قدر کے خلاف جانچنے کے لیے ایک قدر میں تبدیل کرنے کی ضرورت ہوتی ہے:

last_return = Operators.CONCAT(256, *last_return)

پابندیاں

آپ پابندیوں کو عالمی سطح پر (globally) یا کسی مخصوص حالت کے لیے استعمال کر سکتے ہیں۔

عالمی پابندی

عالمی پابندی شامل کرنے کے لیے 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

## چیک کریں کہ کیا عمل درآمد ریورٹ یا 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'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

اوپر دیا گیا تمام کوڈ آپ کو example_run.py (opens in a new tab) میں مل سکتا ہے

صفحہ کی آخری اپ ڈیٹ: ۳ اپریل، ۲۰۲۶

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+6

تعاون کنندگان دیکھیں