Ruka hadi kwenye maudhui makuu

Jinsi ya kutumia Manticore kupata hitilafu kwenye mikataba mahiri

Solidity
mikataba mahiri
usalama
upimaji
uthibitishaji rasmi
Ya juu
Trailofbits
13 Januari 2020
11 dakika za kusoma

Lengo la mafunzo haya ni kuonyesha jinsi ya kutumia Manticore kupata hitilafu kiotomatiki kwenye mikataba mahiri.

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 inaendesha eth-security-toolbox kwenye docker ambayo ina ufikiaji wa saraka yako ya sasa. Unaweza kubadilisha faili kutoka kwa mwenyeji wako, na kuendesha 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 unaobadilika (dynamic symbolic execution)

Utekelezaji wa Ishara Unaobadilika kwa Ufupi

Utekelezaji wa ishara unaobadilika (DSE) ni mbinu ya uchanganuzi wa programu ambayo inachunguza nafasi ya hali kwa kiwango cha juu cha ufahamu wa kisemantiki. Mbinu hii inategemea ugunduzi wa "njia za programu", zinazowakilishwa kama fomula za hisabati zinazoitwa path predicates. Kimawazo, mbinu hii inafanya kazi kwenye viarifu vya njia katika hatua mbili:

  1. Zinajengwa kwa kutumia vikwazo kwenye ingizo la programu.
  2. Zinatumiwa kuzalisha maingizo ya programu ambayo yatasababisha njia zinazohusiana kutekelezwa.

Mbinu hii haitoi chanya za uongo kwa maana kwamba hali zote za programu zilizotambuliwa zinaweza kuanzishwa wakati wa utekelezaji halisi. Kwa mfano, ikiwa uchanganuzi utapata mzidio wa nambari kamili, unahakikishwa kuwa unaweza kuzalishwa tena.

Mfano wa Kiarifu cha Njia

Ili kupata ufahamu wa jinsi DSE inavyofanya kazi, fikiria mfano ufuatao:

function f(uint a){

  if (a == 65) {
      // Kuna hitilafu
  }

}

Kwa kuwa f() ina njia mbili, DSE itajenga viarifu viwili tofauti vya njia:

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

Kila kiarifu cha njia ni fomula ya hisabati ambayo inaweza kupewa kile kinachoitwa mtatuaji wa SMT (opens in a new tab), ambaye atajaribu kutatua mlinganyo. Kwa Path 1, mtatuaji atasema kwamba njia inaweza kuchunguzwa kwa a = 65. Kwa Path 2, mtatuaji anaweza kutoa a thamani yoyote isipokuwa 65, kwa mfano a = 0.

Kuthibitisha sifa

Manticore inaruhusu udhibiti kamili juu ya utekelezaji wote wa kila njia. Kama matokeo, inakuruhusu kuongeza vikwazo vya kiholela kwa karibu chochote. Udhibiti huu unaruhusu uundaji wa sifa kwenye mkataba.

Fikiria mfano ufuatao:

function unsafe_add(uint a, uint b) returns(uint c){
  c = a + b; // hakuna ulinzi wa mzidio
  return c;
}

Hapa kuna njia moja tu ya kuchunguza katika fanksheni:

  • Njia ya 1: c = a + b

Kwa kutumia Manticore, unaweza kuangalia mzidio, na kuongeza vikwazo kwenye kiarifu cha njia:

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

Ikiwa inawezekana kupata uthamini wa a na b ambao kiarifu cha njia hapo juu kinawezekana, inamaanisha kuwa umepata mzidio. Kwa mfano mtatuaji anaweza kuzalisha ingizo a = 10 , b = MAXUINT256.

Ikiwa utafikiria toleo lililorekebishwa:

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

Fomula inayohusiana na ukaguzi wa mzidio itakuwa:

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

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

DSE kwa hivyo ni zana yenye nguvu, inayoweza kuthibitisha vikwazo vya kiholela kwenye msimbo wako.

Kuendesha chini ya Manticore

Tutaona jinsi ya kuchunguza mkataba mahiri na API ya Manticore. Lengo ni mkataba mahiri ufuatao example.sol (opens in a new tab):

Endesha uchunguzi wa kujitegemea

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

$ manticore project

Utapata matokeo ya visa vya majaribio kama hii (mpangilio unaweza kubadilika):

Bila maelezo ya ziada, Manticore itachunguza mkataba na miamala mipya ya ishara hadi isichunguze njia mpya kwenye mkataba. Manticore haiendeshi miamala mipya baada ya ile iliyoshindwa (k.m: baada ya kutengua).

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

  • global.summary: ufikiaji na maonyo ya kikusanyaji
  • test_XXXXX.summary: ufikiaji, maagizo ya mwisho, salio la akaunti kwa kila kisa cha majaribio
  • test_XXXXX.tx: orodha ya kina ya miamala kwa kila kisa cha majaribio

Hapa Manticore inagundua visa 7 vya majaribio, ambavyo vinalingana na (mpangilio wa jina la faili unaweza kubadilika):

Muamala 0Muamala 1Muamala 2Matokeo
test_00000000.txUundaji wa mkatabaf(!=65)f(!=65)STOP
test_00000001.txUundaji wa mkatabafanksheni mbadalaREVERT
test_00000002.txUundaji wa mkatabaRETURN
test_00000003.txUundaji wa mkatabaf(65)REVERT
test_00000004.txUundaji wa mkatabaf(!=65)STOP
test_00000005.txUundaji wa mkatabaf(!=65)f(65)REVERT
test_00000006.txUundaji wa mkatabaf(!=65)fanksheni mbadalaREVERT

Muhtasari wa uchunguzi f(!=65) unaonyesha f inaitwa na thamani yoyote tofauti na 65.

Kama unavyoweza kugundua, Manticore inazalisha kisa cha kipekee cha majaribio kwa kila muamala uliofanikiwa au uliotenguliwa.

Tumia alama ya --quick-mode ikiwa unataka uchunguzi wa haraka wa msimbo (inazima vigunduzi vya hitilafu, ukokotoaji wa gesi, ...)

Dhibiti mkataba mahiri kupitia API

Sehemu hii inaelezea maelezo ya jinsi ya kudhibiti mkataba mahiri kupitia API ya Python ya Manticore. Unaweza kuunda faili mpya na kiendelezi cha python *.py na uandike msimbo unaohitajika kwa kuongeza amri za API (misingi ambayo itaelezwa hapa chini) kwenye faili hili na kisha uiendeshe kwa amri $ python3 *.py. Pia unaweza kutekeleza amri hapa chini moja kwa moja kwenye kiweko cha python, ili kuendesha kiweko tumia amri $ python3.

Kuunda Akaunti

Jambo la kwanza unalopaswa kufanya ni kuanzisha mnyororo wa vitalu mpya kwa amri zifuatazo:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

Mkataba wa Solidity unaweza kusambazwa kwa kutumia m.solidity_create_contract (opens in a new tab):

Muhtasari

Kutekeleza miamala

Manticore inasaidia aina mbili za muamala:

  • Muamala ghafi: fanksheni zote zinachunguzwa
  • Muamala uliotajwa: fanksheni moja tu inachunguzwa

Muamala ghafi

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

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

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

Kwa mfano:

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)

Ikiwa data ni ya ishara, Manticore itachunguza fanksheni zote za mkataba wakati wa utekelezaji wa muamala. Itakuwa na manufaa kuona maelezo ya Fanksheni Mbadala katika makala ya Hands on the Ethernaut CTF (opens in a new tab) kwa kuelewa jinsi uteuzi wa fanksheni unavyofanya kazi.

Muamala uliotajwa

Fanksheni zinaweza kutekelezwa kupitia jina lake. Ili kutekeleza f(uint var) na thamani ya ishara, kutoka kwa user_account, na kwa Etha 0, tumia:

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

Ikiwa value ya muamala haijabainishwa, ni 0 kwa chaguo-msingi.

Muhtasari

  • Hoja za muamala zinaweza kuwa halisi au za ishara
  • Muamala ghafi utachunguza fanksheni zote
  • Fanksheni inaweza kuitwa kwa jina lake

Nafasi ya kazi

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

print("Results are in {}".format(m.workspace))

Sitisha Uchunguzi

Ili kusimamisha uchunguzi tumia m.finalize() (opens in a new tab). Hakuna miamala zaidi inayopaswa kutumwa mara tu mbinu hii inapoitwa na Manticore inazalisha visa vya majaribio kwa kila njia iliyochunguzwa.

Muhtasari: Kuendesha chini ya Manticore

Tukiweka hatua zote zilizopita pamoja, tunapata:

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

Kupata njia za kurusha (throwing paths)

Sasa tutazalisha maingizo maalum kwa njia zinazoibua ubaguzi katika f(). Lengo bado ni mkataba mahiri ufuatao 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();
        }
    }
}

Kutumia maelezo ya hali

Kila njia iliyotekelezwa ina hali yake ya mnyororo wa vitalu. Hali iko tayari au inauawa, ikimaanisha kuwa inafikia agizo la THROW au REVERT:

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

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:

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

Jinsi ya kuzalisha kisa cha majaribio

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

m.generate_testcase(state, 'BugFound')

Muhtasari

  • Unaweza kurudia juu ya hali na m.all_states
  • state.platform.get_balance(account.address) inarejesha salio la akaunti
  • state.platform.transactions inarejesha orodha ya miamala
  • transaction.return_data ni data iliyorejeshwa
  • m.generate_testcase(state, name) inazalisha maingizo kwa ajili ya hali

Muhtasari: Kupata Njia ya Kurusha

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

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

Kuongeza vikwazo

Tutaona jinsi ya kuzuia uchunguzi. Tutafanya dhana kwamba nyaraka za f() zinasema kwamba fanksheni haijawahi kuitwa na a == 65, kwa hivyo hitilafu yoyote na a == 65 sio hitilafu halisi. Lengo bado ni mkataba mahiri ufuatao 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();
        }
    }
}

Waendeshaji

Moduli ya Waendeshaji (opens in a new tab) inawezesha udhibiti wa vikwazo, miongoni mwa mengine inatoa:

  • Operators.AND,
  • Operators.OR,
  • Operators.UGT (isiyotiwa saini kubwa kuliko),
  • Operators.UGE (isiyotiwa saini kubwa kuliko au sawa na),
  • Operators.ULT (isiyotiwa saini ndogo kuliko),
  • Operators.ULE (isiyotiwa saini ndogo kuliko au sawa na).

Ili kuingiza moduli tumia yafuatayo:

from manticore.core.smtlib import Operators

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

last_return = Operators.CONCAT(256, *last_return)

Vikwazo

Unaweza kutumia vikwazo ulimwenguni kote au kwa hali maalum.

Kikwazo cha ulimwengu

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

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)

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 ili kuangalia sifa fulani juu yake.

Kuangalia Kikwazo

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

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # hali inatekelezeka

Muhtasari: Kuongeza Vikwazo

Kuongeza kikwazo kwenye msimbo uliopita, tunapata:

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