सुरक्षा, परीक्षण और औपचारिक सत्यापन

हम Runtime Verification हैं, जो एक अनुसंधान और विकास कंपनी है जो महत्वपूर्ण प्रणालियों की सुरक्षा और शुद्धता सुनिश्चित करने के लिए कठोर टूल बनाती है। हमारी टीम ने KEVM विकसित किया है, जो K Framework में लिखा गया Ethereum Virtual Machine (EVM) का सबसे पूर्ण और युद्ध-परीक्षणित औपचारिक सिमेंटिक्स है। KEVM केवल एक विनिर्देश नहीं है, यह एक निष्पादन योग्य विनिर्देश है जिसका उपयोग स्मार्ट कॉन्ट्रैक्ट के बारे में सिम्बोलिक रूप से तर्क करने, अनुरूपता परीक्षण चलाने, गैस उपयोग का विश्लेषण करने, प्रोग्राम को डीबग करने और शुद्धता गुणों को औपचारिक रूप से सत्यापित करने के लिए किया जा सकता है। यह पूर्ण Ethereum टेस्ट सूट पास करता है और इसका उपयोग उच्च-मूल्य वाले कॉन्ट्रैक्ट को सत्यापित करने के लिए किया जाता है, जिसमें Solidity और Vyper दोनों में ERC-20 टोकन शामिल हैं। हमने हाल ही में Pectra अपग्रेड का समर्थन करने के लिए सिमेंटिक्स को अपडेट किया है। KEVM का सक्रिय रूप से Kontrol द्वारा उपयोग किया जा रहा है - Solidity के लिए हमारा औपचारिक सत्यापन टूल, जिसका सक्रिय रूप से EVM इकोसिस्टम में अग्रणी टीमों द्वारा उपयोग किया जाता है, जिसमें Optimism, Ethereum Foundation, Lido, Uniswap के साथ-साथ व्यापक Ethereum समुदाय के सुरक्षा शोधकर्ता और ऑडिटर शामिल हैं। हम सक्रिय रूप से इस रिपॉजिटरी को बनाए रखते हैं, Ethereum के प्रोटोकॉल विकास में योगदान करते हैं, और Foundry जैसे डेवलपर टूलिंग के साथ एकीकृत करते हैं। KEVM के माध्यम से, हम सिद्ध रूप से सही और सुरक्षित स्मार्ट कॉन्ट्रैक्ट इंफ्रास्ट्रक्चर में जो संभव है उसकी सीमाओं को आगे बढ़ा रहे हैं।

Act औपचारिक सत्यापन (formal verification) के लिए एक स्मार्ट कॉन्ट्रैक्ट विनिर्देश भाषा और टूलकिट है। Act विनिर्देश एक EVM प्रोग्राम के सभी संभावित व्यवहारों का एक औपचारिक, उच्च-स्तरीय विवरण हैं। Act विनिर्देश के बारे में गुणों को साबित करने के लिए कई मौजूदा सामान्य उद्देश्य सत्यापन उपकरणों का लाभ उठाने की अनुमति देता है। ऐसे उपकरणों में SMT सॉल्वर (cvc5, z3, bitwuzla), प्रमेय सिद्ध करने वाले (Coq) और आर्थिक विश्लेषण टूलिंग (CheckMate, Open Games) शामिल हैं। Act विनिर्देशों को EVM में ठोस कार्यान्वयन के समतुल्य स्वचालित रूप से साबित किया जा सकता है। बहुत ही सरल कॉन्ट्रैक्ट्स के लिए, Act विनिर्देशों को EVM बाइटकोड से स्वचालित रूप से उत्पन्न किया जा सकता है। यह एक एंड-टू-एंड पाइपलाइन है जो EVM बाइटकोड के उच्च स्तरीय गुणों के बारे में सैद्धांतिक तर्क का समर्थन करती है। यह शुद्धता (जैसे अकाउंटिंग इनवेरिएंट्स) और आर्थिक गुणों (जैसे प्रोत्साहन संगतता) दोनों के बारे में तर्क का समर्थन करता है। Act विनिर्देश एक उच्च-स्तरीय स्मार्ट कॉन्ट्रैक्ट प्रतिनिधित्व के रूप में काम करते हैं, जो EVM संदर्भ में मौजूदा सामान्य उद्देश्य विश्लेषण और सत्यापन टूलिंग के आसान एकीकरण की अनुमति देता है।

Titanoboa एक Vyper इंटरप्रेटर और परीक्षण फ्रेमवर्क है जो Vyper स्मार्ट कॉन्ट्रैक्ट के लिए एक आधुनिक, एकीकृत विकास अनुभव प्रदान करता है। यह डेवलपर्स को सीधे Python के भीतर Vyper कॉन्ट्रैक्ट का परीक्षण और डीबग करने में सक्षम बनाता है, जो सुंदर ट्रेसबैक, फोर्किंग, डीबगिंग क्षमताओं, pytest एकीकरण और आउट-ऑफ़-द-बॉक्स फ़ज़िंग जैसी सुविधाएं प्रदान करता है। अपनी स्टैंडअलोन क्षमताओं से परे, Titanoboa Ape और Moccasin जैसे अन्य लोकप्रिय परीक्षण फ्रेमवर्क के लिए नींव के रूप में कार्य करता है, और Vyper इकोसिस्टम के लिए इंफ्रास्ट्रक्चर का एक मुख्य हिस्सा है।