Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

Usalama · Elimu · Uchanganuzi · Uthibitishaji rasmi · Utekelezaji wa kiishara · Zana za utatuzi · Uthibitishaji wa wakati wa utekelezaji · Vyper

Kijamii runtimeverification/evm-semantics(586 ☆)

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.

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

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

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

Act

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

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.