స్మార్ట్ కాంట్రాక్ట్‌లలో బగ్‌లను కనుగొనడానికి మాంటికోర్‌ను ఎలా ఉపయోగించాలి

ఈ ట్యుటోరియల్ యొక్క ఉద్దేశ్యం స్మార్ట్ కాంట్రాక్ట్‌లలో బగ్‌లను స్వయంచాలకంగా కనుగొనడానికి మాంటికోర్‌ను ఎలా ఉపయోగించాలో చూపించడం.

ఇన్‌స్టాలేషన్

మాంటికోర్‌కు >= 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) సంగ్రహంగా

డైనమిక్ సింబాలిక్ ఎగ్జిక్యూషన్ (DSE) అనేది అధిక స్థాయి సెమాంటిక్ అవగాహనతో స్థితి (state) స్పేస్‌ను అన్వేషించే ప్రోగ్రామ్ విశ్లేషణ సాంకేతికత. ఈ సాంకేతికత "ప్రోగ్రామ్ పాత్‌ల" అన్వేషణపై ఆధారపడి ఉంటుంది, వీటిని path predicates అని పిలువబడే గణిత సూత్రాలుగా సూచిస్తారు. సంభావితంగా, ఈ సాంకేతికత పాత్ ప్రెడికేట్‌లపై రెండు దశల్లో పనిచేస్తుంది:

1. ప్రోగ్రామ్ ఇన్‌పుట్‌పై పరిమితులను ఉపయోగించి అవి నిర్మించబడతాయి.
2. అనుబంధిత పాత్‌లను అమలు చేయడానికి కారణమయ్యే ప్రోగ్రామ్ ఇన్‌పుట్‌లను రూపొందించడానికి అవి ఉపయోగించబడతాయి.

గుర్తించబడిన అన్ని ప్రోగ్రామ్ స్థితులను కాంక్రీట్ ఎగ్జిక్యూషన్ సమయంలో ట్రిగ్గర్ చేయవచ్చు కాబట్టి ఈ విధానం ఎలాంటి ఫాల్స్ పాజిటివ్‌లను ఉత్పత్తి చేయదు. ఉదాహరణకు, విశ్లేషణలో పూర్ణాంక ఓవర్‌ఫ్లో కనుగొనబడితే, అది పునరుత్పత్తి చేయబడుతుందని హామీ ఇవ్వబడుతుంది.

పాత్ ప్రెడికేట్ ఉదాహరణ

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.

లక్షణాలను ధృవీకరించడం

ప్రతి పాత్ యొక్క మొత్తం ఎగ్జిక్యూషన్‌పై మాంటికోర్ పూర్తి నియంత్రణను అనుమతిస్తుంది. ఫలితంగా, ఇది దాదాపు దేనికైనా ఏకపక్ష పరిమితులను జోడించడానికి మిమ్మల్ని అనుమతిస్తుంది. ఈ నియంత్రణ కాంట్రాక్ట్‌పై లక్షణాలను సృష్టించడానికి అనుమతిస్తుంది.

కింది ఉదాహరణను పరిశీలించండి:

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: టెస్ట్‌కేస్ నం. 0 రూపొందించబడింది - STOP
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 1 రూపొందించబడింది - REVERT
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 2 రూపొందించబడింది - RETURN
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 3 రూపొందించబడింది - REVERT
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 4 రూపొందించబడింది - STOP
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 5 రూపొందించబడింది - REVERT
... m.c.manticore:INFO: టెస్ట్‌కేస్ నం. 6 రూపొందించబడింది - REVERT
... m.c.manticore:INFO: ఫలితాలు /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) అనేది 65కి భిన్నమైన ఏదైనా విలువతో పిలువబడే fని సూచిస్తుంది.

మీరు గమనించినట్లుగా, ప్రతి విజయవంతమైన లేదా రివర్ట్ చేయబడిన లావాదేవీకి మాంటికోర్ ఒక ప్రత్యేకమైన టెస్ట్ కేస్‌ను రూపొందిస్తుంది.

మీకు వేగవంతమైన కోడ్ అన్వేషణ కావాలంటే --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)

m.solidity_create_contract (opens in a new tab) ఉపయోగించి Solidity కాంట్రాక్ట్‌ను డిప్లాయ్ చేయవచ్చు:

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)

కాలర్, చిరునామా, డేటా లేదా లావాదేవీ విలువ కాంక్రీట్ లేదా సింబాలిక్ కావచ్చు:

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

డేటా సింబాలిక్ అయితే, లావాదేవీ అమలు సమయంలో మాంటికోర్ కాంట్రాక్ట్ యొక్క అన్ని ఫంక్షన్‌లను అన్వేషిస్తుంది. ఫంక్షన్ ఎంపిక ఎలా పనిచేస్తుందో అర్థం చేసుకోవడానికి హ్యాండ్స్ ఆన్ ది ఈథర్‌నాట్ CTF (opens in a new tab) కథనంలోని ఫాల్‌బ్యాక్ ఫంక్షన్ వివరణను చూడటం సహాయకరంగా ఉంటుంది.

పేరున్న లావాదేవీ

ఫంక్షన్‌లను వాటి పేరు ద్వారా అమలు చేయవచ్చు. user_account నుండి సింబాలిక్ విలువతో మరియు 0 ఈథర్‌తో f(uint var)ని అమలు చేయడానికి, దీన్ని ఉపయోగించండి:

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

లావాదేవీ యొక్క value పేర్కొనబడకపోతే, అది అప్రమేయంగా 0 అవుతుంది.

సారాంశం

• లావాదేవీ యొక్క ఆర్గ్యుమెంట్‌లు కాంక్రీట్ లేదా సింబాలిక్ కావచ్చు
• ముడి లావాదేవీ అన్ని ఫంక్షన్‌లను అన్వేషిస్తుంది
• ఫంక్షన్‌ను వాటి పేరు ద్వారా పిలవవచ్చు

వర్క్‌స్పేస్

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)లో కనుగొనవచ్చు

త్రోయింగ్ పాత్‌లను పొందడం

మేము ఇప్పుడు 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();
        }
    }
}

స్థితి సమాచారాన్ని ఉపయోగించడం

అమలు చేయబడిన ప్రతి పాత్‌కు దాని బ్లాక్‌చైన్ స్థితి ఉంటుంది. ఒక స్థితి సిద్ధంగా ఉంటుంది లేదా అది చంపబడుతుంది (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: చివరి లావాదేవీ ద్వారా అందించబడిన డేటా

చివరి లావాదేవీ ద్వారా అందించబడిన డేటా ఒక శ్రేణి (array), దీనిని 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();
        }
    }
}

ఆపరేటర్లు

ఆపరేటర్లు (opens in a new tab) మాడ్యూల్ పరిమితుల తారుమారుని సులభతరం చేస్తుంది, ఇతర వాటితో పాటు ఇది వీటిని అందిస్తుంది:

• Operators.AND,
• Operators.OR,
• Operators.UGT (అన్‌సైన్డ్ గ్రేటర్ దేన్),
• Operators.UGE (అన్‌సైన్డ్ గ్రేటర్ దేన్ లేదా ఈక్వల్ టు),
• Operators.ULT (అన్‌సైన్డ్ లోయర్ దేన్),
• Operators.ULE (అన్‌సైన్డ్ లోయర్ దేన్ లేదా ఈక్వల్ టు).

మాడ్యూల్‌ను దిగుమతి చేయడానికి కింది వాటిని ఉపయోగించండి:

from manticore.core.smtlib import Operators

శ్రేణిని విలువకు కలపడానికి (concatenate) Operators.CONCAT ఉపయోగించబడుతుంది. ఉదాహరణకు, లావాదేవీ యొక్క 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)లో కనుగొనవచ్చు