diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index b073cad96..77ba42667 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,18 +1,6 @@ -diff -druN access/AccessControl.sol access/AccessControl.sol ---- access/AccessControl.sol 2023-02-27 10:59:32.652558153 +0100 -+++ access/AccessControl.sol 2023-02-27 11:58:55.064499723 +0100 -@@ -94,7 +94,7 @@ - * - * _Available since v4.6._ - */ -- function _checkRole(bytes32 role) internal view virtual { -+ function _checkRole(bytes32 role) public view virtual { // HARNESS: internal -> public - _checkRole(role, _msgSender()); - } - diff -druN governance/extensions/GovernorCountingSimple.sol governance/extensions/GovernorCountingSimple.sol --- governance/extensions/GovernorCountingSimple.sol 2023-02-27 10:59:32.652558153 +0100 -+++ governance/extensions/GovernorCountingSimple.sol 2023-02-27 11:58:55.064499723 +0100 ++++ governance/extensions/GovernorCountingSimple.sol 2023-02-28 16:49:10.417726143 +0100 @@ -27,7 +27,7 @@ mapping(address => bool) hasVoted; } @@ -24,7 +12,7 @@ diff -druN governance/extensions/GovernorCountingSimple.sol governance/extension * @dev See {IGovernor-COUNTING_MODE}. diff -druN governance/extensions/GovernorPreventLateQuorum.sol governance/extensions/GovernorPreventLateQuorum.sol --- governance/extensions/GovernorPreventLateQuorum.sol 2023-02-27 10:59:32.652558153 +0100 -+++ governance/extensions/GovernorPreventLateQuorum.sol 2023-02-27 11:58:55.064499723 +0100 ++++ governance/extensions/GovernorPreventLateQuorum.sol 2023-02-28 16:49:10.417726143 +0100 @@ -20,10 +20,10 @@ abstract contract GovernorPreventLateQuorum is Governor { using SafeCast for uint256; @@ -40,7 +28,7 @@ diff -druN governance/extensions/GovernorPreventLateQuorum.sol governance/extens event ProposalExtended(uint256 indexed proposalId, uint64 extendedDeadline); diff -druN governance/extensions/GovernorVotesQuorumFraction.sol governance/extensions/GovernorVotesQuorumFraction.sol --- governance/extensions/GovernorVotesQuorumFraction.sol 2023-02-27 10:59:32.655891529 +0100 -+++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-02-27 11:58:55.064499723 +0100 ++++ governance/extensions/GovernorVotesQuorumFraction.sol 2023-02-28 16:49:10.417726143 +0100 @@ -17,10 +17,10 @@ using SafeCast for *; using Checkpoints for Checkpoints.Trace224; @@ -56,7 +44,7 @@ diff -druN governance/extensions/GovernorVotesQuorumFraction.sol governance/exte diff -druN governance/Governor.sol governance/Governor.sol --- governance/Governor.sol 2023-02-27 10:59:32.652558153 +0100 -+++ governance/Governor.sol 2023-02-27 11:58:55.064499723 +0100 ++++ governance/Governor.sol 2023-02-28 16:49:10.421059488 +0100 @@ -51,7 +51,7 @@ string private _name; @@ -68,7 +56,7 @@ diff -druN governance/Governor.sol governance/Governor.sol // {onlyGovernance} modifier needs to be whitelisted in this queue. Whitelisting is set in {_beforeExecute}, diff -druN governance/TimelockController.sol governance/TimelockController.sol --- governance/TimelockController.sol 2023-02-27 10:59:32.652558153 +0100 -+++ governance/TimelockController.sol 2023-02-27 11:58:55.067833070 +0100 ++++ governance/TimelockController.sol 2023-02-28 16:49:10.421059488 +0100 @@ -28,10 +28,10 @@ bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); @@ -84,7 +72,7 @@ diff -druN governance/TimelockController.sol governance/TimelockController.sol * @dev Emitted when a call is scheduled as part of operation `id`. diff -druN governance/utils/Votes.sol governance/utils/Votes.sol --- governance/utils/Votes.sol 2023-02-27 10:59:32.655891529 +0100 -+++ governance/utils/Votes.sol 2023-02-27 13:56:39.610815192 +0100 ++++ governance/utils/Votes.sol 2023-02-28 16:49:10.421059488 +0100 @@ -35,7 +35,25 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -121,7 +109,7 @@ diff -druN governance/utils/Votes.sol governance/utils/Votes.sol } diff -druN proxy/utils/Initializable.sol proxy/utils/Initializable.sol --- proxy/utils/Initializable.sol 2023-02-27 10:59:32.655891529 +0100 -+++ proxy/utils/Initializable.sol 2023-02-27 11:58:55.067833070 +0100 ++++ proxy/utils/Initializable.sol 2023-02-28 16:49:10.421059488 +0100 @@ -60,12 +60,12 @@ * @dev Indicates that the contract has been initialized. * @custom:oz-retyped-from bool @@ -139,7 +127,7 @@ diff -druN proxy/utils/Initializable.sol proxy/utils/Initializable.sol * @dev Triggered when the contract has been initialized or reinitialized. diff -druN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol --- token/ERC1155/ERC1155.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC1155/ERC1155.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC1155/ERC1155.sol 2023-02-28 16:49:10.421059488 +0100 @@ -21,7 +21,7 @@ using Address for address; @@ -169,7 +157,7 @@ diff -druN token/ERC1155/ERC1155.sol token/ERC1155/ERC1155.sol bytes4 response diff -druN token/ERC20/ERC20.sol token/ERC20/ERC20.sol --- token/ERC20/ERC20.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC20/ERC20.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC20/ERC20.sol 2023-02-28 16:49:10.421059488 +0100 @@ -248,7 +248,7 @@ * * - `account` cannot be the zero address. @@ -190,7 +178,7 @@ diff -druN token/ERC20/ERC20.sol token/ERC20/ERC20.sol _beforeTokenTransfer(account, address(0), amount); diff -druN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Capped.sol --- token/ERC20/extensions/ERC20Capped.sol 2023-02-22 15:43:36.624717708 +0100 -+++ token/ERC20/extensions/ERC20Capped.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC20/extensions/ERC20Capped.sol 2023-02-28 16:49:10.421059488 +0100 @@ -30,7 +30,7 @@ /** * @dev See {ERC20-_mint}. @@ -202,7 +190,7 @@ diff -druN token/ERC20/extensions/ERC20Capped.sol token/ERC20/extensions/ERC20Ca } diff -druN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC20FlashMint.sol --- token/ERC20/extensions/ERC20FlashMint.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC20/extensions/ERC20FlashMint.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC20/extensions/ERC20FlashMint.sol 2023-02-28 16:49:10.421059488 +0100 @@ -53,9 +53,11 @@ // silence warning about unused variable without the addition of bytecode. token; @@ -218,7 +206,7 @@ diff -druN token/ERC20/extensions/ERC20FlashMint.sol token/ERC20/extensions/ERC2 * implementation returns the address(0) which means the fee amount will be burnt. diff -druN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Votes.sol --- token/ERC20/extensions/ERC20Votes.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC20/extensions/ERC20Votes.sol 2023-02-27 11:58:57.244508616 +0100 ++++ token/ERC20/extensions/ERC20Votes.sol 2023-02-28 16:49:10.421059488 +0100 @@ -33,8 +33,8 @@ bytes32 private constant _DELEGATION_TYPEHASH = keccak256("Delegation(address delegatee,uint256 nonce,uint256 expiry)"); @@ -351,7 +339,7 @@ diff -druN token/ERC20/extensions/ERC20Votes.sol token/ERC20/extensions/ERC20Vot diff -druN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20Wrapper.sol --- token/ERC20/extensions/ERC20Wrapper.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC20/extensions/ERC20Wrapper.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC20/extensions/ERC20Wrapper.sol 2023-02-28 16:49:10.421059488 +0100 @@ -62,7 +62,7 @@ * @dev Mint wrapped token to cover any underlyingTokens that would have been transferred by mistake. Internal * function that can be exposed with access control if desired. @@ -363,7 +351,7 @@ diff -druN token/ERC20/extensions/ERC20Wrapper.sol token/ERC20/extensions/ERC20W return value; diff -druN token/ERC721/extensions/ERC721Votes.sol token/ERC721/extensions/ERC721Votes.sol --- token/ERC721/extensions/ERC721Votes.sol 2023-02-27 10:59:32.655891529 +0100 -+++ token/ERC721/extensions/ERC721Votes.sol 2023-02-27 11:58:55.067833070 +0100 ++++ token/ERC721/extensions/ERC721Votes.sol 2023-02-28 16:49:10.421059488 +0100 @@ -35,7 +35,7 @@ /** * @dev Returns the balance of `account`. @@ -375,7 +363,7 @@ diff -druN token/ERC721/extensions/ERC721Votes.sol token/ERC721/extensions/ERC72 } diff -druN utils/Address.sol utils/Address.sol --- utils/Address.sol 2023-02-27 10:59:32.659224903 +0100 -+++ utils/Address.sol 2023-02-27 11:58:55.067833070 +0100 ++++ utils/Address.sol 2023-02-28 16:49:10.421059488 +0100 @@ -197,7 +197,7 @@ bool success, bytes memory returndata, @@ -396,7 +384,7 @@ diff -druN utils/Address.sol utils/Address.sol } else { diff -druN utils/Checkpoints.sol utils/Checkpoints.sol --- utils/Checkpoints.sol 2023-02-27 10:59:32.659224903 +0100 -+++ utils/Checkpoints.sol 2023-02-27 11:58:55.071166417 +0100 ++++ utils/Checkpoints.sol 2023-02-28 16:49:10.424392833 +0100 @@ -84,13 +84,13 @@ * * Returns previous value and new value. diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index b57ce3113..69d805e16 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -1,85 +1,133 @@ methods { + hasRole(bytes32, address) returns(bool) envfree + getRoleAdmin(bytes32) returns(bytes32) envfree + grantRole(bytes32, address) revokeRole(bytes32, address) - _checkRole(bytes32) - safeTransferFrom(address, address, uint256, uint256, bytes) - safeBatchTransferFrom(address, address, uint256[], uint256[], bytes) - - getRoleAdmin(bytes32) returns(bytes32) envfree - hasRole(bytes32, address) returns(bool) envfree -} + renounceRole(bytes32, address) +} -// STATUS - verified -// If `onlyRole` modifier reverts then `grantRole()` reverts -rule onlyRoleModifierCheckGrant(env e){ - bytes32 role; address account; +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: only grantRole can grant a role │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyGrantCanGrant(env e, bytes32 role, address account) { + require !hasRole(role, account); - _checkRole@withrevert(e, getRoleAdmin(role)); - bool checkRevert = lastReverted; + method f; calldataarg args; + f(e, args); + + assert hasRole(role, account) => f.selector == grantRole(bytes32, address).selector; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: only revokeRole and renounceRole can grant a role │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyRevokeAndRenounceCanRevoke(env e, bytes32 role, address account) { + require hasRole(role, account); + + method f; calldataarg args; + f(e, args); + + assert !hasRole(role, account) => (f.selector == revokeRole(bytes32, address).selector || f.selector == renounceRole(bytes32, address).selector); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: only an account with admin role can call grantRole │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyAdminCanGrant(env e, bytes32 role, address account) { + bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender); grantRole@withrevert(e, role, account); - bool grantRevert = lastReverted; - assert checkRevert => grantRevert, "modifier goes bananas"; + assert !lastReverted => isAdmin; } - -// STATUS - verified -// check onlyRole modifier for revokeRole() -rule onlyRoleModifierCheckRevoke(env e){ - bytes32 role; address account; - - _checkRole@withrevert(e, getRoleAdmin(role)); - bool checkRevert = lastReverted; +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: only an account with admin role can call revokeRole │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyAdminCanRevoke(env e, bytes32 role, address account) { + bool isAdmin = hasRole(getRoleAdmin(role), e.msg.sender); revokeRole@withrevert(e, role, account); - bool revokeRevert = lastReverted; - assert checkRevert => revokeRevert, "modifier goes bananas"; + assert !lastReverted => isAdmin; } - -// STATUS - verified -// grantRole() does not affect another accounts -rule grantRoleEffect(env e){ - bytes32 role; address account; - bytes32 anotherRole; address nonEffectedAcc; - require account != nonEffectedAcc; - - bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc); - - grantRole(e, role, account); - - bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc); - - assert hasRoleBefore == hasRoleAfter, "modifier goes bananas"; +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: only the affected account can revoke │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyUserCanRenounce(env e, bytes32 role, address account) { + renounceRole@withrevert(e, role, account); + assert !lastReverted => account == e.msg.sender; } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: grantRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule grantRoleEffect(env e) { + bytes32 role1; bytes32 role2; + address account1; address account2; -// STATUS - verified -// revokeRole() does not affect another accounts -rule revokeRoleEffect(env e){ - bytes32 role; address account; - bytes32 anotherRole; address nonEffectedAcc; - require account != nonEffectedAcc; + bool hasRoleBefore = hasRole(role1, account1); + grantRole(e, role2, account2); + bool hasRoleAfter = hasRole(role1, account1); - bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc); - - revokeRole(e, role, account); - - bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc); - - assert hasRoleBefore == hasRoleAfter, "modifier goes bananas"; + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == true && role1 == role2 && account1 == account2 + ); } +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: revokeRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule revokeRoleEffect(env e) { + bytes32 role1; bytes32 role2; + address account1; address account2; + bool hasRoleBefore = hasRole(role1, account1); + revokeRole(e, role2, account2); + bool hasRoleAfter = hasRole(role1, account1); + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == false && role1 == role2 && account1 == account2 + ); +} +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: renounceRole only affects the specified user/role combo │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceRoleEffect(env e) { + bytes32 role1; bytes32 role2; + address account1; address account2; + bool hasRoleBefore = hasRole(role1, account1); + renounceRole(e, role2, account2); + bool hasRoleAfter = hasRole(role1, account1); - - - - - + assert ( + hasRoleBefore != hasRoleAfter + ) => ( + hasRoleAfter == false && role1 == role2 && account1 == account2 + ); +} \ No newline at end of file