diff --git a/certora/diff/access_AccessControl.sol.patch b/certora/diff/access_AccessControl.sol.patch new file mode 100644 index 000000000..c11474a50 --- /dev/null +++ b/certora/diff/access_AccessControl.sol.patch @@ -0,0 +1,11 @@ +--- access/AccessControl.sol 2023-08-10 22:02:18 ++++ access/AccessControl.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.9.0) (access/AccessControl.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {IAccessControl} from "./IAccessControl.sol"; + import {Context} from "../utils/Context.sol"; diff --git a/certora/diff/access_IAccessControl.sol.patch b/certora/diff/access_IAccessControl.sol.patch new file mode 100644 index 000000000..979939693 --- /dev/null +++ b/certora/diff/access_IAccessControl.sol.patch @@ -0,0 +1,11 @@ +--- access/IAccessControl.sol 2023-08-10 22:02:20 ++++ access/IAccessControl.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts v4.4.1 (access/IAccessControl.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev External interface of AccessControl declared to support ERC165 detection. diff --git a/certora/diff/security_Pausable.sol.patch b/certora/diff/security_Pausable.sol.patch new file mode 100644 index 000000000..7bc32deaa --- /dev/null +++ b/certora/diff/security_Pausable.sol.patch @@ -0,0 +1,11 @@ +--- security/Pausable.sol 2023-08-10 21:54:54 ++++ security/Pausable.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts (last updated v4.7.0) (security/Pausable.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {Context} from "../utils/Context.sol"; + diff --git a/certora/diff/token_ERC721_ERC721.sol.patch b/certora/diff/token_ERC721_ERC721.sol.patch index c3eae357a..d29518304 100644 --- a/certora/diff/token_ERC721_ERC721.sol.patch +++ b/certora/diff/token_ERC721_ERC721.sol.patch @@ -1,6 +1,6 @@ ---- token/ERC721/ERC721.sol 2023-03-07 10:48:47.736822221 +0100 -+++ token/ERC721/ERC721.sol 2023-03-09 19:49:39.669338673 +0100 -@@ -199,6 +199,11 @@ +--- token/ERC721/ERC721.sol 2023-08-10 16:45:36 ++++ token/ERC721/ERC721.sol 2023-08-10 22:11:07 +@@ -208,6 +208,11 @@ return _owners[tokenId]; } diff --git a/certora/diff/utils_Context.sol.patch b/certora/diff/utils_Context.sol.patch new file mode 100644 index 000000000..f458c6d6e --- /dev/null +++ b/certora/diff/utils_Context.sol.patch @@ -0,0 +1,11 @@ +--- utils/Context.sol 2023-08-10 21:54:56 ++++ utils/Context.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts v4.4.1 (utils/Context.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Provides information about the current execution context, including the diff --git a/certora/diff/utils_introspection_ERC165.sol.patch b/certora/diff/utils_introspection_ERC165.sol.patch new file mode 100644 index 000000000..d0ec74e92 --- /dev/null +++ b/certora/diff/utils_introspection_ERC165.sol.patch @@ -0,0 +1,11 @@ +--- utils/introspection/ERC165.sol 2023-08-10 22:02:24 ++++ utils/introspection/ERC165.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts v4.4.1 (utils/introspection/ERC165.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + import {IERC165} from "./IERC165.sol"; + diff --git a/certora/diff/utils_introspection_IERC165.sol.patch b/certora/diff/utils_introspection_IERC165.sol.patch new file mode 100644 index 000000000..b100b173e --- /dev/null +++ b/certora/diff/utils_introspection_IERC165.sol.patch @@ -0,0 +1,11 @@ +--- utils/introspection/IERC165.sol 2023-08-09 11:45:05 ++++ utils/introspection/IERC165.sol 2023-08-10 22:11:07 +@@ -1,7 +1,7 @@ + // SPDX-License-Identifier: MIT + // OpenZeppelin Contracts v4.4.1 (utils/introspection/IERC165.sol) + +-pragma solidity ^0.8.20; ++pragma solidity ^0.8.19; + + /** + * @dev Interface of the ERC165 standard, as defined in the diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol index 42a536af1..f34532fab 100644 --- a/certora/harnesses/AccessControlHarness.sol +++ b/certora/harnesses/AccessControlHarness.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.20; +pragma solidity ^0.8.19; -import "../patched/access/AccessControl.sol"; +import {AccessControl} from "../patched/access/AccessControl.sol"; contract AccessControlHarness is AccessControl {} diff --git a/certora/harnesses/PausableHarness.sol b/certora/harnesses/PausableHarness.sol index b9c15cf54..8663db15c 100644 --- a/certora/harnesses/PausableHarness.sol +++ b/certora/harnesses/PausableHarness.sol @@ -1,8 +1,8 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.20; +pragma solidity ^0.8.19; -import "../patched/security/Pausable.sol"; +import {Pausable} from "../patched/security/Pausable.sol"; contract PausableHarness is Pausable { function pause() external { diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index cd5af2a99..70b067218 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -1,126 +1,119 @@ -import "helpers/helpers.spec" -import "methods/IAccessControl.spec" - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Definitions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -definition DEFAULT_ADMIN_ROLE() returns bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000; - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) { - calldataarg args; - - bool hasRoleBefore = hasRole(role, account); - f(e, args); - bool hasRoleAfter = hasRole(role, account); - - assert ( - !hasRoleBefore && - hasRoleAfter - ) => ( - f.selector == grantRole(bytes32, address).selector - ); - - assert ( - hasRoleBefore && - !hasRoleAfter - ) => ( - f.selector == revokeRole(bytes32, address).selector || - f.selector == renounceRole(bytes32, address).selector - ); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: grantRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule grantRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - grantRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> isCallerAdmin; - - // effect - assert success => hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: revokeRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule revokeRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - revokeRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> isCallerAdmin; - - // effect - assert success => !hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: renounceRole only affects the specified user/role combo │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule renounceRoleEffect(env e, bytes32 role) { - require nonpayable(e); - - bytes32 otherRole; - address account; - address otherAccount; - - bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); - - renounceRole@withrevert(e, role, account); - bool success = !lastReverted; - - bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); - - // liveness - assert success <=> account == e.msg.sender; - - // effect - assert success => !hasRole(role, account); - - // no side effect - assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); -} +import "helpers/helpers.spec"; +import "methods/IAccessControl.spec"; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Identify entrypoints: only grantRole, revokeRole and renounceRole can alter permissions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyGrantCanGrant(env e, method f, bytes32 role, address account) { + calldataarg args; + + bool hasRoleBefore = hasRole(role, account); + f(e, args); + bool hasRoleAfter = hasRole(role, account); + + assert ( + !hasRoleBefore && + hasRoleAfter + ) => ( + f.selector == sig:grantRole(bytes32, address).selector + ); + + assert ( + hasRoleBefore && + !hasRoleAfter + ) => ( + f.selector == sig:revokeRole(bytes32, address).selector || + f.selector == sig:renounceRole(bytes32, address).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: grantRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule grantRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + grantRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: revokeRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule revokeRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool isCallerAdmin = hasRole(getRoleAdmin(role), e.msg.sender); + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + revokeRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // liveness + assert success <=> isCallerAdmin; + + // effect + assert success => !hasRole(role, account); + + // no side effect + assert hasOtherRoleBefore != hasOtherRoleAfter => (role == otherRole && account == otherAccount); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceRoleEffect(env e, bytes32 role) { + require nonpayable(e); + + bytes32 otherRole; + address account; + address otherAccount; + + bool hasOtherRoleBefore = hasRole(otherRole, otherAccount); + + renounceRole@withrevert(e, role, account); + bool success = !lastReverted; + + bool hasOtherRoleAfter = hasRole(otherRole, otherAccount); + + // 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/Pausable.spec b/certora/specs/Pausable.spec index aea38003f..a7aff9cc1 100644 --- a/certora/specs/Pausable.spec +++ b/certora/specs/Pausable.spec @@ -1,96 +1,96 @@ -import "helpers/helpers.spec" - -methods { - paused() returns (bool) envfree - pause() - unpause() - onlyWhenPaused() - onlyWhenNotPaused() -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: _pause pauses the contract │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule pause(env e) { - require nonpayable(e); - - bool pausedBefore = paused(); - - pause@withrevert(e); - bool success = !lastReverted; - - bool pausedAfter = paused(); - - // liveness - assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; - - // effect - assert success => pausedAfter, "contract must be paused after a successful call"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: _unpause unpauses the contract │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule unpause(env e) { - require nonpayable(e); - - bool pausedBefore = paused(); - - unpause@withrevert(e); - bool success = !lastReverted; - - bool pausedAfter = paused(); - - // liveness - assert success <=> pausedBefore, "works if and only if the contract was paused before"; - - // effect - assert success => !pausedAfter, "contract must be unpaused after a successful call"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: whenPaused modifier can only be called if the contract is paused │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule whenPaused(env e) { - require nonpayable(e); - - onlyWhenPaused@withrevert(e); - assert !lastReverted <=> paused(), "works if and only if the contract is paused"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule whenNotPaused(env e) { - require nonpayable(e); - - onlyWhenNotPaused@withrevert(e); - assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; -} - -/* -┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ -│ Rules: only _pause and _unpause can change paused status │ -└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ -*/ -rule noPauseChange(env e) { - method f; - calldataarg args; - - bool pausedBefore = paused(); - f(e, args); - bool pausedAfter = paused(); - - assert pausedBefore != pausedAfter => ( - (!pausedAfter && f.selector == unpause().selector) || - (pausedAfter && f.selector == pause().selector) - ), "contract's paused status can only be changed by _pause() or _unpause()"; -} +import "helpers/helpers.spec"; + +methods { + function paused() external returns (bool) envfree; + function pause() external; + function unpause() external; + function onlyWhenPaused() external; + function onlyWhenNotPaused() external; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _pause pauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule pause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + pause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> !pausedBefore, "works if and only if the contract was not paused before"; + + // effect + assert success => pausedAfter, "contract must be paused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: _unpause unpauses the contract │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule unpause(env e) { + require nonpayable(e); + + bool pausedBefore = paused(); + + unpause@withrevert(e); + bool success = !lastReverted; + + bool pausedAfter = paused(); + + // liveness + assert success <=> pausedBefore, "works if and only if the contract was paused before"; + + // effect + assert success => !pausedAfter, "contract must be unpaused after a successful call"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenPaused modifier can only be called if the contract is paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenPaused(env e) { + require nonpayable(e); + + onlyWhenPaused@withrevert(e); + assert !lastReverted <=> paused(), "works if and only if the contract is paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: whenNotPaused modifier can only be called if the contract is not paused │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule whenNotPaused(env e) { + require nonpayable(e); + + onlyWhenNotPaused@withrevert(e); + assert !lastReverted <=> !paused(), "works if and only if the contract is not paused"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rules: only _pause and _unpause can change paused status │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noPauseChange(env e) { + method f; + calldataarg args; + + bool pausedBefore = paused(); + f(e, args); + bool pausedAfter = paused(); + + assert pausedBefore != pausedAfter => ( + (!pausedAfter && f.selector == sig:unpause().selector) || + (pausedAfter && f.selector == sig:pause().selector) + ), "contract's paused status can only be changed by _pause() or _unpause()"; +} diff --git a/certora/specs/methods/IAccessControl.spec b/certora/specs/methods/IAccessControl.spec index 4d41ffda7..c75e4ef2d 100644 --- a/certora/specs/methods/IAccessControl.spec +++ b/certora/specs/methods/IAccessControl.spec @@ -1,7 +1,7 @@ methods { - hasRole(bytes32, address) returns(bool) envfree - getRoleAdmin(bytes32) returns(bytes32) envfree - grantRole(bytes32, address) - revokeRole(bytes32, address) - renounceRole(bytes32, address) + function hasRole(bytes32, address) external returns(bool) envfree; + function getRoleAdmin(bytes32) external returns(bytes32) envfree; + function grantRole(bytes32, address) external; + function revokeRole(bytes32, address) external; + function renounceRole(bytes32, address) external; }