यह लेख बताता है कि कैसे Certora ने Initializable.sol OpenZeppelin कॉन्ट्रैक्ट को औपचारिक रूप से सत्यापित (formally verify) किया। हम मान कर चलते हैं कि पाठक पहले से ही जानते हैं कि इस कॉन्ट्रैक्ट का उपयोग कैसे किया जाता है। यदि नहीं, तो कृपया Initializable Contracts पर हमारा लेख देखें।
Upgradeable contracts में, constructor का उपयोग नहीं किया जाता है। इसके बजाय, डिप्लॉयमेंट (deployment) के बाद, डिप्लॉयर initialize(...) को कॉल करता है और यह state variables को उनकी प्रारंभिक स्थितियों में सेट कर देता है। initialize(...) फ़ंक्शन को केवल एक बार ही कॉल किया जा सकना चाहिए।
यदि बाद में storage variables को किसी अन्य वैल्यू पर सेट करने की अनुमति देनी हो (जैसे कि यदि कोई ERC-20 टोकन अपना नाम या totalSupply बदलता है) तो ये बदलाव reinitialize फ़ंक्शन के माध्यम से किए जाने चाहिए। external functions का नाम “initializer” और “reinitializer” होना आवश्यक नहीं है, लेकिन उन फ़ंक्शंस पर OpenZeppelin लाइब्रेरी के initializer() और reinitializer() modifier का लागू होना आवश्यक है।
सुरक्षा उद्देश्यों के लिए, upgradeable contracts में initializers के संबंध में निम्नलिखित गुण (properties) होने चाहिए:
- एक बार जब initializer कॉल कर लिया जाता है, तो इसे फिर कभी कॉल करने योग्य नहीं होना चाहिए (सभी कॉल्स revert होनी चाहिए)।
- implementation contract में initializer को कॉल करना संभव नहीं होना चाहिए। केवल proxy में मौजूद initializer ही कॉल किया जा सकना चाहिए, क्योंकि सभी state proxy contract में रखी जाती है। यही कारण है कि proxy patterns के logic contracts अपने constructor में
_disableInitializers()को कॉल करते हैं। - एक बार जब initializer और reinitializer डिसेबल (disabled) हो जाते हैं, तो उन्हें स्थायी रूप से डिसेबल ही रहना चाहिए।
- यदि हम reinitializer फ़ंक्शन को कॉल करते हैं, तो हमें पिछले वर्ज़न (version) से उसे बढ़ाना (increment) होगा। वर्ज़न एक
uint64वेरिएबल के रूप में स्टोर किया जाता है।
ध्यान दें कि initializer और reinitializer का access control इस कॉन्ट्रैक्ट के दायरे (scope) से बाहर है। यह कॉन्ट्रैक्ट यह भी लागू (enforce) नहीं करता है कि उन फ़ंक्शंस के नाम क्या हैं, यह केवल यह सुनिश्चित करता है कि modifiers की कार्यक्षमता सही है।
हम OpenZeppelin की Initializable.spec फ़ाइल के अधिकांश हिस्से को कवर करेंगे, लेकिन पूरा नहीं, क्योंकि इसके कुछ हिस्से उन तकनीकों पर निर्भर करते हैं जिन्हें हमने अभी तक कवर नहीं किया है। हालाँकि, कोर्स में अब तक हमने जो कुछ भी कवर किया है, उसके आधार पर इसके अधिकांश हिस्से समझे जा सकने चाहिए।
यहाँ पहला नियम (rule) है जिसकी हम जाँच करते हैं:
rule cannotInitializeTwice() {
require isInitialized();
initialize@withrevert();
assert lastReverted, "contract must only be initialized once";
}
यह कहता है कि यदि कॉन्ट्रैक्ट initialized है, तो initialize() को कॉल करने पर यह revert हो जाएगा। यह नियम यह नहीं कहता है कि यदि कॉन्ट्रैक्ट initialized नहीं है, तो initialize() को कॉल करने पर यह revert नहीं होता है, या दूसरे शब्दों में, एक uninitialized कॉन्ट्रैक्ट को initialize किया जा सकता है। require स्टेटमेंट इस नियम के दायरे (scope) को केवल उन मामलों तक सीमित कर देता है जहाँ initializer को पहले ही कॉल किया जा चुका है।
यह विशिष्टता (specification) कि एक uninitialized कॉन्ट्रैक्ट को initialize किया जा सकता है, निम्नलिखित नियम द्वारा कवर की गई है:
rule initializeEffects() {
requireInvariant notInitializing();
bool isUninitializedBefore = isUninitialized();
initialize@withrevert();
bool success = !lastReverted;
assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts";
assert success => version() == 1, "initialize must set version() to 1";
}
यह नियम कहता है कि initialize केवल और केवल तभी सफल (succeed) होता है जब कॉन्ट्रैक्ट पहले initialize न किया गया हो। यदि initialization सफल होता है, तो वर्ज़न को 1 पर सेट किया जाना चाहिए। requireInvariant सिंटैक्स (syntax) कुछ ऐसा है जिसे हमने अभी तक कवर नहीं किया है, हम बाद के ट्यूटोरियल में इस पर फिर से विचार करेंगे।
यह नियम कि reinitializer डिसेबल (disable) स्टेटस को ओवरराइड (override) नहीं कर सकता, काफी हद तक स्वयं स्पष्ट (self explanatory) है:
rule cannotReinitializeOnceDisabled() {
require isDisabled();
uint64 n;
reinitialize@withrevert(n);
assert lastReverted, "contract is disabled";
}
दूसरे शब्दों में, यदि कॉन्ट्रैक्ट डिसेबल (disabled) है, तो reinitialize पर की गई कोई भी कॉल revert का कारण बनती है।
जब reinitializer को कॉल किया जाता है, तो एक नया वर्ज़न सेट किया जाना चाहिए, और वह वर्ज़न पुराने वर्ज़न से बड़ा होना चाहिए। निम्नलिखित नियम कहता है कि यदि नया वर्ज़न वह वर्ज़न है जिसे argument में पास किया गया है, और यदि ट्रांज़ैक्शन revert नहीं हुआ है, तो वह नया वर्ज़न पिछले वाले वर्ज़न से बड़ा है।
rule reinitializeEffects() {
requireInvariant notInitializing();
uint64 versionBefore = version();
uint64 n;
reinitialize@withrevert(n);
bool success = !lastReverted;
assert success <=> versionBefore < n, "can only reinitialize to a later versions";
assert success => version() == n, "reinitialize must set version() to n";
}
अंतिम नियम जिसकी हम जाँच करते हैं वह यह बताता है कि यदि कॉन्ट्रैक्ट “initializing state” (यानी कॉन्ट्रैक्ट वर्तमान में storage variables सेट कर रहा है या reinitialize कर रहा है) में नहीं है, तो disable को कॉल करना हमेशा सफल (succeed) होता है।
rule disableEffect() {
requireInvariant notInitializing();
disable@withrevert();
bool success = !lastReverted;
assert success, "call to _disableInitializers failed";
assert isDisabled(), "disable state not set";
}
सारांश
यहाँ हमने जो नियम दिखाए हैं उन्हें समझना बहुत ही आसान है, लेकिन हम उनकी समीक्षा इसलिए करते हैं ताकि यह प्रदर्शित किया जा सके कि formal verification को हमेशा जटिल होने की आवश्यकता नहीं है। हमने यहाँ जो नियम दिखाए हैं उन्हें एक यूनिट टेस्ट (unit test) के साथ भी पूरा किया जा सकता है, लेकिन formal verification अधिक विस्तृत (thorough) और उच्च आश्वासन (high assurance) वाला होता है।
यह लेख Certora Prover का उपयोग करके formal verification पर एक सीरीज़ का हिस्सा है