प्रस्तावना (Introduction)
इस अध्याय में, हम CVL में env वेरिएबल का परिचय देंगे, जो हमें उन फंक्शन्स के लिए रूल्स बनाने में सक्षम बनाता है जो msg.sender, msg.value, और Solidity के अन्य ग्लोबल वेरिएबल्स जैसे block और tx पर निर्भर करते हैं।
हम पहले दो पर ध्यान केंद्रित करेंगे, जिन्हें CVL वेरिएबल env e से e.msg.sender और e.msg.value के रूप में एक्सेस किया जा सकता है।
हमारे पिछले उदाहरणों में, हमने उन्हें नज़रअंदाज़ कर दिया था क्योंकि जिन फंक्शन्स को हमने वेरिफाई किया था, वे एनवायरनमेंट वेरिएबल्स पर निर्भर नहीं थे। इसलिए, हमने इन फंक्शन्स को methods ब्लॉक में envfree के रूप में टैग किया था। यह Prover को यह बताता है कि एनालिसिस को सरल बनाने के लिए उन्हें प्योर लॉजिक के रूप में मानें और एनवायरनमेंट (ग्लोबल) वेरिएबल्स की अनदेखी करें।
हालाँकि, व्यवहार में, ट्रांजेक्शन्स इन एनवायरनमेंट वेरिएबल्स (env) पर काफी हद तक निर्भर करते हैं, और यहाँ हम एक्सप्लोर करेंगे कि msg.sender और msg.value के साथ रूल्स कैसे बनाए जाएं।
e.msg.sender और e.msg.value (non-payable)
एक साधारण owner-controlled counter कॉन्ट्रैक्ट पर विचार करें, जहाँ केवल owner को ही काउंटर बढ़ाने (increment) की अनुमति है:
contract OwnerCounter {
uint256 public counter;
address public owner;
constructor(address _owner) {
owner = _owner;
}
function increment() public {
require(msg.sender == owner, "not owner");
counter++;
}
}
increment() फंक्शन में एक require स्टेटमेंट है जो अगर कॉलर owner नहीं है तो revert कर देगा। इसलिए, हमारे रूल को msg.sender पर निर्भर होना चाहिए।
इस प्रॉपर्टी को वेरिफाई करने के लिए: “केवल owner ही increment() को सफलतापूर्वक कॉल कर सकता है”, हम निम्नलिखित CVL रूल लिखते हैं:
methods {
function owner() external returns (address) envfree;
function counter() external returns (uint256) envfree;
}
rule increment_onlyOwnerCanCallIncrement(env e) {
address current = owner();
increment@withrevert(e);
assert !lastReverted <=> e.msg.sender == current, "access control failed";
}
methods ब्लॉक में, owner() और counter() फंक्शन्स को envfree के रूप में मार्क किया गया है क्योंकि वे स्टोरेज वेरिएबल्स के view फंक्शन्स हैं और एनवायरनमेंट वेरिएबल्स या env पर निर्भर नहीं करते हैं।
हालाँकि, increment() फंक्शन एनवायरनमेंट पर निर्भर है (इसलिए पैरामीटर e है)। अगर फंक्शन्स को एनवायरनमेंट पर निर्भर माना जाता है, तो उन्हें स्पष्ट रूप से methods ब्लॉक में डिक्लेयर करने की आवश्यकता नहीं होती है। इस प्रकार, हम increment() को methods ब्लॉक में शामिल नहीं करते हैं।
rule ब्लॉक में, env e डिक्लेरेशन को पैरामीटर के रूप में या rule ब्लॉक के अंदर रखा जा सकता है। दोनों ही मान्य (valid) हैं और केवल कोड स्टाइल की प्राथमिकताएं हैं:
rule increment_onlyOwnerCanCallIncrement(env e) {
...
}
rule increment_onlyOwnerCanCallIncrement() {
env e;
...
}
अब, जब हम किसी ऐसे Solidity फंक्शन को कॉल (invoke) करते हैं जो एनवायरनमेंट पर निर्भर है, तो हमें आर्गुमेंट e शामिल करना होगा:
increment@withrevert(e);
(e) को छोड़ने पर एक कंपाइलर एरर आएगा, जो आपको methods ब्लॉक में फंक्शन को envfree के रूप में डिक्लेयर करने के लिए मजबूर करेगा। हालाँकि, अगर आप आँख मूंदकर इसका पालन करते हैं और इसे envfree के रूप में डिक्लेयर करते हैं, तो वायलेशन्स होंगे, और Prover संकेत देगा कि फंक्शन एनवायरनमेंट पर निर्भर है।
अब, अंततः, चलिए assertion की ओर बढ़ते हैं:
assert !lastReverted <=> e.msg.sender == current, "access control failed";
यह चेक करता है कि increment() केवल और केवल तभी revert नहीं करता है जब msg.sender == owner हो। यदि assertion फेल हो जाता है, तो इसका मतलब है कि Prover को एक काउंटर-एग्जांपल (counterexample) मिला है — या तो सही owner को increment() कॉल करने से रोक दिया गया था, या कोई गैर-owner (non-owner) इसे सफलतापूर्वक कॉल करने में सक्षम था।
हालाँकि, जब हम इस रूल को रन करते हैं, तो हमें एक अप्रत्याशित revert केस का सामना करना पड़ता है — जब msg.value != 0 होता है। ऐसा इसलिए होता है क्योंकि increment() एक non-payable फंक्शन है, जिसका मतलब है कि यह Ether स्वीकार नहीं कर सकता है।
Solidity में, एक कॉन्ट्रैक्ट फंक्शन कॉल के माध्यम से Ether प्राप्त कर सकता है, लेकिन केवल तभी जब फंक्शन को स्पष्ट रूप से payable के रूप में मार्क किया गया हो; अन्यथा, ट्रांजेक्शन revert हो जाएगा। भेजे गए Ether की मात्रा ग्लोबल वेरिएबल msg.value में स्टोर होती है, जो वैल्यू को wei (Ether की सबसे छोटी इकाई) में रखता है।
चूँकि increment() को payable के रूप में मार्क नहीं किया गया है, कोई भी नॉन-जीरो (nonzero) msg.value एक revert का कारण बनता है, जैसा कि नीचे दी गई रिपोर्ट में दिखाया गया है:
इसे हल करने के लिए, हमें एक प्रीकंडीशन (precondition) के रूप में e.msg.value == 0 को रखना होगा।
फिर, एक और अप्रत्याशित revert तब होता है जब counter == max_uint256 होता है। चूँकि max_uint256 वह अधिकतम वैल्यू है जिसे काउंटर रख सकता है, counter++ का प्रयास करने पर ओवरफ्लो (overflow) revert होगा (ध्यान दें कि हम फंक्शन को withrevert टैग के साथ कॉल कर रहे हैं):
इसे हल करने के लिए, काउंटर को ओवरफ्लो होने से रोकने के लिए हमें एक और प्रीकंडीशन require(counter() < max_uint256) जोड़नी होगी।
इन दो अप्रत्याशित revert केसेस की पहचान होने के साथ, दोनों कंडीशन्स को प्रीकंडीशन्स के रूप में शामिल किया जाना चाहिए। नीचे सही किया गया रूल और Prover रिपोर्ट दी गई है। जैसा कि अपेक्षित था, वेरिफिकेशन पास हो जाता है:
rule increment_onlyOwnerCanCallIncrement(env e) {
address current = owner();
require e.msg.value == 0;
require counter() < max_uint256;
increment@withrevert(e);
assert !lastReverted <=> e.msg.sender == current, "access control failed";
}
Prover रन: link
<=> के बजाय => के साथ प्रीकंडीशन्स (Preconditions) में ढील देना (Relaxing)
ऊपर हमने जो रूल बनाया था, वह कहता है “फंक्शन केवल और केवल तभी revert करता है जब कॉलर owner न हो।” चूँकि अन्य वैध revert कंडीशन्स भी हैं, अर्थात् msg.value != 0 और counter() == max_uint256, “फंक्शन केवल और केवल तभी revert करता है जब कॉलर owner न हो” को सत्य साबित करने के लिए हमें प्रीकंडीशन में उन संभावनाओं को खत्म करना पड़ा था।
अगर हम इसके बजाय यह कहना चाहें कि, “यदि कोई गैर-owner फंक्शन को कॉल करता है, तो ट्रांजेक्शन revert हो जाता है”, तो हम बिना प्रीकंडीशन्स के इम्प्लीकेशन ऑपरेटर (implication operator) का उपयोग कर सकते हैं। अन्य revert केसेस (यानी msg.value != 0 और काउंटर का अधिकतम होना) वायलेशन का कारण नहीं बनते हैं। हम केवल इस बात की परवाह करते हैं कि गैर-owner द्वारा फंक्शन को कॉल करने पर वह revert हो जाए।
अब यह कहने के बाद, यहाँ औपचारिक रूप से वेरिफाई करने के लिए प्रॉपर्टी है: “यदि कॉलर owner नहीं है, तो फंक्शन को revert होना चाहिए।” नीचे इसके लिए रूल दिया गया है — एक सरल रूल — और जैसा कि अपेक्षित था, यह रूल पास हो जाता है:
rule increment_notOwnerCannotCallIncrement(env e) {
address current = owner();
increment@withrevert(e);
assert e.msg.sender != current => lastReverted, "access control failed";
}
Prover रन: link
अब, हम समझते हैं कि एनवायरनमेंट पर निर्भर फंक्शन्स के लिए रूल्स कैसे लिखे जाते हैं। Prover कॉलर के आधार पर निष्पादन (execution) के बारे में तर्क (reason) करने के लिए e.msg.sender का उपयोग करता है और ETH ट्रांसफर्स के बारे में तर्क करने के लिए e.msg.value का उपयोग करता है। अगले अध्याय में, हम दोनों कॉन्सेप्ट्स को अधिक विस्तार से एक्सप्लोर करेंगे।
सारांश
- CVL में
envवेरिएबल उन फंक्शन्स के बारे में तर्क (reasoning) करने की अनुमति देता है जोmsg.sender,msg.value, और अन्य ग्लोबल वेरिएबल्स पर निर्भर करते हैं। - ऐसे फंक्शन्स में
env eशामिल होना चाहिए, या तो रूल पैरामीटर के रूप में या रूल ब्लॉक के भीतर। - इन एनवायरनमेंट पर निर्भर फंक्शन्स को methods ब्लॉक में डिक्लेयर करने की आवश्यकता नहीं होती है, जबकि
envfreeफंक्शन्स को स्पष्ट रूप से डिक्लेयर किया जाना चाहिए औरenvfreeके रूप में मार्क किया जाना चाहिए। - यदि किसी एनवायरनमेंट पर निर्भर फंक्शन को इस तरह सही ढंग से इम्प्लीमेंट नहीं किया गया है, तो यह फिर भी कंपाइल होगा और Prover पर रन करेगा, लेकिन वायलेशन्स और चेतावनियां (warnings) उत्पन्न करेगा।
- यदि
msg.valueका ठीक से हिसाब नहीं रखा गया है, तो Prover इससे उत्पन्न होने वाले वायलेशन्स और काउंटर-एग्जांपल्स (counterexamples) जनरेट करेगा।
यह लेख Certora Prover का उपयोग करके फॉर्मल वेरिफिकेशन पर एक सीरीज़ का हिस्सा है