Nonces, जिसका अर्थ “number used once” (एक बार इस्तेमाल होने वाला नंबर) है, का उपयोग replay attacks को रोकने के लिए digital signature schemes में किया जाता है। इस लेख के उद्देश्य के लिए, हम यह मानकर चलते हैं कि पाठक पहले से ही जानते हैं कि nonces क्या होते हैं और उनका उपयोग कैसे किया जाता है।

OpenZeppelin nonces.sol लाइब्रेरी एक counter का उपयोग करके signers के nonces को ट्रैक करती है जो प्रत्येक address के लिए increment होता है। यहाँ पूरी लाइब्रेरी दी गई है (संक्षिप्तता के लिए comments हटा दिए गए हैं):

Copy
abstract contract Nonces {

    error InvalidAccountNonce(address account, uint256 currentNonce);

    mapping(address account => uint256) private _nonces;

    function nonces(address owner) public view virtual returns (uint256) {
        return _nonces[owner];
    }

    function _useNonce(address owner) internal virtual returns (uint256) {
        unchecked {
            return _nonces[owner]++;
        }
    }

    function _useCheckedNonce(address owner, uint256 nonce) internal virtual {
        uint256 current = _useNonce(owner);
        if (nonce != current) {
            revert InvalidAccountNonce(owner, current);
        }
    }
}

संक्षेप में यह कॉन्ट्रैक्ट इस प्रकार है:

• nonces(address owner) एक view function है जो owner के लिए वर्तमान nonce लौटाता है।
• _useNonce(address owner) owner के लिए nonce को increment करता है और increment से पहले की nonce वैल्यू लौटाता है। उदाहरण के लिए, यदि Alice का nonce 2 था और हम उसके अकाउंट के लिए _useNonce को कॉल करते हैं, तो _useNonce 2 लौटाएगा, लेकिन फ़ंक्शन के execute होने के बाद उसका वर्तमान nonce 3 हो जाएगा।
• _useCheckedNonce(address owner, uint256 nonce) nonce को increment करता है, लेकिन जब तक nonce argument वर्तमान nonce के बराबर नहीं होता है, तब तक revert कर देता है। उदाहरण के लिए, यदि Alice का वर्तमान nonce 15 है, तो nonce argument के लिए 15 के अलावा कुछ भी देने पर revert हो जाएगा। फ़ंक्शन कॉल के बाद, Alice का nonce 16 हो जाएगा।

यह हमारे ट्यूटोरियल के पिछले हिस्से के Counter उदाहरण से बहुत अलग नहीं है, इसलिए Certora द्वारा इस लाइब्रेरी के लिए लिखे गए rules को समझाना आसान होगा।

यहाँ कुछ properties दी गई हैं जिन्हें साबित किया जाएगा:

• nonce केवल increment होता है
• nonce को increment करना कभी विफल (fail) नहीं होता
• एक nonce को increment करने का प्रभाव अन्य nonces पर नहीं पड़ता है

Nonces.sol Spec

यहाँ वह spec है जो Certora ने nonces.sol के लिए लिखा है।

Helper function

इस spec में यह जाँचने के लिए एक helper CVL function शामिल है कि nonce maximum value of uint256 नहीं है। व्यवहार में, एक counter इतना अधिक नहीं पहुँच सकता है:

Copy
function nonceSanity(address account) returns bool {
    return nonces(account) < max_uint256;
}

Nonce only increments

हम सबसे आसान rule से शुरुआत करेंगे, क्योंकि हमने parametric rules वाले अध्याय में ऐसा ही कुछ देखा था:

Copy
// address account in the argument is equivalent to
// declaring it inside the function body
rule nonceOnlyIncrements(
address account)
 {
    require nonceSanity(account);

    mathint nonceBefore = nonces(account);

    env e; method f; calldataarg args;
    f(e, args);

    mathint nonceAfter = nonces(account);

    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1, "nonce only increments";
}

यह rule कहता है कि “सभी लेन-देन (transactions) का परिणाम या तो nonce में कोई बदलाव न होने के रूप में होता है या फिर यह ठीक 1 से बढ़ जाता है।”

useNonce rule

useNonce rule दो assertions करता है:

• useNonce() को कॉल करने पर कभी revert नहीं होता है
• किसी account A पर nonce को increment करने से बाकी सभी accounts अप्रभावित रहते हैं, अर्थात उनका nonce नहीं बदलता है।

Copy
rule useNonce(address account) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    mathint nonceUsed = useNonce@withrevert(account);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    // liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

आइए इसे एक-एक करके समझें:

Copy
require nonceSanity(account);

यह कोड सुनिश्चित करता है कि जब nonce type(uint256).max हो, तो prover (असंभव) स्थिति का परीक्षण न करे।

Copy
address other;

यह other वह तरीका है जिससे हम rule के argument में निर्दिष्ट account के अलावा “किसी अन्य अकाउंट” का संदर्भ (reference) प्राप्त करते हैं। ध्यान दें कि इस rule में precondition के रूप में account != other की आवश्यकता नहीं होती है — इसे बाद में हैंडल किया जाता है।

Copy
mathint nonceBefore = nonces(account);
mathint otherNonceBefore = nonces(other);

यह state transition से पहले account और other के nonces की वैल्यूज़ को पढ़ता है।

Copy
mathint nonceUsed = useNonce@withrevert(account);
bool success = !lastReverted;

mathint nonceAfter = nonces(account);
mathint otherNonceAfter = nonces(other);

कोड mathint nonceUsed = useNonce@withrevert(account); एक मुख्य लाइन है, क्योंकि nonce वहीं increment होता है। हम nonceAfter और otherNonceAfter में नए nonce state को रिकॉर्ड करते हैं।

अब आइए assertions को देखें:

Copy
// liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";

याद रखें कि फ़ंक्शन useNonce वह nonce लौटाता है जो अभी उपयोग (consume) किया गया था, इसलिए nonceBefore == nonceUsed assertion का प्रयोग किया गया है।

अंतिम assertion यह बताता है कि कोई अन्य nonce नहीं बदला गया था। इसका लॉजिक contrapositive rule का उपयोग करके निकाला जा सकता है।

Implications के contrapositive rule के अनुसार, यदि A → B है, तो !B → !A होगा। मान लीजिए कि A का अर्थ other ≠ account है और B का अर्थ otherNonceBefore = otherNonceAfter है। तब हम कह सकते हैं कि “यदि other, account के बराबर नहीं है, तो other का nonce नहीं बदला।” इसलिए, हम लिख सकते हैं कि other ≠ account का तात्पर्य otherNonceBefore = otherNonceAfter है, या दूसरे शब्दों में A → B। Contrapositive rule का उपयोग करते हुए, हम कह सकते हैं कि !B → !A या समान रूप से otherNonceBefore ≠ otherNonceAfter (बदलाव हुआ) का तात्पर्य other = account है और यह बिल्कुल वही है जो अंतिम assertion कहता है।

useCheckedNonce rule

अंतिम rule पिछले उदाहरणों के बहुत सारे लॉजिक का फिर से उपयोग करता है, जिसे हम यहाँ नहीं समझाएंगे। मुख्य अंतर यह लाइन है: assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";। याद रखें कि useCheckedNonce तभी सफल होता है (revert नहीं होता) जब इसे पास किया गया nonce यूज़र के वर्तमान nonce के बराबर हो। इसलिए, biconditional operator यह एन्कोड करता है कि “यदि nonce मैच करता है, तो लेनदेन (transaction) का सफल होना सुनिश्चित है। यदि नहीं, तो इसका revert होना तय है।”

Copy
rule useCheckedNonce(address account, uint256 currentNonce) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    useCheckedNonce@withrevert(account, currentNonce);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    //// SEE HERE ////
    // liveness
    // the to_mathint cast makes it explicit to have the same type on both sides
    assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";

    // effect
    assert success => nonceAfter == nonceBefore + 1, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

यह लेख Certora Prover का उपयोग करके formal verification पर आधारित श्रृंखला का हिस्सा है।