Jinsi ya kutumia Manticore kupata hitilafu katika Mkataba-erevu

Lengo la mafunzo haya ni kuonyesha jinsi ya kutumia Manticore kupata hitilafu kiotomatiki katika Mkataba-erevu.

Usakinishaji

Manticore inahitaji >= python 3.6. Inaweza kusakinishwa kupitia pip au kwa kutumia docker.

Manticore kupitia docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

Amri ya mwisho huendesha eth-security-toolbox kwenye docker ambayo ina ufikiaji wa saraka yako ya sasa. Unaweza kubadilisha faili kutoka kwa mwenyeji wako, na uendeshe zana kwenye faili kutoka kwa docker

Ndani ya docker, endesha:

solc-select 0.5.11
cd /home/trufflecon/

Manticore kupitia pip

pip3 install --user manticore

solc 0.5.11 inapendekezwa.

Kuendesha hati

Ili kuendesha hati ya python na python 3:

python3 script.py

Utangulizi wa utekelezaji wa ishara wenye nguvu

Utekelezaji wa Ishara Wenye Nguvu kwa Kifupi

Utekelezaji wa ishara wenye nguvu (DSE) ni mbinu ya uchambuzi wa programu ambayo inachunguza nafasi ya hali na kiwango cha juu cha ufahamu wa kisemantiki. Mbinu hii inategemea ugunduzi wa "njia za programu", zinazowakilishwa kama kanuni za hisabati zinazoitwa path predicates. Kimsingi, mbinu hii hufanya kazi kwenye viarifu vya njia katika hatua mbili:

1. Zinajengwa kwa kutumia vikwazo kwenye pembejeo ya programu.
2. Zinatumika kutengeneza pembejeo za programu ambazo zitasababisha njia zinazohusiana kutekelezwa.

Mbinu hii haitoi chanya za uwongo kwa maana kwamba hali zote za programu zilizotambuliwa zinaweza kuanzishwa wakati wa utekelezaji halisi. Kwa mfano, ikiwa uchambuzi utapata kufurika kwa nambari, imehakikishwa kuwa inaweza kuzalishwa tena.

Mfano wa Kiarifu cha Njia

Ili kupata maarifa ya jinsi DSE inavyofanya kazi, zingatia mfano ufuatao:

1function f(uint a){
2
3  if (a == 65) {
4      // Kuna hitilafu
5  }
6
7}
Nakala

Kwa vile f() ina njia mbili, DSE itaunda viarifu viwili tofauti vya njia:

• Njia ya 1: a == 65
• Njia ya 2: Si (a == 65)

Kila kiarifu cha njia ni fomula ya hisabati ambayo inaweza kupewa kile kinachoitwa SMT solver (opens in a new tab), ambayo itajaribu kutatua mlingano. Kwa Njia 1, kisuluhishi kitasema kuwa njia inaweza kuchunguzwa na a = 65. Kwa Njia 2, kisuluhishi kinaweza kutoa a thamani yoyote isipokuwa 65, kwa mfano a = 0.

Kuthibitisha sifa

Manticore inaruhusu udhibiti kamili juu ya utekelezaji wote wa kila njia. Kwa hivyo, hukuruhusu kuongeza vikwazo vya kiholela kwa karibu kila kitu. Udhibiti huu unaruhusu uundaji wa sifa kwenye mkataba.

Fikiria mfano ufuatao:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // hakuna ulinzi wa kufurika
3  return c;
4}
Nakala

Hapa kuna njia moja tu ya kuchunguza katika kitendakazi:

• Njia ya 1: c = a + b

Ukitumia Manticore, unaweza kuangalia kufurika, na kuongeza vikwazo kwa kiarifu cha njia:

• c = a + b NA (c < a AU c < b)

Ikiwezekana kupata uthamini wa a na b ambapo kiarifu cha njia hapo juu kinawezekana, inamaanisha kuwa umepata kufurika. Kwa mfano, kisuluhishi kinaweza kutoa ingizo a = 10, b = MAXUINT256.

Ukizingatia toleo lililorekebishwa:

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}
Nakala

Fomula inayohusishwa na ukaguzi wa kufurika itakuwa:

• c = a + b NA (c >= a) NA (c=>b) NA (c < a AU c < b)

Fomula hii haiwezi kutatuliwa; kwa maneno mengine huu ni uthibitisho kwamba katika safe_add, c itaongezeka kila wakati.

Kwa hivyo DSE ni zana yenye nguvu, ambayo inaweza kuthibitisha vikwazo vya kiholela kwenye msimbo wako.

Inaendeshwa chini ya Manticore

Tutaona jinsi ya kuchunguza Mkataba-erevu na API ya Manticore. Lengo ni Mkataba-erevu ufuatao 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}
Onyesha yote
Nakala

Endesha uchunguzi wa pekee

Unaweza kuendesha Manticore moja kwa moja kwenye Mkataba-erevu kwa amri ifuatayo (project inaweza kuwa Faili ya Solidity, au saraka ya mradi):

$ manticore project

Utapata matokeo ya kesi za majaribio kama hii (mpangilio unaweza kubadilika):

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...
Onyesha yote

Bila maelezo ya ziada, Manticore itachunguza mkataba na miamala mipya ya ishara hadi isichugunze njia mpya kwenye mkataba. Manticore haiendeshi miamala mipya baada ya ule ulioshindwa (k.m: baada ya kurudishwa).

Manticore itatoa taarifa katika saraka ya mcore_*. Miongoni mwa mengine, utapata katika saraka hii:

• global.summary: ufikiaji na maonyo ya mkusanyaji
• test_XXXXX.summary: ufikiaji, maagizo ya mwisho, salio za akaunti kwa kila kesi ya jaribio
• test_XXXXX.tx: orodha ya kina ya miamala kwa kila kesi ya jaribio

Hapa Manticore ilipata kesi 7 za majaribio, ambazo zinalingana na (mpangilio wa jina la faili unaweza kubadilika):

Muhtasari wa uchunguzi f(!=65) unaashiria f kuitwa na thamani yoyote tofauti na 65.

Kama unavyoweza kuona, Manticore inazalisha kesi ya kipekee ya majaribio kwa kila muamala uliofaulu au uliorudishwa.

Tumia alama ya --quick-mode ikiwa unataka uchunguzi wa haraka wa msimbo (huzima vitambua hitilafu, ukokotoaji wa gesi, ...)

Kudhibiti Mkataba-erevu kupitia API

Sehemu hii inaelezea kwa undani jinsi ya kudhibiti Mkataba-erevu kupitia API ya Python ya Manticore. Unaweza kuunda faili mpya yenye kiendelezi cha python *.py na uandike msimbo unaohitajika kwa kuongeza amri za API (misingi yake itaelezwa hapa chini) kwenye faili hii na kisha kuiendesha kwa amri ya $ python3 *.py. Pia unaweza kutekeleza amri zilizo hapa chini moja kwa moja kwenye konsoli ya python, ili kuendesha konsoli tumia amri ya $ python3.

Kuunda Akaunti

Jambo la kwanza unapaswa kufanya ni kuanzisha mnyororo wa bloku mpya na amri zifuatazo:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
Nakala

Akaunti isiyo ya mkataba inaundwa kwa kutumia m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)
Nakala

Mkataba wa Solidity unaweza kusambazwa kwa kutumia 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# Anzisha mkataba
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Onyesha yote
Nakala

Muhtasari

• Unaweza kuunda akaunti za mtumiaji na akaunti za mkataba kwa kutumia m.create_account (opens in a new tab) na m.solidity_create_contract (opens in a new tab).

Kutekeleza miamala

Manticore inasaidia aina mbili za miamala:

• Muamala ghafi: vitendakazi vyote vinachunguzwa
• Muamala wenye jina: kitendakazi kimoja tu ndicho kinachunguzwa

Muamala ghafi

Muamala ghafi unatekelezwa kwa kutumia m.transaction (opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
Nakala

Mpigaji simu, anwani, data, au thamani ya muamala inaweza kuwa halisi au ya kiishara:

• m.make_symbolic_value (opens in a new tab) huunda thamani ya kiishara.
• m.make_symbolic_buffer(size) (opens in a new tab) huunda safu ya baiti ya kiishara.

Kwa mfano:

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

Ikiwa data ni ya kiishara, Manticore itachunguza vitendakazi vyote vya mkataba wakati wa utekelezaji wa muamala. Itakuwa na msaada kuona maelezo ya Kitendaji cha Kurudi Nyuma katika makala ya Hands on the Ethernaut CTF (opens in a new tab) kwa kuelewa jinsi uteuzi wa kitendakazi unavyofanya kazi.

Muamala wenye jina

Vitendakazi vinaweza kutekelezwa kupitia jina lao. Ili kutekeleza f(uint var) na thamani ya kiishara, kutoka user_account, na ether 0, tumia:

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

Ikiwa thamani ya muamala haijaainishwa, ni 0 kwa chaguo-msingi.

Muhtasari

• Hoja za muamala zinaweza kuwa halisi au za kiishara
• Muamala ghafi utachunguza vitendakazi vyote
• Kitendakazi kinaweza kuitwa kwa jina lake

Eneo la kazi

m.workspace ni saraka inayotumika kama saraka ya matokeo kwa faili zote zinazozalishwa:

1print("Matokeo yako katika {}".format(m.workspace))
Nakala

Sisha Uchunguzi

Ili kusimamisha uchunguzi tumia m.finalize() (opens in a new tab). Hakuna miamala zaidi inapaswa kutumwa mara tu mbinu hii inapoitwa na Manticore hutoa kesi za majaribio kwa kila njia iliyochunguzwa.

Muhtasari: Inaendeshwa chini ya Manticore

Kuweka hatua zote zilizopita pamoja, tunapata:

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("Matokeo yako katika {}".format(m.workspace))
15m.finalize() # simamisha uchunguzi
Onyesha yote
Nakala

Msimbo wote hapo juu unaweza kuupata katika example_run.py (opens in a new tab)

Kupata njia za kurusha

Sasa tutatoa pembejeo maalum kwa njia zinazoibua ubaguzi katika f(). Lengo bado ni Mkataba-erevu ufuatao 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}
Nakala

Kutumia taarifa ya hali

Kila njia inayotekelezwa ina hali yake ya mnyororo wa bloku. Hali iko tayari au inauawa, ikimaanisha kwamba inafikia maagizo ya KUTUPA au KURUDISHA:

• m.ready_states (opens in a new tab): orodha ya hali ambazo ziko tayari (hazikutekeleza REVERT/INVALID)
• m.killed_states (opens in a new tab): orodha ya hali ambazo zimeuawa
• m.all_states (opens in a new tab): hali zote

1for state in m.all_states:
2    # fanya kitu na hali
Nakala

Unaweza kufikia maelezo ya hali. Kwa mfano:

• state.platform.get_balance(account.address): salio la akaunti
• state.platform.transactions: orodha ya miamala
• state.platform.transactions[-1].return_data: data iliyorejeshwa na muamala wa mwisho

Data iliyorejeshwa na muamala wa mwisho ni safu, ambayo inaweza kubadilishwa kuwa thamani na ABI.deserialize, kwa mfano:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
Nakala

Jinsi ya kuzalisha kesi ya majaribio

Tumia m.generate_testcase(state, name) (opens in a new tab) kuzalisha kesi ya majaribio:

1m.generate_testcase(state, 'BugFound')
Nakala

Muhtasari

• Unaweza kurudia hali kwa m.all_states
• state.platform.get_balance(account.address) inarudisha salio la akaunti
• state.platform.transactions inarudisha orodha ya miamala
• transaction.return_data ni data iliyorejeshwa
• m.generate_testcase(state, name) inazalisha pembejeo za hali

Muhtasari: Kupata Njia ya Kutupa

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## Angalia ikiwa utekelezaji unaisha na REVERT au INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Tupa imepatikana {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Onyesha yote
Nakala

Msimbo wote ulio hapo juu unaweza kuupata kwenye example_run.py (opens in a new tab)

Kumbuka tungeweza kutoa hati rahisi zaidi, kwani hali zote zilizorejeshwa na terminated_state zina REVERT au INVALID katika matokeo yao: mfano huu ulikusudiwa tu kuonyesha jinsi ya kuendesha API.

Kuongeza vikwazo

Tutaona jinsi ya kuzuia uchunguzi. Tutafanya dhana kwamba nyaraka za f() inasema kwamba kitendakazi hakijaitwa kamwe na a == 65, kwa hivyo hitilafu yoyote na a == 65 sio hitilafu halisi. Lengo bado ni Mkataba-erevu ufuatao 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}
Nakala

Waendeshaji

Sehemu ya Operators (opens in a new tab) hurahisisha upotoshaji wa vikwazo, miongoni mwa vingine hutoa:

• Operators.NA,
• Operators.AU,
• Operators.UGT (kubwa kuliko isiyo na alama),
• Operators.UGE (kubwa kuliko au sawa na isiyo na alama),
• Operators.ULT (chini kuliko isiyo na alama),
• Operators.ULE (chini kuliko au sawa na isiyo na alama).

Ili kuingiza moduli tumia yafuatayo:

1from manticore.core.smtlib import Operators
Nakala

Operators.CONCAT hutumiwa kuunganisha safu kwa thamani. Kwa mfano, return_data ya muamala inahitaji kubadilishwa kuwa thamani ili kuangaliwa dhidi ya thamani nyingine:

1last_return = Operators.CONCAT(256, *last_return)
Nakala

Vikwazo

Unaweza kutumia vikwazo kimataifa au kwa hali maalum.

Kikwazo cha kimataifa

Tumia m.constrain(constraint) kuongeza kikwazo cha kimataifa. Kwa mfano, unaweza kuita mkataba kutoka kwa anwani ya ishara, na kuzuia anwani hii kuwa na maadili maalum:

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

Kikwazo cha hali

Tumia state.constrain(constraint) (opens in a new tab) kuongeza kikwazo kwa hali maalum. Inaweza kutumika kuzuia hali baada ya uchunguzi wake kuangalia mali fulani juu yake.

Kuangalia Kikwazo

Tumia solver.check(state.constraints) kujua kama kikwazo bado kinawezekana. Kwa mfano, yafuatayo yatazuia symbolic_value kuwa tofauti na 65 na kuangalia kama hali bado inawezekana:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # hali inawezekana
Nakala

Muhtasari: Kuongeza Vikwazo

Kuongeza kikwazo kwa msimbo uliopita, tunapata:

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## Angalia ikiwa utekelezaji unaisha na REVERT au INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # hatuzingatii njia ambapo a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Hitilafu imepatikana, matokeo yapo kwenye {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Hakuna hitilafu iliyopatikana')
Onyesha yote
Nakala

Msimbo wote ulio hapo juu unaweza kuupata kwenye example_run.py (opens in a new tab)

Ukurasa ulihaririwa mwisho: 26 Aprili 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+5

Ona wachangiaji