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

நாங்கள் 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 மூலம், நிரூபிக்கக்கூடிய சரியான மற்றும் பாதுகாப்பான ஸ்மார்ட் ஒப்பந்த உள்கட்டமைப்பில் சாத்தியமானவற்றின் எல்லைகளை நாங்கள் விரிவுபடுத்துகிறோம்.

Branching Tree Technique-ஐ அடிப்படையாகக் கொண்ட ஸ்மார்ட் ஒப்பந்தச் சோதனை உருவாக்கி (test generator).

Runtime Verification ஒரு தசாப்தத்திற்கும் மேலாக ஓப்பன் சோர்ஸ் ஃபார்மல் வெரிஃபிகேஷன் கருவிகளில் முன்னணியில் உள்ளது. எங்கள் பொதுவான அணுகுமுறை பல பிளாக்செயின்களில் எங்கள் தொழில்நுட்பத்தைப் பயன்படுத்த அனுமதிக்கிறது. KEVM அனைத்து EVM அடிப்படையிலான ஸ்மார்ட் ஒப்பந்தங்களுக்கும் எங்கள் சரிபார்ப்பு உள்கட்டமைப்பை வழங்கும் அதே வேளையில், Kontrol ஆனது Solidity ஸ்மார்ட் ஒப்பந்தங்களுக்கான ஃபார்மல் வெரிஃபிகேஷனுக்கான நுழைவுத் தடையை வெகுவாகக் குறைக்கிறது. எங்கள் டூலிங் முற்றிலும் ஓப்பன் சோர்ஸ் ஆகும், மேலும் Optimism சுற்றுச்சூழல் அமைப்பின் அனைத்து டெவலப்பர்களுக்கும் கூடுதல் கட்டணமின்றி இலவசமாக அணுகக்கூடியது. KEVM என்பது K framework-ல் எழுதப்பட்ட ஒரு EVM எக்ஸிகியூட்டபிள் ஃபார்மல் செமாண்டிக்ஸ் ஆகும். KEVM அனைத்து Ethereum கன்ஃபார்மன்ஸ் சோதனைகளையும் கடந்து செல்கிறது மற்றும் K framework உடன் ஸ்மார்ட் ஒப்பந்தங்களை ஃபார்மல் முறையில் சரிபார்ப்பதற்கான நுழைவுப் புள்ளியாகும். இருப்பினும், சாதாரண KEVM-ஐப் பயன்படுத்த, விவரக்குறிப்புகளை எழுத K framework-ல் தற்காலிகப் பயிற்சி தேவைப்படுகிறது. கூடுதலாக, இந்த விவரக்குறிப்புகள் மிகவும் விரிவானதாக இருக்கலாம், அவற்றை எழுதுவதில் சிரமத்தை அதிகரிக்கும். டெவலப்பர்கள் தங்கள் ஸ்மார்ட் ஒப்பந்தங்களின் ஃபார்மல் விவரக்குறிப்பை நேரடியாக Foundry பண்புச் சோதனைகளாக எழுத அனுமதிப்பதன் மூலம் Kontrol இதைத் தீர்க்கிறது. இந்தச் சோதனைகள் தானாகவே KEVM விவரக்குறிப்புகளாக மொழிபெயர்க்கப்பட்டு, அனைத்து சரிபார்ப்பு உத்தரவாதங்களையும் வைத்திருக்கும் அதே வேளையில் மிகவும் எளிதான டெவலப்பர் அனுபவத்தை அனுமதிக்கிறது.