Merge branch 'master' into fv/ERC20Wrapper

OpenZeppelin · Mar 8, 2023 · fbdbddd · fbdbddd
2 parents 8c7ce2b + 5f7f660
commit fbdbddd
Show file tree

Hide file tree

Showing 11 changed files with 480 additions and 40 deletions.
diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol
@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.2;
+
+import "../patched/proxy/utils/Initializable.sol";
+
+contract InitializableHarness is Initializable {
+    function initialize()          public initializer      {}
+    function reinitialize(uint8 n) public reinitializer(n) {}
+    function disable()             public { _disableInitializers(); }
+
+    function nested_init_init()                     public initializer      { initialize();    }
+    function nested_init_reinit(uint8 m)            public initializer      { reinitialize(m); }
+    function nested_reinit_init(uint8 n)            public reinitializer(n) { initialize();    }
+    function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); }
+
+    function version() public view returns (uint8) {
+        return _getInitializedVersion();
+    }
+
+    function initializing() public view returns (bool) {
+        return _isInitializing();
+    }
+}
diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable2Step.sol";
+
+contract Ownable2StepHarness is Ownable2Step {
+  function restricted() external onlyOwner {}
+}
diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol
@@ -0,0 +1,9 @@
+// SPDX-License-Identifier: MIT
+
+pragma solidity ^0.8.0;
+
+import "../patched/access/Ownable.sol";
+
+contract OwnableHarness is Ownable {
+  function restricted() external onlyOwner {}
+}
diff --git a/certora/run.js b/certora/run.js
@@ -8,7 +8,7 @@
 
 const MAX_PARALLEL = 4;
 
-const specs = require(__dirname + '/specs.json');
+let specs = require(__dirname + '/specs.json');
 
 const proc = require('child_process');
 const { PassThrough } = require('stream');
@@ -20,14 +20,20 @@ if (request.startsWith('-')) {
   extraOptions.unshift(request);
   request = '';
 }
-const [reqSpec, reqContract] = request.split(':').reverse();
 
-for (const { spec, contract, files, options = [] } of Object.values(specs)) {
-  if ((!reqSpec || reqSpec === spec) && (!reqContract || reqContract === contract)) {
-    limit(runCertora, spec, contract, files, [...options.flatMap(opt => opt.split(' ')), ...extraOptions]);
+if (request) {
+  const [reqSpec, reqContract] = request.split(':').reverse();
+  specs = Object.values(specs).filter(s => reqSpec === s.spec && (!reqContract || reqContract === s.contract));
+  if (specs.length === 0) {
+    console.error(`Error: Requested spec '${request}' not found in specs.json`);
+    process.exit(1);
   }
 }
 
+for (const { spec, contract, files, options = [] } of Object.values(specs)) {
+  limit(runCertora, spec, contract, files, [...options.split(' '), ...extraOptions]);
+}
+
 // Run certora, aggregate the output and print it at the end
 async function runCertora(spec, contract, files, options = []) {
   const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options];

diff --git a/certora/specs.json b/certora/specs.json
@@ -4,6 +4,16 @@
     "contract": "AccessControlHarness",
     "files": ["certora/harnesses/AccessControlHarness.sol"]
   },
+  {
+    "spec": "Ownable",
+    "contract": "OwnableHarness",
+    "files": ["certora/harnesses/OwnableHarness.sol"]
+  },
+  {
+    "spec": "Ownable2Step",
+    "contract": "Ownable2StepHarness",
+    "files": ["certora/harnesses/Ownable2StepHarness.sol"]
+  },
   {
     "spec": "ERC20",
     "contract": "ERC20PermitHarness",
@@ -30,5 +40,10 @@
       "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness",
       "--optimistic_loop"
     ]
+  },
+  {
+    "spec": "Initializable",
+    "contract": "InitializableHarness",
+    "files": ["certora/harnesses/InitializableHarness.sol"]
   }
 ]
diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec
@@ -44,22 +44,27 @@ rule onlyGrantCanGrant(env e, bytes32 role, address account) {
 rule grantRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    grantRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    grantRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == true && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -70,22 +75,27 @@ rule grantRoleEffect(env e) {
 rule revokeRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool isCallerAdmin = hasRole(getRoleAdmin(role2), e.msg.sender);
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    revokeRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> isCallerAdmin;
+    revokeRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> isCallerAdmin;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
 
 /*
@@ -96,19 +106,24 @@ rule revokeRoleEffect(env e) {
 rule renounceRoleEffect(env e) {
     require nonpayable(e);
 
-    bytes32 role1; bytes32 role2;
-    address account1; address account2;
+    bytes32 role;
+    bytes32 otherRole;
+    address account;
+    address otherAccount;
 
-    bool hasRoleBefore = hasRole(role1, account1);
+    bool hasOtherRoleBefore = hasRole(otherRole, otherAccount);
 
-    renounceRole@withrevert(e, role2, account2);
-    assert !lastReverted <=> account2 == e.msg.sender;
+    renounceRole@withrevert(e, role, account);
+    bool success = !lastReverted;
 
-    bool hasRoleAfter = hasRole(role1, account1);
+    bool hasOtherRoleAfter = hasRole(otherRole, otherAccount);
 
-    assert (
-        hasRoleBefore != hasRoleAfter
-    ) => (
-        hasRoleAfter == false && role1 == role2 && account1 == account2
-    );
+    // liveness
+    assert success <=> account == e.msg.sender;
+
+    // effect
+    assert success => !hasRole(role, account);
+
+    // no side effect
+    assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount);
 }
diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec
@@ -0,0 +1,165 @@
+import "helpers.spec"
+
+methods {
+    // initialize, reinitialize, disable
+    initialize()        envfree
+    reinitialize(uint8) envfree
+    disable()           envfree
+
+    nested_init_init()            envfree
+    nested_init_reinit(uint8)       envfree
+    nested_reinit_init(uint8)       envfree
+    nested_reinit_reinit(uint8,uint8) envfree
+
+    // view
+    version()      returns uint8 envfree
+    initializing() returns bool  envfree
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Definitions                                                                                                         │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+definition isUninitialized() returns bool = version() == 0;
+definition isInitialized()   returns bool = version() > 0;
+definition isDisabled()      returns bool = version() == 255;
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution.    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+invariant notInitializing()
+    !initializing()
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: The version cannot decrease & disable state is irrevocable.                                                   │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule increasingVersion(env e) {
+    uint8 versionBefore = version();
+    bool disabledBefore = isDisabled();
+
+    method f; calldataarg args;
+    f(e, args);
+
+    assert versionBefore <= version(), "_initialized must only increase";
+    assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize a contract that is already initialized.                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeTwice() {
+    require isInitialized();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract must only be initialized once";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot initialize once disabled.                                                                              │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotInitializeOnceDisabled() {
+    require isDisabled();
+
+    initialize@withrevert();
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot reinitialize once disabled.                                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotReinitializeOnceDisabled() {
+    require isDisabled();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+
+    assert lastReverted, "contract is disabled";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Cannot nest initializers (after construction).                                                                │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule cannotNestInitializers_init_init() {
+    nested_init_init@withrevert();
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_init_reinit(uint8 m) {
+    nested_init_reinit@withrevert(m);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_init(uint8 n) {
+    nested_reinit_init@withrevert(n);
+    assert lastReverted, "nested initializers";
+}
+
+rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) {
+    nested_reinit_reinit@withrevert(n, m);
+    assert lastReverted, "nested initializers";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Initialize correctly sets the version.                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+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";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Reinitialize correctly sets the version.                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule reinitializeEffects() {
+    requireInvariant notInitializing();
+
+    uint8 versionBefore = version();
+
+    uint8 n;
+    reinitialize@withrevert(n);
+    bool success = !lastReverted;
+
+    assert success <=> versionBefore < n, "can only reinitialize to a latter versions";
+    assert success => version() == n,     "reinitialize must set version() to n";
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Rule: Can disable.                                                                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule disableEffect() {
+    requireInvariant notInitializing();
+
+    disable@withrevert();
+    bool success = !lastReverted;
+
+    assert success,      "call to _disableInitializers failed";
+    assert isDisabled(), "disable state not set";
+}