परिचय
पिछले अध्याय में, हमने प्रदर्शित किया था कि मैपिंग वैल्यूज़ में बदलावों से जुड़ी properties को verify करने के लिए Sstore hooks आवश्यक हैं। यह hook स्टोरेज राइट्स (storage writes) की निगरानी करता है, प्रत्येक key के लिए पुराने और नए मान (values) कैप्चर करता है, और ghost variables को अपडेट करने के लिए कस्टम CVL कोड निष्पादित (execute) करता है।
हमने इसे एक साधारण कॉन्ट्रैक्ट PointSystem का उपयोग करके प्रदर्शित किया था जो किसी उपयोगकर्ता (user) को पॉइंट्स देता है, उन्हें pointsOf[address] में रिकॉर्ड करता है, और totalPoints में कुल (total) अपडेट करता है:
contract PointSystem {
mapping (address => uint256) public pointsOf;
uint256 public totalPoints;
function addPoints(address _user, uint256 _amount) external {
pointsOf[_user] += _amount;
totalPoints += _amount;
}
}
हालाँकि, व्यवहार में, कॉन्ट्रैक्ट्स गैस दक्षता (gas efficiency) के लिए ऑप्टिमाइज़ होते हैं और ऐसे मामलों में unchecked ब्लॉक्स का उपयोग करते हैं जहाँ ओवरफ़्लो (overflow) होना व्यावहारिक रूप से असंभव होता है। उदाहरण के लिए, ऊपर दिया गया PointSystem कॉन्ट्रैक्ट एक unchecked ब्लॉक का उपयोग कर सकता है और इसे ऐसे तरीके से लागू (implement) किया जा सकता है जिसमें ओवरफ़्लो न हो सके।
नीचे दिया गया कॉन्ट्रैक्ट इसे प्रदर्शित करता है — जब pointsOf[address] में जोड़ा जाता है तो unchecked ब्लॉक का सुरक्षित रूप से उपयोग किया जाता है:
contract PointSystemUnchecked {
mapping (address => uint256) public pointsOf;
uint256 public totalPoints;
function addPoints(address _user, uint256 _amount) external {
totalPoints += _amount;
unchecked {
pointsOf[_user] += _amount;
}
}
}
यह इसलिए काम करता है क्योंकि totalPoints += _amount पहले unchecked के बिना execute होता है, इसलिए यह ओवरफ़्लो होने पर रिवर्ट (revert) हो जाता है और एक सर्किट ब्रेकर के रूप में कार्य करता है। चूँकि pointsOf[_user] में होने वाली प्रत्येक वृद्धि totalPoints को भी बढ़ाती है, कोई भी उपयोगकर्ता कभी भी कुल पॉइंट्स (total points) से अधिक पॉइंट्स एकत्र नहीं कर सकता है।
हालाँकि, Prover इस तर्क को ध्यान में नहीं रखता है। जैसे ही हम एक unchecked ब्लॉक जोड़ते हैं, Prover अब अंकगणितीय सुरक्षा (arithmetic safety) नहीं मानता है। इसका मतलब है कि यह जानबूझकर ऐसे प्रारंभिक अवस्थाओं (initial states) को असाइन करेगा जो unchecked ऑपरेशन्स में रैपअराउंड (wraparound) व्यवहार को ट्रिगर करते हैं।
Prover, unchecked ब्लॉक्स में कोई अंकगणितीय सुरक्षा नहीं मानता है
इसे प्रदर्शित करने के लिए, आइए नए PointSystemUnchecked कॉन्ट्रैक्ट के खिलाफ PointSystem के लिए हमारे स्पेसिफिकेशन्स (specifications) चलाएं। नीचे स्पेसिफिकेशन्स दिए गए हैं (invariant और rule दोनों), जो अब unchecked ब्लॉक के कारण विफल (fail) हो जाते हैं:
ghost mathint g_sumOfUserPoints {
init_state axiom g_sumOfUserPoints == 0;
}
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
invariant sumOfUserPointsEqualsTotalPoints_i() // fails
totalPoints() == g_sumOfUserPoints;
rule sumOfUserPointsEqualsTotalPoints_r(env e, method f, calldataarg args) { // fails
require totalPoints() == 0 && g_sumOfUserPoints == 0;
f(e, args);
assert totalPoints() == g_sumOfUserPoints;
}
Prover रन (विफल): link
यह एक सवाल उठाता है: जब unchecked ब्लॉक का उपयोग किया जाता है तो totalPoints और g_sumOfUserPoints अलग क्यों हो जाते हैं? इसका उत्तर यह है कि unchecked ब्लॉक, Prover को किसी arbitrary user (pointsOf[address]) को एक गैर-शून्य (nonzero) प्रारंभिक मान (initial value) असाइन करने के लिए ट्रिगर करता है ताकि execution पथ के साथ एक ओवरफ़्लो परिदृश्य बनाया जा सके, जबकि totalPoints शून्य से शुरू होता है (वास्तविक प्रारंभिक अवस्था)। परिणामस्वरूप, Prover ने एक ऐसी अवस्था का परीक्षण किया जहाँ उपयोगकर्ता के पॉइंट्स कुल पॉइंट्स से अधिक हैं — जो कॉन्ट्रैक्ट में एक असंभव अवस्था है।
Prover जानबूझकर ओवरफ़्लो को ट्रिगर करने के लिए प्रारंभिक अवस्थाएँ (initial states) सेट करता है
अब, आइए हमारे द्वारा लिखे गए rule और invariant के कॉल ट्रेस (call trace) का विश्लेषण करें ताकि यह समझा जा सके कि उल्लंघन (violation), जो कि एक फॉल्स पॉजिटिव (false positive) है, कैसे उत्पन्न हुआ।
Rule कॉल ट्रेस
Prover एड्रेस 0xf (pointsOf[0xf] = 0x2) को एक गैर-शून्य मान (nonzero value) असाइन करता है ताकि बाद में, uint256 रेंज के भीतर एक पर्याप्त रूप से बड़ा मान जोड़कर, यह एक ओवरफ़्लो को सिमुलेट कर सके:
फिर कॉल addPoints(_user=0xf, _amount=2^256 - 2) निष्पादित (execute) होता है, जिसके परिणामस्वरूप pointsOf[address] = 0x2 + (2^256 - 2) = 2^256 ≡ 0 होता है (ओवरफ़्लो के कारण नया मान शून्य पर रैप (wrap) हो जाता है):
addPoints() को इनवोक (invoke) करने से कॉन्ट्रैक्ट में totalPoints में भी वृद्धि होती है। चूँकि totalPoints शुरू में शून्य है, 2^256 - 2 (आर्गुमेंट) जोड़ने पर अंतिम मान 2^256 - 2 हो जाता है, जैसा कि नीचे दिए गए ट्रेस में दिखाया गया है:
अब, आइए देखें कि Sstore हुक लॉजिक g_sumOfUserPoints की गणना कैसे करता है:
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
प्रारंभिक मान (Initial values):
g_sumOfUserPoints = 0(प्रारंभिक मान)pointsOf[0xf] (oldVal) = 0x2(प्रारंभिक मान)
addPoints(0xf, 2^256 - 2) के बाद पोस्ट-कॉल मान (Post-call values):
pointsOf[0xf] (newVal) = 0x0(0x2और2^256 - 2जोड़ने के बाद रैप्ड-अराउंड मान)pointsOf[0xf] (oldVal) = 0x2g_sumOfUserPoints = 0 + (0x0 - 0x2) = -0x2
इसलिए, totalPoints (2^256 - 2) अब g_sumOfUserPoints(-2) के बराबर नहीं है:
Invariant कॉल ट्रेस
यही समस्या invariant के साथ भी हुई। Prover ने जानबूझकर pointsOf[address] = 0xc00…000 को सीड (seed) किया, जो प्री-कॉल अवस्था (pre-call state) में totalPoints से अधिक है:
हमें यह देखने के लिए किसी अन्य कॉल ट्रेस की आवश्यकता नहीं है कि, अंतिम अवस्था (final state) में, अकाउंटिंग विसंगतियाँ (inconsistencies) होती हैं, और वे totalPoints को g_sumOfUserPoints से अलग कर देती हैं।
मुख्य समस्या
totalPoints और g_sumOfUserPoints दोनों शून्य से शुरू होते हैं (जैसा कि rule precondition और invariant के init_state axiom में दिखाया गया है), लेकिन Prover एक ओवरफ़्लो पथ (overflow path) का परीक्षण करने के लिए pointsOf[user] को एक गैर-शून्य मान (nonzero value) पर सेट करता है।
इसका कारण यह है कि यदि pointsOf[user] शून्य से शुरू होता है तो ओवरफ़्लो नहीं हो सकता है। शून्य में max_uint256 मान जोड़ने से केवल uint256 सीमा तक पहुँचा जाता है, उसके पार नहीं। unchecked ऑपरेशन pointsOf[_user] += _amount में ओवरफ़्लो उत्पन्न करने के लिए, pointsOf[_user] का प्रारंभिक मान पहले से ही शून्य से अधिक होना चाहिए — उदाहरण के लिए, 2 + (2²⁵⁶ − 2) = 2²⁵⁶ ≡ 0।
यह सेटअप एक अवास्तविक अवस्था (unrealistic state) बनाता है जहाँ pointsOf[user] > 0 जबकि totalPoints = 0, जो वास्तविक execution में नहीं हो सकता क्योंकि addPoints() के भीतर दोनों मान हमेशा एक साथ बदलते हैं।
Ghost और स्टोरेज के बीच वास्तविक संबंध को परिभाषित करना
आइए Sstore हुक implementation को फिर से देखें।
Sstore हुक pointsOf[address] में होने वाले प्रत्येक राइट (write) से बदलाव (newVal - oldVal) जोड़कर ghost वेरिएबल g_sumOfUserPoints को अपडेट करता है:
hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}
हालाँकि, Prover को ghost g_sumOfUserPoints और स्टोरेज pointsOf[address] के बीच वास्तविक संबंध (realistic relationship) का पता नहीं होता है।
g_sumOfUserPoints बस उन मानों को स्वीकार करता है जिन्हें यह प्रोसेस करता है, और Prover g_sumOfUserPoints में फीड करने के लिए pointsOf[address] का यथार्थवादी मान निर्धारित नहीं कर सकता। परिणामस्वरूप, Prover सभी संभावित मानों का परीक्षण करता है, जिनमें ऐसे अवास्तविक मान भी शामिल हैं जो विफलताओं का कारण बन सकते हैं।
आगे हमें जो करने की आवश्यकता है वह यह है कि Prover को स्पष्ट रूप से प्रत्येक व्यक्तिगत उपयोगकर्ता के पॉइंट्स (pointsOf[user]) और उपयोगकर्ता पॉइंट्स के योग (g_sumOfUserPoints) के बीच इच्छित संबंध का निर्देश दें: g_sumOfUserPoints हमेशा pointsOf[user] से बड़ा या उसके बराबर होना चाहिए। हम Sload हुक का उपयोग करके इस संबंध को लागू (enforce) कर सकते हैं।
Mappings के लिए Sload हुक सिंटैक्स
आगे बढ़ने से पहले, आइए पहले mappings के लिए Sload hooks के सिंटैक्स और पैटर्न को देखें। hooks का सिंटैक्स साधारण वेरिएबल्स के समान ही है, सिवाय इसके कि mappings के लिए हमें KEY कीवर्ड शामिल करना होगा। उदाहरण के लिए: storageVar[KEY address user]:
hook Sload uint256 val balances[KEY address user] {
// implement hook logic
}
Sload हुक में, स्थानीय हुक वेरिएबल (local hook variable) val उस मान को कैप्चर करता है जिसे की (key) user के साथ स्टोरेज मैपिंग से पढ़ा (read) गया है।
किसी कॉन्ट्रैक्ट ऑपरेशन में, वेरिएबल के अपडेट या प्रोसेस होने से पहले स्टोरेज रीड्स (storage reads) होते हैं। उदाहरण के लिए, इस Solidity लाइन pointsOf[_user] += _amount में, _amount जोड़ने से पहले pointsOf[_user] को अपना वर्तमान मान पढ़ना होगा।
इसलिए, यह महत्वपूर्ण है कि स्टोरेज मैपिंग से “पढ़ा गया मान” (value read) सटीक हो, इससे पहले कि इसके डेटा को प्रोसेस किया जाए और (Sstore hooks के माध्यम से) एक ghost वेरिएबल को असाइन किया जाए।
चूँकि Prover स्टोरेज वेरिएबल्स और ghost वेरिएबल्स के बीच के संबंध को नहीं जानता है, हमें स्पष्ट रूप से इस संबंध को निम्नानुसार परिभाषित करना होगा:
hook Sload uint256 points pointsOf[KEY address account] {
require g_sumOfUserPoints >= points;
}
यहाँ, points एक स्थानीय हुक वेरिएबल (local hook variable) है जो मैपिंग pointsOf[address] से पढ़े गए मान को कैप्चर करता है। यह implementation Prover को केवल उन अवस्थाओं (states) का अन्वेषण (explore) करने के लिए बाध्य (constrain) करता है जहाँ g_sumOfUserPoints, points से बड़ा या उसके बराबर है।
वैकल्पिक रूप से, हम require के बारे में यह सोच सकते हैं कि यह pointsOf[address] (किसी विशेष उपयोगकर्ता के पॉइंट्स) के मान को हमेशा g_sumOfUserPoints के बराबर या उससे कम होने के लिए बाध्य करता है। इसका मतलब है कि Prover कभी भी ऐसे परिदृश्य (scenario) का परीक्षण नहीं करेगा जहाँ किसी व्यक्तिगत उपयोगकर्ता के पॉइंट्स, ghost वेरिएबल द्वारा ट्रैक किए गए कुल पॉइंट्स (total points) से अधिक हों।
Sload हुक का उपयोग करने से ghost-स्टोरेज की विसंगतियां (inconsistencies) ठीक हो जाती हैं
हमारे स्पेसिफिकेशन (specification) में, हम यह लागू करने के लिए ऊपर दिखाए गए Sload हुक को जोड़ते हैं कि सभी पॉइंट्स के योग को दर्शाने वाला ghost वेरिएबल (g_sumOfUserPoints) स्टोरेज से पढ़े जाने पर हमेशा किसी भी व्यक्तिगत pointsOf[account] मान से बड़ा या उसके बराबर हो।
यह Prover को ऐसी अवस्था को इनिशियलाइज़ (initialize) करने से रोकता है जहाँ किसी एकल खाते का बैलेंस (balance) कुल योग (total sum) से अधिक हो — एक ऐसी स्थिति जो, जैसा कि हमने देखा है, फॉल्स पॉजिटिव्स (false positives) की ओर ले जाती है।
hook Sload uint256 points pointsOf[KEY address account] {
require g_sumOfUserPoints >= points;
}
इसके लागू होने के साथ, CVL rule और invariant दोनों सफल हो जाते हैं, और property वेरीफाई (verify) हो जाती है:
Prover रन (सत्यापित/verified): link
सारांश
uncheckedब्लॉक Solidity के अंतर्निहित (built-in) ओवरफ़्लो चेक को डिसेबल कर देता है, जिसके कारण Prover कार्यान्वयन (implementation) का परीक्षण करने के लिए ओवरफ़्लो को ट्रिगर करने वाले प्रारंभिक मान (initial values) असाइन करके असुरक्षित अंकगणित (unsafe arithmetic) का अन्वेषण (explore) करता है।- इन अवास्तविक प्रारंभिक मानों (unrealistic initial values) को
Sloadहुक मेंrequireका उपयोग करके रोका जा सकता है, ताकि Prover केवल निर्दिष्ट सीमाओं (specified bounds) के भीतर ही अवस्थाओं का अन्वेषण करे, जैसे कि यह आवश्यक करना कि किसी व्यक्तिगत पॉइंट का मान कुल (total) से अधिक न हो।
यह लेख Certora Prover का उपयोग करके formal verification पर एक श्रृंखला (series) का हिस्सा है