স্মার্ট কন্ট্রাক্টে বাগ খুঁজতে কীভাবে ম্যান্টিকোর (Manticore) ব্যবহার করবেন

এই টিউটোরিয়ালের উদ্দেশ্য হলো স্মার্ট কন্ট্রাক্টে স্বয়ংক্রিয়ভাবে বাগ খুঁজতে কীভাবে ম্যান্টিকোর (Manticore) ব্যবহার করতে হয় তা দেখানো।

ইনস্টলেশন

ম্যান্টিকোরের জন্য >= python 3.6 প্রয়োজন। এটি pip বা docker ব্যবহার করে ইনস্টল করা যেতে পারে।

ডকারের মাধ্যমে ম্যান্টিকোর

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/

পিপের মাধ্যমে ম্যান্টিকোর

pip3 install --user manticore

solc 0.5.11 সুপারিশ করা হয়।

স্ক্রিপ্ট রান করা

python 3 দিয়ে একটি পাইথন স্ক্রিপ্ট রান করতে:

python3 script.py

ডাইনামিক সিম্বলিক এক্সিকিউশনের পরিচিতি

সংক্ষেপে ডাইনামিক সিম্বলিক এক্সিকিউশন

ডাইনামিক সিম্বলিক এক্সিকিউশন (DSE) হলো একটি প্রোগ্রাম অ্যানালাইসিস কৌশল যা উচ্চ মাত্রার শব্দার্থিক সচেতনতার (semantic awareness) সাথে একটি স্টেট স্পেস অন্বেষণ করে। এই কৌশলটি "প্রোগ্রাম পাথ" আবিষ্কারের উপর ভিত্তি করে তৈরি, যা গাণিতিক সূত্র হিসেবে উপস্থাপিত হয় এবং এদের path predicates বলা হয়। ধারণাগতভাবে, এই কৌশলটি দুটি ধাপে পাথ প্রেডিকেটে কাজ করে:

1. এগুলো প্রোগ্রামের ইনপুটের উপর কনস্ট্রেইন্ট ব্যবহার করে তৈরি করা হয়।
2. এগুলো প্রোগ্রামের ইনপুট তৈরি করতে ব্যবহৃত হয় যা সংশ্লিষ্ট পাথগুলোকে এক্সিকিউট করবে।

এই পদ্ধতিটি কোনো ফলস পজিটিভ তৈরি করে না, কারণ চিহ্নিত সমস্ত প্রোগ্রাম স্টেট কংক্রিট এক্সিকিউশনের সময় ট্রিগার করা যেতে পারে। উদাহরণস্বরূপ, যদি অ্যানালাইসিসে কোনো ইন্টিজার ওভারফ্লো পাওয়া যায়, তবে এটি পুনরুৎপাদনযোগ্য (reproducible) হওয়ার নিশ্চয়তা থাকে।

পাথ প্রেডিকেটের উদাহরণ

DSE কীভাবে কাজ করে তার একটি ধারণা পেতে, নিচের উদাহরণটি বিবেচনা করুন:

1function f(uint a){
2
3  if (a == 65) {
4      // একটি বাগ রয়েছে
5  }
6
7}
কপি করুন

যেহেতু f()-এ দুটি পাথ রয়েছে, একটি DSE দুটি ভিন্ন পাথ প্রেডিকেট তৈরি করবে:

• পাথ 1: a == 65
• পাথ 2: Not (a == 65)

প্রতিটি পাথ প্রেডিকেট হলো একটি গাণিতিক সূত্র যা একটি তথাকথিত SMT solver (opens in a new tab)-কে দেওয়া যেতে পারে, যা সমীকরণটি সমাধান করার চেষ্টা করবে। Path 1-এর জন্য, সলভার বলবে যে পাথটি a = 65 দিয়ে অন্বেষণ করা যেতে পারে। Path 2-এর জন্য, সলভার a-কে 65 ছাড়া অন্য যেকোনো মান দিতে পারে, উদাহরণস্বরূপ a = 0।

প্রপার্টি যাচাই করা

ম্যান্টিকোর প্রতিটি পাথের সমস্ত এক্সিকিউশনের উপর সম্পূর্ণ নিয়ন্ত্রণ প্রদান করে। ফলস্বরূপ, এটি আপনাকে প্রায় যেকোনো কিছুতে ইচ্ছামতো কনস্ট্রেইন্ট যোগ করার অনুমতি দেয়। এই নিয়ন্ত্রণ কন্ট্রাক্টে প্রপার্টি তৈরির সুযোগ দেয়।

নিচের উদাহরণটি বিবেচনা করুন:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // কোনো ওভারফ্লো সুরক্ষা নেই
3  return c;
4}
কপি করুন

এখানে ফাংশনটিতে অন্বেষণ করার জন্য কেবল একটি পাথ রয়েছে:

• পাথ 1: c = a + b

ম্যান্টিকোর ব্যবহার করে, আপনি ওভারফ্লো পরীক্ষা করতে পারেন এবং পাথ প্রেডিকেটে কনস্ট্রেইন্ট যোগ করতে পারেন:

• c = a + b AND (c < a OR c < b)

যদি a এবং b-এর এমন কোনো মান খুঁজে পাওয়া সম্ভব হয় যার জন্য উপরের পাথ প্রেডিকেটটি কার্যকর, তার মানে হলো আপনি একটি ওভারফ্লো খুঁজে পেয়েছেন। উদাহরণস্বরূপ সলভার a = 10 , b = MAXUINT256 ইনপুট তৈরি করতে পারে।

যদি আপনি একটি সংশোধিত সংস্করণ বিবেচনা করেন:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
কপি করুন

ওভারফ্লো চেক সহ সংশ্লিষ্ট সূত্রটি হবে:

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

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
সব দেখানকপি করুন

একটি স্ট্যান্ডঅ্যালোন এক্সপ্লোরেশন রান করা

আপনি নিচের কমান্ডের মাধ্যমে সরাসরি স্মার্ট কন্ট্রাক্টে ম্যান্টিকোর রান করতে পারেন (project একটি সলিডিটি ফাইল বা একটি প্রজেক্ট ডিরেক্টরি হতে পারে):

$ manticore project

আপনি এর মতো টেস্টকেসগুলোর আউটপুট পাবেন (ক্রম পরিবর্তন হতে পারে):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
সব দেখান

অতিরিক্ত তথ্য ছাড়া, ম্যান্টিকোর নতুন সিম্বলিক লেনদেন দিয়ে কন্ট্রাক্টটি অন্বেষণ করবে যতক্ষণ না এটি কন্ট্রাক্টে নতুন পাথ অন্বেষণ করা বন্ধ করে। ম্যান্টিকোর একটি ব্যর্থ লেনদেনের পরে (যেমন: রিভার্টের পরে) নতুন লেনদেন চালায় না।

ম্যান্টিকোর একটি mcore_* ডিরেক্টরিতে তথ্য আউটপুট করবে। অন্যান্য জিনিসের মধ্যে, আপনি এই ডিরেক্টরিতে পাবেন:

• global.summary: কভারেজ এবং কম্পাইলার সতর্কতা
• test_XXXXX.summary: কভারেজ, শেষ নির্দেশিকা, প্রতিটি টেস্ট কেসের জন্য একাউন্ট ব্যালেন্স
• test_XXXXX.tx: প্রতিটি টেস্ট কেসের জন্য লেনদেনের বিস্তারিত তালিকা

এখানে ম্যান্টিকোর 7টি টেস্ট কেস খুঁজে পেয়েছে, যা নিচেরগুলোর সাথে মিলে যায় (ফাইলের নামের ক্রম পরিবর্তন হতে পারে):

অন্বেষণ সারাংশ f(!=65) নির্দেশ করে যে f-কে 65 ছাড়া অন্য যেকোনো মান দিয়ে কল করা হয়েছে।

যেমনটি আপনি লক্ষ্য করতে পারেন, ম্যান্টিকোর প্রতিটি সফল বা রিভার্ট হওয়া লেনদেনের জন্য একটি অনন্য টেস্ট কেস তৈরি করে।

আপনি যদি দ্রুত কোড অন্বেষণ চান তবে --quick-mode ফ্ল্যাগ ব্যবহার করুন (এটি বাগ ডিটেক্টর, গ্যাস গণনা ইত্যাদি নিষ্ক্রিয় করে)

এপিআই-এর মাধ্যমে একটি স্মার্ট কন্ট্রাক্ট ম্যানিপুলেট করা

এই বিভাগে ম্যান্টিকোর পাইথন এপিআই-এর মাধ্যমে কীভাবে একটি স্মার্ট কন্ট্রাক্ট ম্যানিপুলেট করতে হয় তার বিস্তারিত বর্ণনা করা হয়েছে। আপনি পাইথন এক্সটেনশন *.py দিয়ে নতুন ফাইল তৈরি করতে পারেন এবং এই ফাইলে এপিআই কমান্ডগুলো (যার মূল বিষয়গুলো নিচে বর্ণনা করা হবে) যোগ করে প্রয়োজনীয় কোড লিখতে পারেন এবং তারপর $ python3 *.py কমান্ড দিয়ে এটি রান করতে পারেন। এছাড়াও আপনি নিচের কমান্ডগুলো সরাসরি পাইথন কনসোলে এক্সিকিউট করতে পারেন, কনসোল রান করতে $ python3 কমান্ড ব্যবহার করুন।

একাউন্ট তৈরি করা

আপনার প্রথম যে কাজটি করা উচিত তা হলো নিচের কমান্ডগুলো দিয়ে একটি নতুন ব্লকচেইন শুরু করা:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
কপি করুন

একটি নন-কন্ট্রাক্ট একাউন্ট m.create_account (opens in a new tab)-এর মাধ্যমে তৈরি করা হয়:

1user_account = m.create_account(balance=1000)
কপি করুন

একটি সলিডিটি কন্ট্রাক্ট m.solidity_create_contract (opens in a new tab)-এর মাধ্যমে ডিপ্লয় করা যেতে পারে:

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_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) লেনদেন: শুধুমাত্র একটি ফাংশন অন্বেষণ করা হয়

র (Raw) লেনদেন

একটি র লেনদেন m.transaction (opens in a new tab)-এর মাধ্যমে এক্সিকিউট করা হয়:

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
কপি করুন

কলার, এডড্রেস, ডাটা বা লেনদেনের মান কংক্রিট বা সিম্বলিক হতে পারে:

• m.make_symbolic_value (opens in a new tab) একটি সিম্বলিক মান তৈরি করে।
• m.make_symbolic_buffer(size) (opens in a new tab) একটি সিম্বলিক বাইট অ্যারে তৈরি করে।

উদাহরণস্বরূপ:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
কপি করুন

যদি ডাটা সিম্বলিক হয়, ম্যান্টিকোর লেনদেন এক্সিকিউশনের সময় কন্ট্রাক্টের সমস্ত ফাংশন অন্বেষণ করবে। ফাংশন নির্বাচন কীভাবে কাজ করে তা বোঝার জন্য Hands on the Ethernaut CTF (opens in a new tab) আর্টিকেলে ফলব্যাক ফাংশনের ব্যাখ্যা দেখা সহায়ক হবে।

নেমড (Named) লেনদেন

ফাংশনগুলো তাদের নামের মাধ্যমে এক্সিকিউট করা যেতে পারে। user_account থেকে একটি সিম্বলিক মান এবং 0 ইথার দিয়ে f(uint var) এক্সিকিউট করতে, ব্যবহার করুন:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
কপি করুন

যদি লেনদেনের value নির্দিষ্ট করা না থাকে, তবে এটি ডিফল্টভাবে 0 হয়।

সারাংশ

• একটি লেনদেনের আর্গুমেন্ট কংক্রিট বা সিম্বলিক হতে পারে
• একটি র লেনদেন সমস্ত ফাংশন অন্বেষণ করবে
• ফাংশন তাদের নাম দিয়ে কল করা যেতে পারে

ওয়ার্কস্পেস

m.workspace হলো সেই ডিরেক্টরি যা তৈরি করা সমস্ত ফাইলের আউটপুট ডিরেক্টরি হিসেবে ব্যবহৃত হয়:

1print("Results are in {}".format(m.workspace))
কপি করুন

অন্বেষণ শেষ করা

অন্বেষণ থামাতে m.finalize() (opens in a new tab) ব্যবহার করুন। এই মেথডটি কল করার পরে আর কোনো লেনদেন পাঠানো উচিত নয় এবং ম্যান্টিকোর অন্বেষণ করা প্রতিটি পাথের জন্য টেস্ট কেস তৈরি করে।

সারাংশ: ম্যান্টিকোরের অধীনে রান করা

আগের সমস্ত ধাপ একসাথে করলে, আমরা পাই:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # অনুসন্ধান থামান
সব দেখানকপি করুন

উপরের সমস্ত কোড আপনি example_run.py (opens in a new tab)-এ খুঁজে পেতে পারেন

থ্রোয়িং পাথগুলো পাওয়া

আমরা এখন f()-এ এক্সেপশন তৈরি করা পাথগুলোর জন্য নির্দিষ্ট ইনপুট তৈরি করব। লক্ষ্য এখনও নিচের স্মার্ট কন্ট্রাক্টটি example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
কপি করুন

স্টেট তথ্য ব্যবহার করা

এক্সিকিউট হওয়া প্রতিটি পাথের নিজস্ব ব্লকচেইন স্টেট থাকে। একটি স্টেট হয় প্রস্তুত (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): সমস্ত স্টেট

1for state in m.all_states:
2    # স্টেট নিয়ে কিছু করুন
কপি করুন

আপনি স্টেট তথ্য অ্যাক্সেস করতে পারেন। উদাহরণস্বরূপ:

• state.platform.get_balance(account.address): একাউন্টের ব্যালেন্স
• state.platform.transactions: লেনদেনের তালিকা
• state.platform.transactions[-1].return_data: শেষ লেনদেনের মাধ্যমে রিটার্ন করা ডাটা

শেষ লেনদেনের মাধ্যমে রিটার্ন করা ডাটা হলো একটি অ্যারে, যা ABI.deserialize দিয়ে একটি মানে রূপান্তর করা যেতে পারে, উদাহরণস্বরূপ:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
কপি করুন

কীভাবে টেস্টকেস তৈরি করবেন

টেস্টকেস তৈরি করতে m.generate_testcase(state, name) (opens in a new tab) ব্যবহার করুন:

1m.generate_testcase(state, 'BugFound')
কপি করুন

সারাংশ

• আপনি m.all_states দিয়ে স্টেটের উপর ইটারেট করতে পারেন
• state.platform.get_balance(account.address) একাউন্টের ব্যালেন্স রিটার্ন করে
• state.platform.transactions লেনদেনের তালিকা রিটার্ন করে
• transaction.return_data হলো রিটার্ন করা ডাটা
• m.generate_testcase(state, name) স্টেটের জন্য ইনপুট তৈরি করে

সারাংশ: থ্রোয়িং পাথ পাওয়া

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14# # চেক করুন একটি এক্সিকিউশন REVERT বা INVALID দিয়ে শেষ হয় কিনা
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
সব দেখানকপি করুন

উপরের সমস্ত কোড আপনি example_run.py (opens in a new tab)-এ খুঁজে পেতে পারেন

দ্রষ্টব্য: আমরা আরও সহজ একটি স্ক্রিপ্ট তৈরি করতে পারতাম, কারণ terminated_state দ্বারা রিটার্ন করা সমস্ত স্টেটের ফলাফলে REVERT বা INVALID থাকে: এই উদাহরণটি শুধুমাত্র এপিআই কীভাবে ম্যানিপুলেট করতে হয় তা দেখানোর জন্য ছিল।

কনস্ট্রেইন্ট যোগ করা

আমরা দেখব কীভাবে অন্বেষণকে সীমাবদ্ধ (constrain) করতে হয়। আমরা ধরে নেব যে f()-এর ডকুমেন্টেশনে বলা হয়েছে যে ফাংশনটি কখনোই a == 65 দিয়ে কল করা হয় না, তাই a == 65 সহ কোনো বাগ আসল বাগ নয়। লক্ষ্য এখনও নিচের স্মার্ট কন্ট্রাক্টটি example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
কপি করুন

অপারেটর

Operators (opens in a new tab) মডিউলটি কনস্ট্রেইন্ট ম্যানিপুলেট করা সহজ করে, অন্যান্য জিনিসের মধ্যে এটি প্রদান করে:

• Operators.AND,
• Operators.OR,
• Operators.UGT (আনসাইনড গ্রেটার দ্যান),
• Operators.UGE (আনসাইনড গ্রেটার দ্যান অর ইকুয়াল টু),
• Operators.ULT (আনসাইনড লোয়ার দ্যান),
• Operators.ULE (আনসাইনড লোয়ার দ্যান অর ইকুয়াল টু)।

মডিউলটি ইমপোর্ট করতে নিচেরটি ব্যবহার করুন:

1from manticore.core.smtlib import Operators
কপি করুন

Operators.CONCAT একটি অ্যারেকে একটি মানের সাথে যুক্ত (concatenate) করতে ব্যবহৃত হয়। উদাহরণস্বরূপ, একটি লেনদেনের return_data-কে অন্য একটি মানের বিপরীতে চেক করার জন্য একটি মানে পরিবর্তন করতে হবে:

1last_return = Operators.CONCAT(256, *last_return)
কপি করুন

কনস্ট্রেইন্ট

আপনি বিশ্বব্যাপী (globally) বা একটি নির্দিষ্ট স্টেটের জন্য কনস্ট্রেইন্ট ব্যবহার করতে পারেন।

গ্লোবাল কনস্ট্রেইন্ট

একটি গ্লোবাল কনস্ট্রেইন্ট যোগ করতে m.constrain(constraint) ব্যবহার করুন। উদাহরণস্বরূপ, আপনি একটি সিম্বলিক এডড্রেস থেকে একটি কন্ট্রাক্ট কল করতে পারেন এবং এই এডড্রেসটিকে নির্দিষ্ট মান হতে সীমাবদ্ধ করতে পারেন:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
কপি করুন

স্টেট কনস্ট্রেইন্ট

একটি নির্দিষ্ট স্টেটে কনস্ট্রেইন্ট যোগ করতে state.constrain(constraint) (opens in a new tab) ব্যবহার করুন। এটি অন্বেষণের পরে স্টেটের উপর কোনো প্রপার্টি চেক করার জন্য স্টেটকে সীমাবদ্ধ করতে ব্যবহৃত হতে পারে।

কনস্ট্রেইন্ট চেক করা

একটি কনস্ট্রেইন্ট এখনও কার্যকর কিনা তা জানতে solver.check(state.constraints) ব্যবহার করুন। উদাহরণস্বরূপ, নিচেরটি symbolic_value-কে 65 থেকে ভিন্ন হতে সীমাবদ্ধ করবে এবং স্টেটটি এখনও কার্যকর কিনা তা চেক করবে:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # স্টেটটি সম্ভব
কপি করুন

সারাংশ: কনস্ট্রেইন্ট যোগ করা

আগের কোডে কনস্ট্রেইন্ট যোগ করলে, আমরা পাই:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19# # চেক করুন একটি এক্সিকিউশন REVERT বা INVALID দিয়ে শেষ হয় কিনা
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # আমরা সেই পাথটি বিবেচনা করি না যেখানে a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
সব দেখানকপি করুন

উপরের সমস্ত কোড আপনি example_run.py (opens in a new tab)-এ খুঁজে পেতে পারেন

পেজ সর্বশেষ আপডেট: 3 মার্চ, 2026

m (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+7

অবদানকারীদের দেখুন