Jinsi ya kutumia Echidna kujaribu mikataba-erevu

Usakinishaji

Echidna inaweza kusakinishwa kupitia docker au kutumia binary iliyokusanywa awali.

Echidna 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/training

Binary

https://github.com/crytic/echidna/releases/tag/v1.4.0.0 (opens in a new tab)

Utangulizi wa fuzzing kulingana na sifa

Echidna ni fuzzer kulingana na sifa, tulielezea katika machapisho yetu ya awali ya blogu (1 (opens in a new tab), 2 (opens in a new tab), 3 (opens in a new tab)).

Fuzzing

Fuzzing (opens in a new tab) ni mbinu inayojulikana sana katika jumuiya ya usalama. Inajumuisha kuzalisha pembejeo ambazo ni nasibu kiasi ili kupata hitilafu katika programu. Fuzzers za programu za jadi (kama vile AFL (opens in a new tab) au LibFuzzer (opens in a new tab)) zinajulikana kuwa zana bora za kupata hitilafu.

Zaidi ya uzalishaji wa pembejeo nasibu kabisa, kuna mbinu na mikakati mingi ya kuzalisha pembejeo nzuri, ikiwemo:

• Pata maoni kutoka kwa kila utekelezaji na uelekeze uzalishaji kwa kutumia maoni hayo. Kwa mfano, ikiwa pembejeo mpya iliyozalishwa itasababisha ugunduzi wa njia mpya, inaweza kuwa na maana kuzalisha pembejeo mpya zilizo karibu nayo.
• Kuzalisha pembejeo inayoheshimu kizuizi cha kimuundo. Kwa mfano, ikiwa pembejeo yako ina kichwa chenye checksum, itakuwa na maana kuiruhusu fuzzer kuzalisha pembejeo inayohakiki checksum.
• Kutumia pembejeo zinazojulikana kuzalisha pembejeo mpya: ikiwa una uwezo wa kufikia seti kubwa ya data ya pembejeo halali, fuzzer yako inaweza kuzalisha pembejeo mpya kutoka humo, badala ya kuanza uzalishaji wake kutoka mwanzo. Hizi kwa kawaida huitwa mbegu.

Fuzzing kulingana na sifa

Echidna ni ya familia maalum ya fuzzer: fuzzing kulingana na sifa iliyohamasishwa sana na QuickCheck (opens in a new tab). Tofauti na fuzzer za kawaida ambazo zitajaribu kupata kuharibika, Echidna itajaribu kuvunja visivyobadilika vilivyobainishwa na mtumiaji.

Katika mikataba-erevu, visivyobadilika ni chaguo za kukokotoa za Solidity, ambazo zinaweza kuwakilisha hali yoyote isiyo sahihi au batili ambayo mkataba unaweza kufikia, ikiwa ni pamoja na:

• Udhibiti usio sahihi wa ufikiaji: mshambulizi alikua mmiliki wa mkataba.
• Mashine ya hali isiyo sahihi: tokeni zinaweza kuhamishwa wakati mkataba umesitishwa.
• Hesabu isiyo sahihi: mtumiaji anaweza kufanya 'underflow' salio lake na kupata tokeni za bure zisizo na kikomo.

Kujaribu sifa na Echidna

Tutaona jinsi ya kujaribu mkataba-erevu na Echidna. Lengo ni mkataba-erevu ufuatao token.sol (opens in a new tab):

1contract Token{
2  mapping(address => uint) public balances;
3  function airdrop() public{
4      balances[msg.sender] = 1000;
5  }
6  function consume() public{
7      require(balances[msg.sender]>0);
8      balances[msg.sender] -= 1;
9  }
10  function backdoor() public{
11      balances[msg.sender] += 1;
12  }
13}
Onyesha yote
Nakala

Tutafanya dhana kwamba tokeni hii lazima iwe na sifa zifuatazo:

• Mtu yeyote anaweza kuwa na kiwango cha juu cha tokeni 1000
• Tokeni haiwezi kuhamishwa (sio tokeni ya ERC20)

Andika sifa

Sifa za Echidna ni chaguo za kukokotoa za Solidity. Sifa lazima:

• Haina kigezo
• Rejesha true ikiwa imefanikiwa
• Jina lake kuanza na echidna

Echidna ita:

• Zalisha kiotomatiki miamala isiyo ya kawaida ili kujaribu sifa.
• Ripoti miamala yoyote inayoongoza sifa kurejesha false au kutupa hitilafu.
• Puuza athari za kando wakati wa kuita sifa (yaani, ikiwa sifa inabadilisha kigezo cha hali, inapotea baada ya jaribio)

Sifa ifuatayo hukagua kwamba mhusika hana zaidi ya tokeni 1000:

1function echidna_balance_under_1000() public view returns(bool){
2      return balances[msg.sender] <= 1000;
3}
Nakala

Tumia urithi kutenganisha mkataba wako na sifa zako:

1contract TestToken is Token{
2      function echidna_balance_under_1000() public view returns(bool){
3            return balances[msg.sender] <= 1000;
4      }
5  }
Nakala

token.sol (opens in a new tab) inatekeleza sifa na kurithi kutoka kwa tokeni.

Anzisha mkataba

Echidna inahitaji kiunda bila kigezo. Ikiwa mkataba wako unahitaji uanzishaji maalum, unahitaji kuufanya katika kiunda.

Kuna anwani maalum katika Echidna:

• 0x00a329c0648769A73afAc7F9381E08FB43dBEA72 ambayo huita kiunda.
• 0x10000, 0x20000, na 0x00a329C0648769a73afAC7F9381e08fb43DBEA70 ambazo huita kiholela chaguo za kukokotoa zingine.

Hatuhitaji uanzishaji wowote maalum katika mfano wetu wa sasa, kwa hivyo kiunda chetu hakina kitu.

Endesha Echidna

Echidna inazinduliwa na:

echidna-test contract.sol

Ikiwa contract.sol ina mikataba mingi, unaweza kubainisha lengo:

echidna-test contract.sol --contract MyContract

Muhtasari: Kujaribu sifa

Yafuatayo ni muhtasari wa uendeshaji wa echidna kwenye mfano wetu:

1contract TestToken is Token{
2    constructor() public {}
3        function echidna_balance_under_1000() public view returns(bool){
4          return balances[msg.sender] <= 1000;
5        }
6  }
Nakala

echidna-test testtoken.sol --contract TestToken
...
echidna_balance_under_1000: failed!💥
  Call sequence, shrinking (1205/5000):
    airdrop()
    backdoor()
...
Onyesha yote

Echidna iligundua kuwa sifa inakiukwa ikiwa backdoor itaitwa.

Kuchuja chaguo za kukokotoa za kuita wakati wa kampeni ya fuzzing

Tutaona jinsi ya kuchuja chaguo za kukokotoa za kufanyiwa 'fuzz'. Lengo ni mkataba-erevu ufuatao:

1contract C {
2  bool state1 = false;
3  bool state2 = false;
4  bool state3 = false;
5  bool state4 = false;
6
7  function f(uint x) public {
8    require(x == 12);
9    state1 = true;
10  }
11
12  function g(uint x) public {
13    require(state1);
14    require(x == 8);
15    state2 = true;
16  }
17
18  function h(uint x) public {
19    require(state2);
20    require(x == 42);
21    state3 = true;
22  }
23
24 function i() public {
25    require(state3);
26    state4 = true;
27  }
28
29  function reset1() public {
30    state1 = false;
31    state2 = false;
32    state3 = false;
33    return;
34  }
35
36  function reset2() public {
37    state1 = false;
38    state2 = false;
39    state3 = false;
40    return;
41  }
42
43  function echidna_state4() public returns (bool) {
44    return (!state4);
45  }
46}
Onyesha yote
Nakala

Mfano huu mdogo unalazimisha Echidna kupata mfuatano fulani wa miamala ili kubadilisha kigezo cha hali. Hii ni ngumu kwa fuzzer (inapendekezwa kutumia zana ya utekelezaji wa ishara kama Manticore (opens in a new tab)). Tunaweza kuendesha Echidna ili kuthibitisha hili:

echidna-test multi.sol
...
echidna_state4: passed! 🎉
Seed: -3684648582249875403

Kuchuja chaguo za kukokotoa

Echidna ina shida kupata mfuatano sahihi wa kujaribu mkataba huu kwa sababu chaguo mbili za kukokotoa za kuweka upya (reset1 na reset2) zitaweka vigezo vyote vya hali kuwa false. Hata hivyo, tunaweza kutumia kipengele maalum cha Echidna ama kuweka kwenye orodha nyeusi chaguo za kukokotoa za kuweka upya au kuweka kwenye orodha nyeupe tu chaguo za kukokotoa za f, g, h na i.

Ili kuweka kwenye orodha nyeusi chaguo za kukokotoa, tunaweza kutumia faili hii ya usanidi:

1filterBlacklist: true
2filterFunctions: ["reset1", "reset2"]

Njia nyingine ya kuchuja chaguo za kukokotoa ni kuorodhesha chaguo za kukokotoa zilizoidhinishwa. Ili kufanya hivyo, tunaweza kutumia faili hii ya usanidi:

1filterBlacklist: false
2filterFunctions: ["f", "g", "h", "i"]

• filterBlacklist ni true kwa chaguo-msingi.
• Kuchuja kutafanywa kwa jina tu (bila vigezo). Ikiwa una f() na f(uint256), kichujio cha "f" kitafanana na chaguo zote mbili za kukokotoa.

Endesha Echidna

Ili kuendesha Echidna na faili ya usanidi blacklist.yaml:

echidna-test multi.sol --config blacklist.yaml
...
echidna_state4: failed!💥
  Call sequence:
    f(12)
    g(8)
    h(42)
    i()

Echidna itapata mfuatano wa miamala ya kukanusha sifa karibu mara moja.

Muhtasari: Kuchuja chaguo za kukokotoa

Echidna inaweza kuweka kwenye orodha nyeusi au orodha nyeupe chaguo za kukokotoa za kuita wakati wa kampeni ya fuzzing kwa kutumia:

1filterBlacklist: true
2filterFunctions: ["f1", "f2", "f3"]

echidna-test contract.sol --config config.yaml
...

Echidna huanza kampeni ya fuzzing ama kwa kuweka kwenye orodha nyeusi f1, f2 na f3 au kwa kuita hizi pekee, kulingana na thamani ya boolean ya filterBlacklist.

Jinsi ya kujaribu assert ya Solidity na Echidna

Katika mafunzo haya mafupi, tutaonyesha jinsi ya kutumia Echidna kujaribu ukaguzi wa dai katika mikataba. Tuseme tuna mkataba kama huu:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    // tmp <= counter
8    return (counter - tmp);
9  }
10}
Onyesha yote
Nakala

Andika dai

Tunataka kuhakikisha kuwa tmp ni ndogo au sawa na counter baada ya kurudisha tofauti yake. Tunaweza kuandika sifa ya Echidna, lakini tutahitaji kuhifadhi thamani ya tmp mahali fulani. Badala yake, tunaweza kutumia dai kama hili:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Onyesha yote
Nakala

Endesha Echidna

Ili kuwezesha upimaji wa kutofaulu kwa dai, tengeneza faili ya usanidi wa Echidna (opens in a new tab) config.yaml:

1checkAsserts: true

Tunapoendesha mkataba huu katika Echidna, tunapata matokeo yanayotarajiwa:

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(217110167319967866419195559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Onyesha yote

Kama unavyoona, Echidna inaripoti kushindwa kwa dai fulani katika chaguo la kukokotoa la inc. Kuongeza zaidi ya dai moja kwa kila chaguo la kukokotoa kunawezekana, lakini Echidna haiwezi kusema ni dai gani lililoshindwa.

Wakati gani na jinsi gani ya kutumia madai

Madai yanaweza kutumika kama njia mbadala ya sifa dhahiri, haswa ikiwa masharti ya kukagua yanahusiana moja kwa moja na matumizi sahihi ya operesheni fulani f. Kuongeza madai baada ya msimbo fulani kutalazimisha ukaguzi ufanyike mara tu baada ya kutekelezwa:

1function f(..) public {
2    // msimbo fulani tata
3    ...
4    assert (condition);
5    ...
6}
7
Nakala

Kinyume chake, kutumia sifa ya wazi ya echidna kutatekeleza miamala kwa nasibu na hakuna njia rahisi ya kulazimisha ni lini hasa itakaguliwa. Bado inawezekana kufanya njia hii mbadala:

1function echidna_assert_after_f() public returns (bool) {
2    f(..);
3    return(condition);
4}
Nakala

Hata hivyo, kuna baadhi ya masuala:

• Inashindwa ikiwa f imetangazwa kama internal au external.
• Haijulikani ni vigezo vipi vinapaswa kutumika kuita f.
• Ikiwa f inabatilika, sifa itashindwa.

Kwa ujumla, tunapendekeza kufuata pendekezo la John Regehr (opens in a new tab) kuhusu jinsi ya kutumia madai:

• Usilazimishe athari yoyote ya kando wakati wa ukaguzi wa dai. Kwa mfano: assert(ChangeStateAndReturn() == 1)
• Usidai kauli zilizo wazi. Kwa mfano assert(var >= 0) ambapo var imetangazwa kama uint.

Mwisho, tafadhali usitumie require badala ya assert, kwani Echidna haitaweza kuitambua (lakini mkataba utabatilika hata hivyo).

Muhtasari: Ukaguzi wa Madai

Yafuatayo ni muhtasari wa uendeshaji wa echidna kwenye mfano wetu:

1contract Incrementor {
2  uint private counter = 2**200;
3
4  function inc(uint val) public returns (uint){
5    uint tmp = counter;
6    counter += val;
7    assert (tmp <= counter);
8    return (counter - tmp);
9  }
10}
Onyesha yote
Nakala

echidna-test assert.sol --config config.yaml
Analyzing contract: assert.sol:Incrementor
assertion in inc: failed!💥
  Call sequence, shrinking (2596/5000):
    inc(217110167319967866419195559689128982722488122124807605757398297001483711807488)
    inc(7237005577332262213973186563042994240829374041602535252466099000494570602496)
    inc(86844066927987146567678238756515930889952488499230423029593188005934847229952)
Seed: 1806480648350826486
Onyesha yote

Echidna iligundua kuwa dai katika inc linaweza kushindwa ikiwa chaguo hili la kukokotoa litaitwa mara nyingi na vigezo vikubwa.

Kukusanya na kurekebisha mkusanyiko wa Echidna

Tutaona jinsi ya kukusanya na kutumia mkusanyiko wa miamala na Echidna. Lengo ni mkataba-erevu ufuatao magic.sol (opens in a new tab):

1contract C {
2  bool value_found = false;
3  function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public {
4    require(magic_1 == 42);
5    require(magic_2 == 129);
6    require(magic_3 == magic_4+333);
7    value_found = true;
8    return;
9  }
10
11  function echidna_magic_values() public returns (bool) {
12    return !value_found;
13  }
14
15}
Onyesha yote
Nakala

Mfano huu mdogo unalazimisha Echidna kupata thamani fulani ili kubadilisha kigezo cha hali. Hii ni ngumu kwa fuzzer (inapendekezwa kutumia zana ya utekelezaji wa ishara kama Manticore (opens in a new tab)). Tunaweza kuendesha Echidna ili kuthibitisha hili:

echidna-test magic.sol
...
echidna_magic_values: passed! 🎉
Seed: 2221503356319272685

Hata hivyo, bado tunaweza kutumia Echidna kukusanya mkusanyiko tunapoendesha kampeni hii ya 'fuzzing'.

Kukusanya mkusanyiko

Ili kuwezesha ukusanyaji wa mkusanyiko, tengeneza saraka ya mkusanyiko:

mkdir corpus-magic

Na faili ya usanidi wa Echidna (opens in a new tab) config.yaml:

1coverage: true
2corpusDir: "corpus-magic"

Sasa tunaweza kuendesha zana yetu na kuangalia mkusanyiko uliokusanywa:

echidna-test magic.sol --config config.yaml

Echidna bado haiwezi kupata thamani sahihi za 'uchawi', lakini tunaweza kuangalia mkusanyiko iliokusanya. Kwa mfano, moja ya faili hizi ilikuwa:

1[
2  {
3    "_gas'": "0xffffffff",
4    "_delay": ["0x13647", "0xccf6"],
5    "_src": "00a329c0648769a73afac7f9381e08fb43dbea70",
6    "_dst": "00a329c0648769a73afac7f9381e08fb43dbea72",
7    "_value": "0x0",
8    "_call": {
9      "tag": "SolCall",
10      "contents": [
11        "magic",
12        [
13          {
14            "contents": [
15              256,
16              "93723985220345906694500679277863898678726808528711107336895287282192244575836"
17            ],
18            "tag": "AbiUInt"
19          },
20          {
21            "contents": [256, "334"],
22            "tag": "AbiUInt"
23          },
24          {
25            "contents": [
26              256,
27              "68093943901352437066264791224433559271778087297543421781073458233697135179558"
28            ],
29            "tag": "AbiUInt"
30          },
31          {
32            "tag": "AbiUInt",
33            "contents": [256, "332"]
34          }
35        ]
36      ]
37    },
38    "_gasprice'": "0xa904461f1"
39  }
40]
Onyesha yote
Nakala

Ni wazi, pembejeo hii haitasababisha kutofaulu kwa sifa yetu. Hata hivyo, katika hatua inayofuata, tutaona jinsi ya kuirekebisha kwa ajili hiyo.

Kupanda mbegu kwenye mkusanyiko

Echidna inahitaji msaada ili kushughulikia chaguo la kukokotoa la magic. Tutakili na kurekebisha pembejeo ili kutumia vigezo vinavyofaa kwake:

cp corpus/2712688662897926208.txt corpus/new.txt

Tutarekebisha new.txt ili iite magic(42,129,333,0). Sasa, tunaweza kuendesha Echidna tena:

echidna-test magic.sol --config config.yaml
...
echidna_magic_values: failed!💥
  Call sequence:
    magic(42,129,333,0)
Unique instructions: 142
Unique codehashes: 1
Seed: -7293830866560616537
Onyesha yote

Wakati huu, iligundua kuwa sifa inakiukwa mara moja.

Kupata miamala yenye matumizi makubwa ya Gesi

Tutaona jinsi ya kupata miamala yenye matumizi makubwa ya Gesi na Echidna. Lengo ni mkataba-erevu ufuatao:

1contract C {
2  uint state;
3
4  function expensive(uint8 times) internal {
5    for(uint8 i=0; i < times; i++)
6      state = state + i;
7  }
8
9  function f(uint x, uint y, uint8 times) public {
10    if (x == 42 && y == 123)
11      expensive(times);
12    else
13      state = 0;
14  }
15
16  function echidna_test() public returns (bool) {
17    return true;
18  }
19
20}
Onyesha yote
Nakala

Hapa expensive inaweza kuwa na matumizi makubwa ya Gesi.

Hivi sasa, Echidna daima inahitaji mali ya kujaribu: hapa echidna_test daima inarudi true. Tunaweza kuendesha Echidna ili kuthibitisha hili:

1echidna-test gas.sol
2...
3echidna_test: passed! 🎉
4
5Seed: 2320549945714142710

Kupima Matumizi ya Gesi

Ili kuwezesha matumizi ya Gesi na Echidna, tengeneza faili ya usanidi config.yaml:

1estimateGas: true

Katika mfano huu, tutapunguza pia ukubwa wa mfuatano wa manunuzi ili kufanya matokeo yawe rahisi kueleweka:

1seqLen: 2
2estimateGas: true

Endesha Echidna

Mara tu tunapokuwa na faili ya usanidi iliyoundwa, tunaweza kuendesha Echidna kama hii:

echidna-test gas.sol --config config.yaml
...
echidna_test: passed! 🎉
f used a maximum of 1333608 gas
  Call sequence:
    f(42,123,249) Gas price: 0x10d5733f0a Time delay: 0x495e5 Block delay: 0x88b2
Unique instructions: 157
Unique codehashes: 1
Seed: -325611019680165325
Onyesha yote

• Gesi inayoonyeshwa ni makadirio yaliyotolewa na HEVM (opens in a new tab).

Kuchuja Simu zinazopunguza Gesi

Mafunzo kuhusu kuchuja chaguo za kukokotoa za kuita wakati wa kampeni ya fuzzing hapo juu yanaonyesha jinsi ya kuondoa baadhi ya chaguo za kukokotoa kutoka kwa majaribio yako.
Hii inaweza kuwa muhimu kwa kupata makadirio sahihi ya Gesi. Fikiria mfano ufuatao:

1contract C {
2  address [] addrs;
3  function push(address a) public {
4    addrs.push(a);
5  }
6  function pop() public {
7    addrs.pop();
8  }
9  function clear() public{
10    addrs.length = 0;
11  }
12  function check() public{
13    for(uint256 i = 0; i < addrs.length; i++)
14      for(uint256 j = i+1; j < addrs.length; j++)
15        if (addrs[i] == addrs[j])
16          addrs[j] = address(0x0);
17  }
18  function echidna_test() public returns (bool) {
19      return true;
20  }
21}
Onyesha yote
Nakala

Ikiwa Echidna inaweza kuita chaguo zote za kukokotoa, haitapata kwa urahisi miamala yenye gharama kubwa ya Gesi:

1echidna-test pushpop.sol --config config.yaml
2...
3pop used a maximum of 10746 gas
4...
5check used a maximum of 23730 gas
6...
7clear used a maximum of 35916 gas
8...
9push used a maximum of 40839 gas
Onyesha yote

Hiyo ni kwa sababu gharama inategemea ukubwa wa addrs na simu za nasibu huelekea kuacha safu karibu tupu. Kuorodhesha pop na clear nyeusi, hata hivyo, hutupa matokeo bora zaidi:

1filterBlacklist: true
2filterFunctions: ["pop", "clear"]

1echidna-test pushpop.sol --config config.yaml
2...
3push used a maximum of 40839 gas
4...
5check used a maximum of 1484472 gas

Muhtasari: Kupata miamala yenye matumizi makubwa ya Gesi

Echidna inaweza kupata miamala yenye matumizi makubwa ya Gesi kwa kutumia chaguo la usanidi la estimateGas:

1estimateGas: true

echidna-test contract.sol --config config.yaml
...

Echidna itaripoti mfuatano wenye matumizi ya juu zaidi ya Gesi kwa kila chaguo la kukokotoa, mara tu kampeni ya fuzzing itakapokamilika.

Ukurasa ulihaririwa mwisho: 21 Oktoba 2025

p (opens in a new tab)

p (opens in a new tab)

n (opens in a new tab)

+8

Ona wachangiaji