Ownable एक एब्सट्रैक्ट कॉन्ट्रैक्ट (abstract contract) है जो ओनर-आधारित (owner-based) एक्सेस कंट्रोल प्रदान करता है। जब इसे इनहेरिट किया जाता है, तो यह onlyOwner मॉडिफायर का उपयोग करके विशिष्ट फ़ंक्शंस को केवल ओनर तक सीमित कर देता है। इसके तीन मुख्य तंत्र (mechanisms) हैं, जिनमें से प्रत्येक को निम्नलिखित फ़ंक्शंस के माध्यम से लागू किया गया है:

• onlyOwner()

  यह मॉडिफायर विशिष्ट फ़ंक्शंस तक पहुंच को सीमित करता है, जिससे केवल ओनर ही उन्हें कॉल कर सकता है।

• renounceOwnership()

  यह पब्लिक फ़ंक्शन onlyOwner मॉडिफायर द्वारा सुरक्षित है, जिससे केवल ओनर ही इसे कॉल कर सकता है। जब इसे निष्पादित (execute) किया जाता है, तो यह ओनर को शून्य एड्रेस (address(0)) पर सेट कर देता है। त्यागने (renouncement) के बाद, onlyOwner द्वारा प्रतिबंधित सभी फ़ंक्शंस स्थायी रूप से अगम्य (inaccessible) हो जाते हैं।

• transferOwnership(address)

  यह भी एक पब्लिक फ़ंक्शन है और, renounceOwnership() की तरह, यह onlyOwner मॉडिफायर द्वारा प्रतिबंधित है। जब इसे किसी वैध एड्रेस (जो address(0) न हो) के साथ कॉल किया जाता है, तो यह कॉन्ट्रैक्ट के ओनरशिप को उस एड्रेस पर अपडेट कर देता है, भले ही वह वर्तमान ओनर का ही एड्रेस क्यों न हो।

औपचारिक सत्यापन (formal verification) के उनके दृष्टिकोण को समझाते समय संदर्भ के लिए नीचे OpenZeppelin Ownable contract दिया गया है:

Copy
// SPDX-License-Identifier: MIT
// OpenZeppelin Contracts (last updated v5.0.0) (access/Ownable.sol)

pragma solidity ^0.8.20;

import {Context} from "../utils/Context.sol";

/**
 * @dev Contract module which provides a basic access control mechanism, where
 * there is an account (an owner) that can be granted exclusive access to
 * specific functions.
 *
 * The initial owner is set to the address provided by the deployer. This can
 * later be changed with {transferOwnership}.
 *
 * This module is used through inheritance. It will make available the modifier
 * `onlyOwner`, which can be applied to your functions to restrict their use to
 * the owner.
 */
abstract contract Ownable is Context {
    address private _owner;

    /**
     * @dev The caller account is not authorized to perform an operation.
     */
    error OwnableUnauthorizedAccount(address account);

    /**
     * @dev The owner is not a valid owner account. (eg. `address(0)`)
     */
    error OwnableInvalidOwner(address owner);

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    /**
     * @dev Initializes the contract setting the address provided by the deployer as the initial owner.
     */
    constructor(address initialOwner) {
        if (initialOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(initialOwner);
    }

    /**
     * @dev Throws if called by any account other than the owner.
     */
    modifier onlyOwner() {
        _checkOwner();
        _;
    }

    /**
     * @dev Returns the address of the current owner.
     */
    function owner() public view virtual returns (address) {
        return _owner;
    }

    /**
     * @dev Throws if the sender is not the owner.
     */
    function _checkOwner() internal view virtual {
        if (owner() != _msgSender()) {
            revert OwnableUnauthorizedAccount(_msgSender());
        }
    }

    /**
     * @dev Leaves the contract without owner. It will not be possible to call
     * `onlyOwner` functions. Can only be called by the current owner.
     *
     * NOTE: Renouncing ownership will leave the contract without an owner,
     * thereby disabling any functionality that is only available to the owner.
     */
    function renounceOwnership() public virtual onlyOwner {
        _transferOwnership(address(0));
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Can only be called by the current owner.
     */
    function transferOwnership(address newOwner) public virtual onlyOwner {
        if (newOwner == address(0)) {
            revert OwnableInvalidOwner(address(0));
        }
        _transferOwnership(newOwner);
    }

    /**
     * @dev Transfers ownership of the contract to a new account (`newOwner`).
     * Internal function without access restriction.
     */
    function _transferOwnership(address newOwner) internal virtual {
        address oldOwner = _owner;
        _owner = newOwner;
        emit OwnershipTransferred(oldOwner, newOwner);
    }
}

OZ के Ownable CVL स्पेसिफिकेशन्स

यहाँ Ownable कॉन्ट्रैक्ट के लिए CVL स्पेसिफिकेशन का लिंक दिया गया है: Ownable CVL Specification।

सरलता के लिए, हमने निम्नलिखित परिभाषाओं (definitions) को IOwnable.spec और helpers.spec से इंपोर्ट करने के बजाय सीधे स्पेसिफिकेशन फ़ाइल में रखकर मामूली संशोधन किए हैं:

• function owner() external returns (address) envfree (methods ब्लॉक के भीतर रखा गया)
• definition nonpayable(env e) returns bool = e.msg.value == 0

नीचे दिया गया यह संशोधित संस्करण कार्यात्मक रूप से मूल के समतुल्य है और इसका उपयोग चर्चा के लिए किया जाएगा:

Copy
methods {
    function restricted() external;
    function owner() external returns (address) envfree; // taken from the import IOwnable.spec
}


definition
 nonpayable(env e) returns bool = e.msg.value == 0; // taken from the helpers.spec

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

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

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or renounceOwnership
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

definition कीवर्ड के उपयोग पर ध्यान दें। यह पूरे स्पेसिफिकेशन में उपयोग किए जाने वाले सामान्य एक्सप्रेशन्स के लिए पुन: प्रयोज्य (reusable) लॉजिक घोषित करता है और इसे अधिकांश नियमों (rules) में लागू किया जाता है:

Copy
definition nonpayable(env e) returns bool = e.msg.value == 0;

जब बिना ईथर (Ether) भेजे कॉल की जाती है, अर्थात जब msg.value == 0 होता है, तो nonpayable(env e) true रिटर्न करता है।

यह भी उल्लेख करना उचित है कि स्पेसिफिकेशन restricted() नामक एक फ़ंक्शन को कॉल करता है, जो Ownable कॉन्ट्रैक्ट का हिस्सा नहीं है। इसके बजाय, इसे harness contract में लागू किया गया है जो एब्सट्रैक्ट कॉन्ट्रैक्ट Ownable को इनहेरिट करता है।

जब हम सत्यापन (verification) चलाते हैं, तो हम हार्नेस कॉन्ट्रैक्ट (harness contract) को सत्यापित कर रहे होते हैं। हार्नेस अक्सर इससे अधिक काम करता है, लेकिन वह एक अन्य अध्याय का विषय है। अभी के लिए, महत्वपूर्ण बात यह है कि हमने एक restricted() फ़ंक्शन जोड़ा है और onlyOwner मॉडिफायर लागू किया है।

हार्नेस कॉन्ट्रैक्ट का इम्प्लीमेंटेशन नीचे दिया गया है:

Copy
/// OwnableHarness.sol

import {Ownable} from "src/Ownable/Ownable.sol"; // import path: modify as necessary

contract OwnableHarness is Ownable {
    constructor(address initialOwner) Ownable(initialOwner) {}

    function restricted() external onlyOwner {}
}

Access Control

हम सबसे बुनियादी नियम से शुरू करते हैं: onlyCurrentOwnerCanCallOnlyOwner()। यह नियम सत्यापित करता है कि onlyOwner मॉडिफायर गैर-ओनर्स (non-owners) को प्रतिबंधित फ़ंक्शंस को कॉल करने से रोकता है:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Access control: only current owner can call restricted functions                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyCurrentOwnerCanCallOnlyOwner(env e) {
    require nonpayable(e);

    address current = owner();

    calldataarg args;
    restricted@withrevert(e, args);

    assert !lastReverted <=> e.msg.sender == current, "access control failed";
}

require nonpayable(e) लाइन का अर्थ है कि बाकी नियम का मूल्यांकन केवल उन ट्रांज़ैक्शन्स के लिए किया जाएगा जो ईथर नहीं भेजते हैं (e.msg.value == 0); अन्य सभी इनपुट्स को विश्लेषण से बाहर रखा गया है।

address current = owner() लाइन वर्तमान ओनर का एड्रेस प्राप्त करती है, जिसका उपयोग फिर असर्शन (assertion) में किया जाता है।

अब निम्नलिखित लाइनों पर विचार करें, जिन्हें थोड़ी अधिक व्याख्या की आवश्यकता है:

Copy
calldataarg args;
restricted@withrevert(e, args);

calldataarg args लाइन फ़ंक्शन कॉल restricted@withrevert(e, args) में मनमाने (arbitrary) आर्गुमेंट्स पास करती है। हालाँकि, इसे इस प्रकार सरल किया जा सकता है:

Copy
restricted@withrevert(e);

क्योंकि प्रोवर (Prover) डिफ़ॉल्ट रूप से इनपुट्स को स्वचालित रूप से मनमाने मान (arbitrary values) निर्दिष्ट करता है, जिससे इस मामले में calldataarg अनावश्यक हो जाता है (साथ ही, restricted() में कोई पैरामीटर नहीं है)। दोनों रूप मान्य हैं और स्पेसिफिकेशन लिखने वाले की पसंद को दर्शाते हैं।

अब अगला प्रश्न यह है कि क्या इसे methods ब्लॉक में शामिल किया जाना चाहिए:

Copy
methods {
    function restricted() external;
    ...
}

OpenZeppelin स्पेसिफिकेशन में इसे शामिल किया गया है। हालाँकि, ऐसा करने से एक चेतावनी (warning) उत्पन्न होती है (भले ही यह नियम सत्यापित हो):

“Method declaration for OwnableHarness.restricted() is neither envfree, optional, nor summarized, so it has no effect.”_

जैसा कि हमने अपने पिछले अध्याय में चर्चा की थी, यदि कोई फ़ंक्शन पर्यावरण-निर्भर (environment-dependent) है और उसे उसी तरह माना जाता है, तो उसे methods ब्लॉक में शामिल करने की आवश्यकता नहीं है। इस मामले में, हम methods ब्लॉक से function restricted() external लाइन को हटाकर इसे सरल बना सकते हैं।

अब अंत में, असर्शन (assertion),

Copy
assert !lastReverted <=> e.msg.sender == current, "access control failed";

इसका अर्थ है कि "कॉल केवल और केवल तभी सफल होती है जब कॉलर current एड्रेस हो"। अन्य सभी मामलों में, फ़ंक्शन को रिवर्ट (revert) होना चाहिए। बेशक, यदि फ़ंक्शन को ईथर के साथ भेजा जाता है तो यह रिवर्ट हो सकता है, लेकिन हमने require nonpayable(e) स्टेटमेंट का उपयोग करके इस नियम में उस मामले को स्पष्ट रूप से बाहर कर दिया है।

Renounce Ownership

यह नियम सत्यापित करता है कि केवल ओनर ही ओनरशिप को त्याग सकता है, और यदि यह सफल होता है, तो ओनर का एड्रेस address(0) पर सेट हो जाता है। यहाँ नियम दिया गया है:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: renounceOwnership removes the owner                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule renounceOwnership(env e) {
    require nonpayable(e);

    address current = owner();

    renounceOwnership@withrevert(e);
    bool success = !lastReverted;

    assert success <=> e.msg.sender == current, "unauthorized caller";
    assert success => owner() == 0, "owner not cleared";
}

एक नज़र में, नियम !lastReverted को success पर सेट करता है, जिसका उपयोग दोनों असर्शन्स में किया जाता है।

पहला असर्शन:

Copy
assert success <=> e.msg.sender == current, "unauthorized caller";

पिछले नियम के समान तर्क की पुष्टि करता है: “कॉल केवल और केवल तभी सफल होती है जब कॉलर वर्तमान ओनर हो”।

दूसरा असर्शन:

Copy
assert success => owner() == 0, "owner not cleared";

एक निहितार्थ (implication) है। इसका अर्थ यह है कि "यदि कॉल सफल होती है, तो ओनर को साफ़ किया जाना चाहिए (अर्थात, address(0) पर सेट किया जाना चाहिए)"। दूसरे शब्दों में, ओनरशिप को त्याग दिया जाना चाहिए।

Transfer Ownership

यह नियम सत्यापित करता है कि यदि कॉल सफल होती है, तो कॉलर वर्तमान ओनर होना चाहिए और नया एड्रेस एक वैध एड्रेस होना चाहिए (अर्थात, address(0) नहीं)।

अब हम transferOwnership() के लिए नियम देखते हैं:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Function correctness: transferOwnership changes ownership                                                           │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferOwnership(env e) {
    require nonpayable(e);

    address newOwner;
    address current = owner();

    transferOwnership@withrevert(e, newOwner);
    bool success = !lastReverted;

    assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";
    assert success => owner() == newOwner, "current owner changed";
}

पिछले नियमों की तरह, यह असर्शन,

Copy
assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg";

यह इस आधार (premise) पर आधारित है कि कॉल केवल और केवल तभी सफल होती है जब कॉलर वर्तमान ओनर हो और newOwner एक वैध (गैर-शून्य) एड्रेस हो। newOwner != 0 की शर्त आवश्यक है क्योंकि इसे हटाने से Solidity फ़ंक्शन के आंतरिक चेक (internal check) का उल्लंघन होगा और इसके परिणामस्वरूप रिवर्ट (revert) होगा (इस प्रकार एक उल्लंघन)।

Copy
/// Ownable.sol

function transferOwnership(address newOwner) public virtual onlyOwner {
    if (newOwner == address(0)) { // this line will cause a revert if newOwner is zero
        revert OwnableInvalidOwner(address(0));
    }
    _transferOwnership(newOwner);
}

अब इस नियम के अंतिम असर्शन के लिए,

Copy
assert success => owner() == newOwner, "current owner changed";

इसका अर्थ यह है कि यदि कॉल सफल होती है, तो ओनर को newOwner पर अपडेट किया जाना चाहिए।

Parametric Rules

अब जब Ownable कॉन्ट्रैक्ट की तीन प्रमुख विशेषताओं को औपचारिक रूप से सत्यापित (formally verified) किया जा चुका है, तो एक अंतिम नियम शेष है: एक पैरामीट्रिक रूल (parametric rule) जो ओनरशिप में होने वाले परिवर्तनों को सत्यापित करता है। नियम यह दावा करता है कि यदि ओनर बदलता है, तो यह इनके माध्यम से ही होना चाहिए:

• transferOwnership() जिसके परिणामस्वरूप एक गैर-शून्य (non-zero) नया ओनर बनता है या
• renounceOwnership() जिसके परिणामस्वरूप नए ओनर के रूप में एक शून्य एड्रेस (zero address) सेट होता है।

यहाँ नियम दिया गया है:

Copy
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: ownership can only change in specific ways                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e) {
    address oldCurrent = owner();

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

    address newCurrent = owner();

    // If owner changes, must be either transferOwnership or renounceOwnership
    assert oldCurrent != newCurrent => (
        (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
        (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
    );
}

यह एक पैरामीट्रिक रूल (parametric rule) है, जैसा कि f(e, args) कॉल की उपस्थिति से प्रमाणित होता है। मेथड f(e, args) कॉल के पहले और बाद की लाइनों में, हम owner() का उपयोग करके oldCurrent और newCurrent प्राप्त करते हैं। यह स्पष्ट है कि हम ओनरशिप स्टेट (ownership state) में परिवर्तनों को ट्रैक कर रहे हैं। इन दो कॉल्स के बीच f(e, args) को रखकर, हम मनमाने ढंग से फ़ंक्शन निष्पादन (arbitrary function execution) की अनुमति दे रहे हैं और यह जाँच रहे हैं कि क्या यह ओनरशिप में परिवर्तन का कारण बनता है।

अब असर्शन (assertion):

Copy
assert oldCurrent != newCurrent => (
    (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector) ||
    (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)
);

यदि ओनर बदल गया है (oldCurrent != newCurrent), तो परिवर्तन दो वैध तरीकों में से किसी एक में हुआ होना चाहिए:

- `e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == sig:transferOwnership(address).selector)`

    
इसका अर्थ है कि कॉलर वर्तमान ओनर होना चाहिए, नया ओनर शून्य एड्रेस नहीं है, और जिस फ़ंक्शन ने परिवर्तन को ट्रिगर किया वह `transferOwnership()` है।
    

- `e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == sig:renounceOwnership().selector)`

    
इसका अर्थ है कि कॉलर अभी भी वर्तमान ओनर है, लेकिन नया ओनर शून्य एड्रेस है, और उपयोग किया गया फ़ंक्शन `renounceOwnership()` होना चाहिए।

नियम के अनुसार ओनरशिप बदलने के लिए केवल ये दो ही वैध रास्ते हैं।

यह लेख Certora Prover का उपयोग करके औपचारिक सत्यापन (formal verification) पर एक श्रृंखला का हिस्सा है।