Usalama na majaribio

CodeTracer ni kitatuzi rafiki kwa mtumiaji cha kusafiri kwa wakati kilichoundwa kusaidia anuwai ya lugha za programu za Web3.

Simbolik ni kitatuzi chenye nguvu cha Solidity kinachochanganya utatuzi wa jadi wa sehemu ya kukatiza na utekelezaji wa kiishara, kuwezesha wasanidi programu kuchunguza kila njia inayowezekana ya utekelezaji na kufichua udhaifu kwa usahihi. Inapatikana kama kiendelezi cha VSCode, Simbolik inaunganishwa bila mshono kwenye mtiririko wa kazi uliopo, ikitoa utatuzi wa mtindo wa sehemu ya kukatiza, ukaguzi wa kiwango cha Solidity na EVM, na uwezo wa uthibitishaji rasmi.

Kitatuzi na kiigaji cha muamala kinachotegemea wavuti kwa EVM. Chanzo wazi na kinachoweza kupangishwa kibinafsi. Kagua hali za kigezo katika kila hatua, iga miamala kabla ya kusambaza, na uweke wasifu wa matumizi ya gesi. Inasaidia mtoa huduma yeyote wa RPC.

Abi Ninja ni kiolesura cha mtumiaji (UI) cha kivinjari kwa ajili ya kuita mikataba yenye ABI zinazojulikana, ABI zilizobandikwa, au msimbo wa baiti uliotenganishwa, na usomaji unaotambua proksi kwenye mitandao mingi ikijumuisha nodi yako ya Hardhat au Anvil inayoendeshwa ndani ya nchi.

zana rahisi ya cli ya kupakia msimbo wa mkataba kwenye IDE yako papo hapo.

Ganda la mwingiliano rahisi sana kwa kuingiliana na mikataba mahiri

viem-tracer inaboresha mteja wa Viem ili miito iliyoshindwa ya ethestimateGas na ethsendTransaction ijumuishe kiotomatiki matokeo ya ufuatiliaji yanayosomeka na binadamu yaliyosimbuliwa na sourcify.dev, na inaongeza wasaidizi waliochapishwa karibu na debug_traceCall ili wasanidi programu waweze kukagua utekelezaji bila kuondoka kwenye mrundikano wao uliopo wa RPC.

EDB ni kitatuzi cha kiwango cha chanzo kwa utekelezaji wa Solidity na hatua, za ndani, saa, na vituo vya mapumziko unapohitaji mwonekano wa kiwango cha IDE katika tabia ya mkataba mnyororoni au katika majaribio.

forge-stack-tracer hupitisha matokeo ya majaribio ya Foundry yenye maneno mengi kupitia usimbuzi wa Swiss-Knife ili majaribio yanayoshindwa yarudishe ufuatiliaji wa mrundikano mwingiliano badala ya heksadesimali isiyo wazi.

Chimera ni mfumo wa kuandika majaribio ya Solidity katika Foundry na kuweza kuyatumia tena na Zana zingine za Chanzo Wazi kama vile Echidna, Medusa, Halmos na Kontrol

Slither ni injini ya uchanganuzi tuli ya Python ya Trail of Bits kwa Solidity na Vyper: iendeshe katika CI ili kuwasha vigunduzi, kuchapisha mionekano ya kimuundo ya mikataba, au kuandika hati za ukaguzi maalum kwenye misingi yote ya msimbo.

Synpress inaweka Playwright na otomatiki ya kivinjari inayotambua Ethereum ili uweze kujaribu programu tumizi zilizogatuliwa (dapps) kutoka mwanzo hadi mwisho, ikijumuisha madirisha ibukizi ya mkoba na swichi za mnyororo, katika CI.

Aderyn ni kichanganuzi tuli cha mkataba mahiri wa Solidity cha chanzo wazi, kinachotegemea Rust cha Cyfrin kilichoundwa kusaidia wahandisi wa itifaki na watafiti wa usalama kupata udhaifu katika misingi ya msimbo wa Solidity

Titanoboa ni mkalimani mwingiliano wa Vyper na mfumo wa majaribio kwa mizunguko ya maoni ya haraka unapofanya majaribio na mikataba nje ya mzunguko kamili wa Foundry.

Medusa ni fuzzer ya mkataba mahiri yenye hali iliyohamasishwa na Echidna. Inatoa majaribio ya fuzz yaliyosambamba ya mikataba mahiri na uthibitishaji wa vibadilikaji vya hali ya juu vya mkataba mahiri.

solidity-coverage inatoa ufunikaji wa msimbo wa mkataba mahiri kwa jukwaa la msanidi programu la Hardhat. Ni sahihi sana, inasaidia mkusanyiko kamili wa viaIR wa Solidity na seti kubwa ya mifumo ya tawi la msimbo maalum kwa Solidity. Imesakinishwa kwenye miradi ~230k ya GitHub na inapakuliwa mara ~100k kwa wiki kutoka NPM.

hevm ni injini ya utekelezaji ya EVM ya chanzo wazi, ya kisasa, ya haraka ya kiishara na thabiti inayoweza kupata matatizo katika mikataba mahiri. Kupitia mfumo wake wa utekelezaji na uchanganuzi wa kiishara, hevm inaweza kutekeleza mikataba kiishara, nusu-thabiti, au thabiti ili kupata hitilafu, au kulinganisha mikataba miwili tofauti kwa tofauti, ikifanya ukaguzi wa usawa.

Crytic-Properties ni seti ya majaribio ya usalama yanayoweza kutumika tena kwa baadhi ya viwango vya tokeni vinavyotumiwa sana kama vile ERC-20, ERC-721, ERC-4626, na zaidi.

Wallet Test Framework ni mfumo wa kiotomatiki unaopitia mtiririko wa msingi wa mkoba-uhamishaji, usomaji wa salio, mwingiliano wa kimsingi wa programu tumizi iliyogatuliwa (dapp)-ili timu ziweze kufanya majaribio ya kurudi nyuma ya matarajio ya pamoja ya UX katika CI.

Kizalishaji cha majaribio cha mkataba mahiri kinachotegemea Mbinu ya Mti wa Matawi.

ERCx ni maktaba kamili ya majaribio ya chanzo wazi kwa viwango vya tokeni vya ERC, inayoangazia zaidi ya majaribio 500 ya kibinafsi katika utekelezaji wa ERC-20, ERC-721, ERC-1155, na ERC-4626.

Mkaguzi wa usalama wa mkataba mahiri wa Solidity/EVM mwenye mifumo 104 ya udhaifu na zana 8 za uchanganuzi. Inafikia 100% kwenye vigezo vya CTF na EVMBench (120/120). Uchanganuzi tuli kwa kugundua udhaifu katika mikataba mahiri.

foundry-storage-check ni Kitendo cha GitHub kwa miradi ya Foundry kinachoendeshwa kwenye kila ombi la kuvuta ili kuhakikisha mipangilio ya hifadhi ya proksi inayoweza kuboreshwa inabaki salama dhidi ya mgongano na kwamba nafasi mpya za hifadhi zilizoongezwa zinaanzishwa kwa sifuri mnyororoni kabla ya kuunganishwa kusafirishwa.

blocksmith.js ni kiunganishi chembamba cha JavaScript karibu na forge na anvil kwa ajili ya kuandika hati za majaribio ya Foundry ya minyororo mingi au matukio mengi wakati EVM moja ya ndani haitoshi.

KEVM ni semantiki inayoweza kutekelezwa ya K-framework ya EVM: ielekeze kwenye msimbo wa baiti unapohitaji utekelezaji uliokaguliwa kwa kufuata, uchunguzi wa kiishara, hoja za gesi, au uthibitisho unaofuatilia sheria za Ethereum kwa karibu.

Kontrol inainua majaribio ya mali ya Foundry kuwa uthibitisho unaoungwa mkono na KEVM ili uweze kufuatilia dhamana rasmi kwa kazi ndogo ya vipimo vilivyoandikwa kwa mkono kuliko KEVM ghafi pekee.

hax ni zana ya tafsiri za uhakika wa juu za kitengo kikubwa cha Rust katika lugha rasmi kama vile F* au Rocq.

Act ni lugha ya ubainishaji ya kutangaza ya Ethereum na msururu wa zana kwa ajili ya kuelezea tabia zote za programu ya EVM ili vitatuzi vya SMT, wathibitishaji wa nadharia, au zana za uchanganuzi wa kiuchumi ziweze kufikiri kuhusu usahihi wa kiwango cha msimbo wa baiti na uoanifu wa motisha, ikijumuisha uthibitisho wa uboreshaji wa kiotomatiki dhidi ya utekelezaji halisi.

Verifereum inaunganisha mikataba mahiri ya Ethereum na uthibitishaji wa nadharia unaoungwa mkono na HOL4 ili uweze kulenga madai yenye nguvu sana ya usahihi wakati mbinu za kiotomatiki za SMT hazitoshi.