Mwongozo wa zana za usalama za mkataba-erevu

Tutatumia mbinu tatu tofauti za upimaji na uchanganuzi wa programu:

• Uchanganuzi tuli kwa kutumia Slither. Njia zote za programu hukadiriwa na kuchanganuliwa kwa wakati mmoja, kupitia uwasilishaji tofauti wa programu (k.m., control-flow-graph)
• Fuzzing na Echidna. Msimbo unatekelezwa kwa uzalishaji nasibu bandia wa miamala. Fuzzer itajaribu kupata mfuatano wa miamala ili kukiuka sifa fulani.
• Utekelezaji wa kiishara na Manticore. Mbinu rasmi ya uthibitishaji, ambayo hutafsiri kila njia ya utekelezaji kuwa fomula ya kihisabati, ambayo juu yake vikwazo vinaweza kukaguliwa.

Kila mbinu ina faida na hasara, na itakuwa na manufaa katika kesi maalum:

• ikiwa njia zote zimechunguzwa bila muda kuisha

Slither huchanganua mikataba ndani ya sekunde, hata hivyo, uchanganuzi tuli unaweza kusababisha kengele za uongo na hautafaa sana kwa ukaguzi changamano (k.m., ukaguzi wa kihisabati). Tumia Slither kupitia API kwa ufikiaji wa kubofya kitufe kwa vigunduzi vilivyojengewa ndani au kupitia API kwa ukaguzi uliobainishwa na mtumiaji.

Echidna inahitaji kufanya kazi kwa dakika kadhaa na itatoa matokeo chanya ya kweli pekee. Echidna hukagua sifa za usalama zinazotolewa na mtumiaji, zilizoandikwa katika Solidity. Inaweza kukosa hitilafu kwani inategemea uchunguzi nasibu.

Manticore hufanya uchanganuzi wa "uzito mzito zaidi". Kama Echidna, Manticore inathibitisha sifa zinazotolewa na mtumiaji. Itahitaji muda zaidi kufanya kazi, lakini inaweza kuthibitisha uhalali wa sifa na haitatoa ripoti za kengele za uongo.

Mtiririko wa kazi unaopendekezwa

Anza na vigunduzi vilivyojengewa ndani vya Slither ili kuhakikisha kuwa hakuna hitilafu rahisi zilizopo sasa au zitakazoletwa baadaye. Tumia Slither kukagua sifa zinazohusiana na urithi, utegemezi wa vigeu, na masuala ya kimuundo. Msimbo unavyokua, tumia Echidna kupima sifa changamano zaidi za mashine ya hali. Rejelea Slither ili kuunda ukaguzi maalum kwa ajili ya ulinzi usioupata kutoka kwa Solidity, kama vile kulinda dhidi ya kazi kubatilishwa. Mwishowe, tumia Manticore kufanya uthibitishaji unaolengwa wa sifa muhimu za usalama, k.m., shughuli za kihisabati.

• Tumia CLI ya Slither kugundua masuala ya kawaida
• Tumia Echidna kupima sifa za usalama za kiwango cha juu za mkataba wako
• Tumia Slither kuandika ukaguzi maalum tuli
• Tumia Manticore mara tu unapotaka uhakikisho wa kina wa sifa muhimu za usalama

Dokezo kuhusu majaribio ya kitengo. Majaribio ya kitengo ni muhimu ili kuunda programu ya ubora wa juu. Hata hivyo, mbinu hizi hazifai zaidi kupata dosari za usalama. Kwa kawaida hutumika kupima tabia chanya za msimbo (yaani, msimbo hufanya kazi kama inavyotarajiwa katika muktadha wa kawaida), huku dosari za usalama zikielekea kukaa katika hali za pembeni ambazo wasanidi programu hawakuzizingatia. Katika utafiti wetu wa hakiki nyingi za usalama za mkataba-erevu, ufikiaji wa majaribio ya kitengo haukuwa na athari kwa idadi au ukali wa dosari za usalama (opens in a new tab) tulizopata katika msimbo wa wateja wetu.

Kubainisha Sifa za Usalama

Ili kupima na kuthibitisha msimbo wako kwa ufanisi, ni lazima utambue maeneo yanayohitaji uangalizi. Kwa kuwa rasilimali zako zinazotumika kwenye usalama ni chache, kupanga sehemu dhaifu au zenye thamani ya juu za msimbo wako ni muhimu ili kuboresha juhudi zako. Uundaji wa vitisho unaweza kusaidia. Fikiria kukagua:

• Tathmini za Haraka za Hatari (opens in a new tab) (mbinu tunayopendelea wakati ni mfupi)
• Mwongozo wa Uundaji wa Vitisho vya Mfumo Unaozingatia Data (opens in a new tab) (pia inajulikana kama NIST 800-154)
• Uundaji wa vitisho wa Shostack (opens in a new tab)
• STRIDE (opens in a new tab) / DREAD (opens in a new tab)
• PASTA (opens in a new tab)
• Matumizi ya Madai (opens in a new tab)

Vipengele

Kujua unachotaka kukagua pia kutakusaidia kuchagua zana sahihi.

Maeneo mapana ambayo mara nyingi yanafaa kwa mikataba-erevu ni pamoja na:

• Mashine ya hali. Mikataba mingi inaweza kuwakilishwa kama mashine ya hali. Fikiria kukagua kuwa (1) Hakuna hali batili inayoweza kufikiwa, (2) ikiwa hali ni halali inaweza kufikiwa, na (3) hakuna hali inayotega mkataba.

  • Echidna na Manticore ndizo zana za kupendelea kupima vipimo vya mashine ya hali.

• Vidhibiti vya ufikiaji. Ikiwa mfumo wako una watumiaji waliopewa fursa (k.m., mmiliki, vidhibiti, ...) lazima uhakikishe kwamba (1) kila mtumiaji anaweza tu kutekeleza vitendo vilivyoidhinishwa na (2) hakuna mtumiaji anayeweza kuzuia vitendo kutoka kwa mtumiaji aliye na fursa zaidi.

  • Slither, Echidna na Manticore zinaweza kuangalia vidhibiti sahihi vya ufikiaji. Kwa mfano, Slither inaweza kuangalia kuwa kazi zilizoidhinishwa tu ndizo zinazokosa kirekebishaji cha onlyOwner. Echidna na Manticore ni muhimu kwa udhibiti changamano zaidi wa ufikiaji, kama vile ruhusa inayotolewa tu ikiwa mkataba utafikia hali fulani.

• Shughuli za kihisabati. Kuangalia usahihi wa shughuli za kihisabati ni muhimu sana. Kutumia SafeMath kila mahali ni hatua nzuri ya kuzuia kufurika/kupungua (overflow/underflow), hata hivyo, bado lazima uzingatie dosari zingine za kihisabati, ikiwa ni pamoja na masuala ya kuzungusha na dosari zinazotega mkataba.

  • Manticore ndiyo chaguo bora zaidi hapa. Echidna inaweza kutumika ikiwa hesabu iko nje ya wigo wa SMT solver.

• Usahihi wa urithi. Mikataba ya Solidity inategemea sana urithi mwingi. Makosa kama vile kazi ya kufunika inayokosa mwito wa super na mpangilio wa uunganishaji wa c3 uliotafsiriwa vibaya unaweza kuletwa kwa urahisi.

  • Slither ndiyo zana ya kuhakikisha ugunduzi wa masuala haya.

• Mwingiliano wa nje. Mikataba huingiliana, na baadhi ya mikataba ya nje haipaswi kuaminiwa. Kwa mfano, ikiwa mkataba wako unategemea oracles za nje, je, utabaki salama ikiwa nusu ya oracles zinazopatikana zitahujumiwa?

  • Manticore na Echidna ndio chaguo bora zaidi kwa kupima mwingiliano wa nje na mikataba yako. Manticore ina utaratibu uliojengewa ndani wa kuweka vibadala vya mikataba ya nje.

• Upatanifu wa viwango. Viwango vya Ethereum (k.m., ERC20) vina historia ya dosari katika muundo wao. Fahamu mapungufu ya kiwango unachojengea.

  • Slither, Echidna, na Manticore zitakusaidia kugundua mkengeuko kutoka kwa kiwango fulani.

Karatasi ya kudokezea ya uteuzi wa zana

Maeneo mengine yatahitaji kukaguliwa kulingana na malengo yako, lakini maeneo haya mapana ya kuzingatia ni mwanzo mzuri kwa mfumo wowote wa mkataba-erevu.

Ukaguzi wetu wa umma una mifano ya sifa zilizothibitishwa au zilizopimwa. Fikiria kusoma sehemu za Upimaji na Uthibitishaji wa Kiotomatiki za ripoti zifuatazo ili kukagua sifa halisi za usalama:

• 0x (opens in a new tab)
• Balancer (opens in a new tab)

Ukurasa ulihaririwa mwisho: 22 Oktoba 2025

p (opens in a new tab)

m (opens in a new tab)

c (opens in a new tab)

+9

Ona wachangiaji