பாதுகாப்பு, சோதனை & முறைசார் சரிபார்ப்பு

நாங்கள் Runtime Verification, முக்கியமான சிஸ்டம்களின் பாதுகாப்பையும் சரியான தன்மையையும் உறுதி செய்வதற்கான கடுமையான கருவிகளை உருவாக்கும் ஒரு ஆராய்ச்சி மற்றும் மேம்பாட்டு நிறுவனம். எங்கள் குழு KEVM-ஐ உருவாக்கியுள்ளது, இது K Framework-ல் எழுதப்பட்ட Ethereum Virtual Machine (EVM)-இன் மிகவும் முழுமையான மற்றும் போர்க்களத்தில் சோதிக்கப்பட்ட ஃபார்மல் செமாண்டிக்ஸ் ஆகும். KEVM என்பது ஒரு விவரக்குறிப்பு மட்டுமல்ல, இது ஸ்மார்ட் ஒப்பந்தங்களைப் பற்றி சிம்பாலிக் முறையில் பகுத்தறியவும், கன்ஃபார்மன்ஸ் சோதனைகளை இயக்கவும், கேஸ் பயன்பாட்டை பகுப்பாய்வு செய்யவும், நிரல்களை பிழைத்திருத்தம் செய்யவும் மற்றும் சரியான பண்புகளை ஃபார்மல் முறையில் சரிபார்க்கவும் பயன்படுத்தக்கூடிய ஒரு எக்ஸிகியூட்டபிள் விவரக்குறிப்பாகும். இது முழு Ethereum சோதனைத் தொகுப்பையும் கடந்து செல்கிறது மற்றும் Solidity மற்றும் Vyper இரண்டிலும் உள்ள ERC20 டோக்கன்கள் உட்பட அதிக மதிப்புள்ள ஒப்பந்தங்களைச் சரிபார்க்கப் பயன்படுகிறது. Pectra மேம்படுத்தலை ஆதரிக்க சமீபத்தில் செமாண்டிக்ஸைப் புதுப்பித்தோம். KEVM ஆனது Kontrol-ஆல் தீவிரமாகப் பயன்படுத்தப்படுகிறது - இது Soldiity-க்கான எங்கள் ஃபார்மல் வெரிஃபிகேஷன் கருவியாகும், இது Optimism, Ethereum Foundation, Lido, Uniswap உள்ளிட்ட EVM சுற்றுச்சூழல் அமைப்பில் உள்ள முன்னணி குழுக்களாலும், பரந்த Ethereum சமூகம் முழுவதும் உள்ள பாதுகாப்பு ஆராய்ச்சியாளர்கள் மற்றும் தணிக்கையாளர்களாலும் தீவிரமாகப் பயன்படுத்தப்படுகிறது. நாங்கள் இந்த ரெபோசிட்டரியை தீவிரமாகப் பராமரிக்கிறோம், Ethereum-இன் நெறிமுறை பரிணாமத்திற்குப் பங்களிக்கிறோம், மேலும் Foundry போன்ற டெவலப்பர் டூலிங்குடன் ஒருங்கிணைக்கிறோம். KEVM மூலம், நிரூபிக்கக்கூடிய சரியான மற்றும் பாதுகாப்பான ஸ்மார்ட் ஒப்பந்த உள்கட்டமைப்பில் சாத்தியமானவற்றின் எல்லைகளை நாங்கள் விரிவுபடுத்துகிறோம்.

Act என்பது முறையான சரிபார்ப்புக்கான (formal verification) ஸ்மார்ட் ஒப்பந்தக் குறிப்பீடு மொழி (specification language) மற்றும் கருவித்தொகுப்பாகும். Act குறிப்பீடுகள் ஒரு EVM நிரலின் சாத்தியமான அனைத்து நடத்தைகளின் முறையான, உயர்மட்ட விளக்கமாகும். குறிப்பீடு பற்றிய பண்புகளை நிரூபிக்க, ஏற்கனவே உள்ள பல பொது நோக்கச் சரிபார்ப்புக் கருவிகளைப் பயன்படுத்த Act அனுமதிக்கிறது. அத்தகைய கருவிகளில் SMT solvers (cvc5, z3, bitwuzla), theorem provers (Coq) மற்றும் பொருளாதாரப் பகுப்பாய்வுக் கருவிகள் (CheckMate, Open Games) ஆகியவை அடங்கும். Act குறிப்பீடுகள் EVM-இல் உள்ள உறுதியான செயலாக்கங்களுக்குச் சமமானவை எனத் தானாகவே நிரூபிக்கப்படலாம். மிகவும் எளிமையான ஒப்பந்தங்களுக்கு, EVM பைட் குறியீட்டிலிருந்து (bytecode) Act குறிப்பீடுகளைத் தானாகவே உருவாக்க முடியும். இது EVM பைட் குறியீட்டின் உயர்மட்டப் பண்புகள் பற்றிய கொள்கை ரீதியான பகுத்தறிவை ஆதரிக்கும் எண்ட்-டு-எண்ட் பைப்லைனாகும் (end-to-end pipeline). இது சரியான தன்மை (எ.கா. கணக்கியல் மாறிலிகள்) மற்றும் பொருளாதாரப் பண்புகள் (எ.கா. ஊக்கத்தொகை இணக்கத்தன்மை) ஆகிய இரண்டையும் பற்றிய பகுத்தறிவை ஆதரிக்கிறது. Act குறிப்பீடுகள் உயர்மட்ட ஸ்மார்ட் ஒப்பந்தப் பிரதிநிதித்துவமாகச் செயல்படுகின்றன, இது ஏற்கனவே உள்ள பொது நோக்கப் பகுப்பாய்வு மற்றும் சரிபார்ப்புக் கருவிகளை EVM சூழலில் எளிதாக ஒருங்கிணைக்க அனுமதிக்கிறது.

Titanoboa என்பது ஒரு Vyper இன்டர்ப்ரெட்டர் மற்றும் சோதனை ஃபிரேம்வொர்க் ஆகும், இது Vyper ஸ்மார்ட் ஒப்பந்தங்களுக்கு நவீன, ஒருங்கிணைந்த மேம்பாட்டு அனுபவத்தை வழங்குகிறது. இது டெவலப்பர்களை Python-க்குள் நேரடியாக Vyper ஒப்பந்தங்களைச் சோதிக்கவும் பிழைத்திருத்தம் செய்யவும் அனுமதிக்கிறது, அழகான ட்ரேஸ்பேக்குகள், ஃபோர்க்கிங், பிழைத்திருத்த திறன்கள், pytest ஒருங்கிணைப்பு மற்றும் எந்த கூடுதல் அமைப்பும் இல்லாத ஃபஸ்ஸிங் போன்ற அம்சங்களை வழங்குகிறது. அதன் தனித்த திறன்களுக்கு அப்பால், Titanoboa ஆனது Ape மற்றும் Moccasin போன்ற பிற பிரபலமான சோதனை ஃபிரேம்வொர்க்குகளுக்கான அடித்தளமாகச் செயல்படுகிறது, மேலும் இது Vyper சுற்றுச்சூழல் அமைப்பிற்கான உள்கட்டமைப்பின் முக்கிய பகுதியாகும்.