Security & testing

K Semantics of the Ethereum Virtual Machine (EVM)

Formal verification

பாதுகாப்பு · கல்வி · பகுப்பாய்வு · முறைசார் சரிபார்ப்பு · குறியீட்டுச் செயலாக்கம் · பிழைத்திருத்தக் கருவிகள் · இயக்கநேர சரிபார்ப்பு · Vyper

சமூகம்runtimeverification/evm-semantics(586 ☆)

KEVM என்பது EVM-இன் K-framework செயல்படுத்தக்கூடிய சொற்பொருளியல் (executable semantics) ஆகும்: உங்களுக்கு இணக்கத்தன்மை சரிபார்க்கப்பட்ட செயலாக்கம், குறியீட்டு ஆய்வு, எரிவாயு பகுப்பாய்வு அல்லது எத்திரியத்தின் விதிகளை நெருக்கமாகப் பின்பற்றும் சான்றுகள் தேவைப்படும்போது, பைட் குறியீட்டில் இதைப் பயன்படுத்துங்கள்.

Related resources

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol ஆனது Foundry பண்புச் சோதனைகளை KEVM-ஆதரவுடைய சான்றுகளாக மாற்றுகிறது, இதனால் வெறும் KEVM-ஐ மட்டும் பயன்படுத்துவதை விட குறைவான கையால் எழுதப்பட்ட விவரக்குறிப்பு வேலைகளுடன் முறைசார் உத்தரவாதங்களை நீங்கள் பெற முடியும்.

hax

hax என்பது Rust-இன் பெரிய துணைக்குழுவை F* அல்லது Rocq போன்ற முறையான மொழிகளில் (formal languages) உயர்-உத்தரவாத மொழிபெயர்ப்புகளுக்கான கருவியாகும்.

Act

Act என்பது எத்திரியத்தின் அறிவிப்பு விவரக்குறிப்பு மொழி மற்றும் கருவித்தொகுப்பாகும். இது ஒரு EVM நிரலின் அனைத்து நடத்தைகளையும் விவரிக்கப் பயன்படுகிறது, இதன் மூலம் SMT தீர்ப்பிகள், தேற்ற நிரூபிகள் அல்லது பொருளாதாரப் பகுப்பாய்வுக் கருவிகள், நடைமுறைச் செயலாக்கங்களுக்கு எதிரான தானியங்கி சுத்திகரிப்பு சான்றுகள் உட்பட, பைட் குறியீடு-நிலை சரியான தன்மை மற்றும் ஊக்கத்தொகை இணக்கத்தன்மை குறித்து பகுப்பாய்வு செய்ய முடியும்.

Verifereum

தானியங்கு SMT அணுகுமுறைகள் போதுமானதாக இல்லாதபோது, மிக வலுவான சரியான தன்மைக்கான உறுதிப்பாடுகளை நீங்கள் இலக்காகக் கொள்ளும் வகையில், Verifereum எத்திரியம் திறன் ஒப்பந்தங்களை HOL4-ஆதரவுடைய தேற்றம் நிரூபித்தலுடன் இணைக்கிறது.