From aca4030e4a9b3b6585669bcdfac8518a18c2ec47 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 4 Oct 2023 21:17:15 +0200 Subject: [PATCH] Formal verification of AccessManager (#4611) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Ernesto García Co-authored-by: Francisco Giordano --- certora/Makefile | 4 +- .../access_manager_AccessManager.sol.patch | 98 +++ certora/harnesses/AccessManagedHarness.sol | 36 + certora/harnesses/AccessManagerHarness.sol | 116 +++ certora/specs.json | 19 + certora/specs/AccessManaged.spec | 34 + certora/specs/AccessManager.spec | 826 ++++++++++++++++++ certora/specs/helpers/helpers.spec | 5 + certora/specs/methods/IAccessManaged.spec | 5 + certora/specs/methods/IAccessManager.spec | 33 + contracts/access/manager/AccessManager.sol | 4 +- requirements.txt | 2 +- 12 files changed, 1177 insertions(+), 5 deletions(-) create mode 100644 certora/diff/access_manager_AccessManager.sol.patch create mode 100644 certora/harnesses/AccessManagedHarness.sol create mode 100644 certora/harnesses/AccessManagerHarness.sol create mode 100644 certora/specs/AccessManaged.spec create mode 100644 certora/specs/AccessManager.spec create mode 100644 certora/specs/methods/IAccessManaged.spec create mode 100644 certora/specs/methods/IAccessManager.spec diff --git a/certora/Makefile b/certora/Makefile index 50fd6da082f..d57d2ffdc73 100644 --- a/certora/Makefile +++ b/certora/Makefile @@ -17,7 +17,7 @@ $(DST): FORCE @cp -r $(SRC) $@ # Update a solidity file in the $DST directory using the corresponding patch -$(DST)/%.sol: FORCE +$(DST)/%.sol: FORCE | $(DST) @echo Applying patch to $@ @patch -p0 -d $(DST) < $(patsubst $(DST)_%,$(DIFF)/%.patch,$(subst /,_,$@)) @@ -31,7 +31,7 @@ $(DIFF): FORCE @mkdir $@ # Create the patch file by comparing the source and the destination -$(DIFF)/%.patch: FORCE +$(DIFF)/%.patch: FORCE | $(DIFF) @echo Generating patch $@ @diff -ruN \ $(patsubst $(DIFF)/%.patch,$(SRC)/%,$(subst _,/,$@)) \ diff --git a/certora/diff/access_manager_AccessManager.sol.patch b/certora/diff/access_manager_AccessManager.sol.patch new file mode 100644 index 00000000000..8a9232bc737 --- /dev/null +++ b/certora/diff/access_manager_AccessManager.sol.patch @@ -0,0 +1,98 @@ +--- access/manager/AccessManager.sol 2023-10-04 11:20:52.802378968 +0200 ++++ access/manager/AccessManager.sol 2023-10-04 14:49:43.126279234 +0200 +@@ -6,7 +6,6 @@ + import {IAccessManaged} from "./IAccessManaged.sol"; + import {Address} from "../../utils/Address.sol"; + import {Context} from "../../utils/Context.sol"; +-import {Multicall} from "../../utils/Multicall.sol"; + import {Math} from "../../utils/math/Math.sol"; + import {Time} from "../../utils/types/Time.sol"; + +@@ -48,7 +47,8 @@ + * mindful of the danger associated with functions such as {{Ownable-renounceOwnership}} or + * {{AccessControl-renounceRole}}. + */ +-contract AccessManager is Context, Multicall, IAccessManager { ++// NOTE: The FV version of this contract doesn't include Multicall because CVL HAVOCs on any `delegatecall`. ++contract AccessManager is Context, IAccessManager { + using Time for *; + + // Structure that stores the details for a target contract. +@@ -93,7 +93,7 @@ + mapping(bytes32 operationId => Schedule) private _schedules; + + // This should be transient storage when supported by the EVM. +- bytes32 private _executionId; ++ bytes32 internal _executionId; // private → internal for FV + + /** + * @dev Check that the caller is authorized to perform the operation, following the restrictions encoded in +@@ -185,6 +185,11 @@ + return _targets[target].adminDelay.get(); + } + ++ // Exposed for FV ++ function _getTargetAdminDelayFull(address target) internal view virtual returns (uint32, uint32, uint48) { ++ return _targets[target].adminDelay.getFull(); ++ } ++ + /** + * @dev Get the id of the role that acts as an admin for given role. + * +@@ -213,6 +218,11 @@ + return _roles[roleId].grantDelay.get(); + } + ++ // Exposed for FV ++ function _getRoleGrantDelayFull(uint64 roleId) internal view virtual returns (uint32, uint32, uint48) { ++ return _roles[roleId].grantDelay.getFull(); ++ } ++ + /** + * @dev Get the access details for a given account for a given role. These details include the timepoint at which + * membership becomes active, and the delay applied to all operation by this user that requires this permission +@@ -749,7 +759,7 @@ + /** + * @dev Hashing function for execute protection + */ +- function _hashExecutionId(address target, bytes4 selector) private pure returns (bytes32) { ++ function _hashExecutionId(address target, bytes4 selector) internal pure returns (bytes32) { // private → internal for FV + return keccak256(abi.encode(target, selector)); + } + +@@ -769,7 +779,7 @@ + /** + * @dev Check if the current call is authorized according to admin logic. + */ +- function _checkAuthorized() private { ++ function _checkAuthorized() internal virtual { // private → internal virtual for FV + address caller = _msgSender(); + (bool immediate, uint32 delay) = _canCallSelf(caller, _msgData()); + if (!immediate) { +@@ -792,7 +802,7 @@ + */ + function _getAdminRestrictions( + bytes calldata data +- ) private view returns (bool restricted, uint64 roleAdminId, uint32 executionDelay) { ++ ) internal view returns (bool restricted, uint64 roleAdminId, uint32 executionDelay) { // private → internal for FV + if (data.length < 4) { + return (false, 0, 0); + } +@@ -847,7 +857,7 @@ + address caller, + address target, + bytes calldata data +- ) private view returns (bool immediate, uint32 delay) { ++ ) internal view returns (bool immediate, uint32 delay) { // private → internal for FV + if (target == address(this)) { + return _canCallSelf(caller, data); + } else { +@@ -901,7 +911,7 @@ + /** + * @dev Extracts the selector from calldata. Panics if data is not at least 4 bytes + */ +- function _checkSelector(bytes calldata data) private pure returns (bytes4) { ++ function _checkSelector(bytes calldata data) internal pure returns (bytes4) { // private → internal for FV + return bytes4(data[0:4]); + } + } diff --git a/certora/harnesses/AccessManagedHarness.sol b/certora/harnesses/AccessManagedHarness.sol new file mode 100644 index 00000000000..50be23ad5bd --- /dev/null +++ b/certora/harnesses/AccessManagedHarness.sol @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.20; + +import "../patched/access/manager/IAccessManager.sol"; +import "../patched/access/manager/AccessManaged.sol"; + +contract AccessManagedHarness is AccessManaged { + bytes internal SOME_FUNCTION_CALLDATA = abi.encodeCall(this.someFunction, ()); + + constructor(address initialAuthority) AccessManaged(initialAuthority) {} + + function someFunction() public restricted() { + // Sanity for FV: the msg.data when calling this function should be the same as the data used when checking + // the schedule. This is a reformulation of `msg.data == SOME_FUNCTION_CALLDATA` that focuses on the operation + // hash for this call. + require( + IAccessManager(authority()).hashOperation(_msgSender(), address(this), msg.data) + == + IAccessManager(authority()).hashOperation(_msgSender(), address(this), SOME_FUNCTION_CALLDATA) + ); + } + + function authority_canCall_immediate(address caller) public view returns (bool result) { + (result,) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); + } + + function authority_canCall_delay(address caller) public view returns (uint32 result) { + (,result) = AuthorityUtils.canCallWithDelay(authority(), caller, address(this), this.someFunction.selector); + } + + function authority_getSchedule(address caller) public view returns (uint48) { + IAccessManager manager = IAccessManager(authority()); + return manager.getSchedule(manager.hashOperation(caller, address(this), SOME_FUNCTION_CALLDATA)); + } +} diff --git a/certora/harnesses/AccessManagerHarness.sol b/certora/harnesses/AccessManagerHarness.sol new file mode 100644 index 00000000000..69295d467e7 --- /dev/null +++ b/certora/harnesses/AccessManagerHarness.sol @@ -0,0 +1,116 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.20; + +import "../patched/access/manager/AccessManager.sol"; + +contract AccessManagerHarness is AccessManager { + // override with a storage slot that can basically take any value. + uint32 private _minSetback; + + constructor(address initialAdmin) AccessManager(initialAdmin) {} + + // FV + function minSetback() public view override returns (uint32) { + return _minSetback; + } + + function canCall_immediate(address caller, address target, bytes4 selector) external view returns (bool result) { + (result,) = canCall(caller, target, selector); + } + + function canCall_delay(address caller, address target, bytes4 selector) external view returns (uint32 result) { + (,result) = canCall(caller, target, selector); + } + + function canCallExtended(address caller, address target, bytes calldata data) external view returns (bool, uint32) { + return _canCallExtended(caller, target, data); + } + + function canCallExtended_immediate(address caller, address target, bytes calldata data) external view returns (bool result) { + (result,) = _canCallExtended(caller, target, data); + } + + function canCallExtended_delay(address caller, address target, bytes calldata data) external view returns (uint32 result) { + (,result) = _canCallExtended(caller, target, data); + } + + function getAdminRestrictions_restricted(bytes calldata data) external view returns (bool result) { + (result,,) = _getAdminRestrictions(data); + } + + function getAdminRestrictions_roleAdminId(bytes calldata data) external view returns (uint64 result) { + (,result,) = _getAdminRestrictions(data); + } + + function getAdminRestrictions_executionDelay(bytes calldata data) external view returns (uint32 result) { + (,,result) = _getAdminRestrictions(data); + } + + function hasRole_isMember(uint64 roleId, address account) external view returns (bool result) { + (result,) = hasRole(roleId, account); + } + + function hasRole_executionDelay(uint64 roleId, address account) external view returns (uint32 result) { + (,result) = hasRole(roleId, account); + } + + function getAccess_since(uint64 roleId, address account) external view returns (uint48 result) { + (result,,,) = getAccess(roleId, account); + } + + function getAccess_currentDelay(uint64 roleId, address account) external view returns (uint32 result) { + (,result,,) = getAccess(roleId, account); + } + + function getAccess_pendingDelay(uint64 roleId, address account) external view returns (uint32 result) { + (,,result,) = getAccess(roleId, account); + } + + function getAccess_effect(uint64 roleId, address account) external view returns (uint48 result) { + (,,,result) = getAccess(roleId, account); + } + + function getTargetAdminDelay_after(address target) public view virtual returns (uint32 result) { + (,result,) = _getTargetAdminDelayFull(target); + } + + function getTargetAdminDelay_effect(address target) public view virtual returns (uint48 result) { + (,,result) = _getTargetAdminDelayFull(target); + } + + function getRoleGrantDelay_after(uint64 roleId) public view virtual returns (uint32 result) { + (,result,) = _getRoleGrantDelayFull(roleId); + } + + function getRoleGrantDelay_effect(uint64 roleId) public view virtual returns (uint48 result) { + (,,result) = _getRoleGrantDelayFull(roleId); + } + + function hashExecutionId(address target, bytes4 selector) external pure returns (bytes32) { + return _hashExecutionId(target, selector); + } + + function executionId() external view returns (bytes32) { + return _executionId; + } + + // Pad with zeros (and don't revert) if data is too short. + function getSelector(bytes calldata data) external pure returns (bytes4) { + return bytes4(data); + } + + function getFirstArgumentAsAddress(bytes calldata data) external pure returns (address) { + return abi.decode(data[0x04:0x24], (address)); + } + + function getFirstArgumentAsUint64(bytes calldata data) external pure returns (uint64) { + return abi.decode(data[0x04:0x24], (uint64)); + } + + function _checkAuthorized() internal override { + // We need this hack otherwise certora will assume _checkSelector(_msgData()) can return anything :/ + require(msg.sig == _checkSelector(_msgData())); + super._checkAuthorized(); + } +} diff --git a/certora/specs.json b/certora/specs.json index 3e5acb568b8..20b02a03adc 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -14,6 +14,25 @@ "contract": "AccessControlDefaultAdminRulesHarness", "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"] }, + { + "spec": "AccessManager", + "contract": "AccessManagerHarness", + "files": ["certora/harnesses/AccessManagerHarness.sol"], + "options": ["--optimistic_hashing", "--optimistic_loop"] + }, + { + "spec": "AccessManaged", + "contract": "AccessManagedHarness", + "files": [ + "certora/harnesses/AccessManagedHarness.sol", + "certora/harnesses/AccessManagerHarness.sol" + ], + "options": [ + "--optimistic_hashing", + "--optimistic_loop", + "--link AccessManagedHarness:_authority=AccessManagerHarness" + ] + }, { "spec": "DoubleEndedQueue", "contract": "DoubleEndedQueueHarness", diff --git a/certora/specs/AccessManaged.spec b/certora/specs/AccessManaged.spec new file mode 100644 index 00000000000..adcb8593634 --- /dev/null +++ b/certora/specs/AccessManaged.spec @@ -0,0 +1,34 @@ +import "helpers/helpers.spec"; +import "methods/IAccessManaged.spec"; + +methods { + // FV + function someFunction() external; + function authority_canCall_immediate(address) external returns (bool); + function authority_canCall_delay(address) external returns (uint32); + function authority_getSchedule(address) external returns (uint48); +} + +invariant isConsumingScheduledOpClean() + isConsumingScheduledOp() == to_bytes4(0); + +rule callRestrictedFunction(env e) { + bool immediate = authority_canCall_immediate(e, e.msg.sender); + uint32 delay = authority_canCall_delay(e, e.msg.sender); + uint48 scheduleBefore = authority_getSchedule(e, e.msg.sender); + + someFunction@withrevert(e); + bool success = !lastReverted; + + uint48 scheduleAfter = authority_getSchedule(e, e.msg.sender); + + // can only call if immediate, or (with delay) by consuming a scheduled op + assert success => ( + immediate || + ( + delay > 0 && + isSetAndPast(e, scheduleBefore) && + scheduleAfter == 0 + ) + ); +} diff --git a/certora/specs/AccessManager.spec b/certora/specs/AccessManager.spec new file mode 100644 index 00000000000..cc4b0132a39 --- /dev/null +++ b/certora/specs/AccessManager.spec @@ -0,0 +1,826 @@ +import "helpers/helpers.spec"; +import "methods/IAccessManager.spec"; + +methods { + // FV + function canCall_immediate(address,address,bytes4) external returns (bool); + function canCall_delay(address,address,bytes4) external returns (uint32); + function canCallExtended(address,address,bytes) external returns (bool,uint32); + function canCallExtended_immediate(address,address,bytes) external returns (bool); + function canCallExtended_delay(address,address,bytes) external returns (uint32); + function getAdminRestrictions_restricted(bytes) external returns (bool); + function getAdminRestrictions_roleAdminId(bytes) external returns (uint64); + function getAdminRestrictions_executionDelay(bytes) external returns (uint32); + function hasRole_isMember(uint64,address) external returns (bool); + function hasRole_executionDelay(uint64,address) external returns (uint32); + function getAccess_since(uint64,address) external returns (uint48); + function getAccess_currentDelay(uint64,address) external returns (uint32); + function getAccess_pendingDelay(uint64,address) external returns (uint32); + function getAccess_effect(uint64,address) external returns (uint48); + function getTargetAdminDelay_after(address target) external returns (uint32); + function getTargetAdminDelay_effect(address target) external returns (uint48); + function getRoleGrantDelay_after(uint64 roleId) external returns (uint32); + function getRoleGrantDelay_effect(uint64 roleId) external returns (uint48); + function hashExecutionId(address,bytes4) external returns (bytes32) envfree; + function executionId() external returns (bytes32) envfree; + function getSelector(bytes) external returns (bytes4) envfree; + function getFirstArgumentAsAddress(bytes) external returns (address) envfree; + function getFirstArgumentAsUint64(bytes) external returns (uint64) envfree; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helpers │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition isOnlyAuthorized(bytes4 selector) returns bool = + selector == to_bytes4(sig:labelRole(uint64,string).selector ) || + selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector ) || + selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector ) || + selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector ) || + selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector ) || + selector == to_bytes4(sig:updateAuthority(address,address).selector ) || + selector == to_bytes4(sig:setTargetClosed(address,bool).selector ) || + selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector) || + selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector ) || + selector == to_bytes4(sig:revokeRole(uint64,address).selector ); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: executionId must be clean when not in the middle of a call │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant cleanExecutionId() + executionId() == to_bytes32(0); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: public role │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant publicRole(env e, address account) + hasRole_isMember(e, PUBLIC_ROLE(), account) && + hasRole_executionDelay(e, PUBLIC_ROLE(), account) == 0 && + getAccess_since(e, PUBLIC_ROLE(), account) == 0 && + getAccess_currentDelay(e, PUBLIC_ROLE(), account) == 0 && + getAccess_pendingDelay(e, PUBLIC_ROLE(), account) == 0 && + getAccess_effect(e, PUBLIC_ROLE(), account) == 0; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: hasRole is consistent with getAccess │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant hasRoleGetAccessConsistency(env e, uint64 roleId, address account) + hasRole_isMember(e, roleId, account) == (roleId == PUBLIC_ROLE() || isSetAndPast(e, getAccess_since(e, roleId, account))) && + hasRole_executionDelay(e, roleId, account) == getAccess_currentDelay(e, roleId, account); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: canCall, canCallExtended, getAccess, hasRole, isTargetClosed and getTargetFunctionRole do NOT revert │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule noRevert(env e) { + require nonpayable(e); + require sanity(e); + + address caller; + address target; + bytes data; + bytes4 selector; + uint64 roleId; + + canCall@withrevert(e, caller, target, selector); + assert !lastReverted; + + // require data.length <= max_uint64; + // + // canCallExtended@withrevert(e, caller, target, data); + // assert !lastReverted; + + getAccess@withrevert(e, roleId, caller); + assert !lastReverted; + + hasRole@withrevert(e, roleId, caller); + assert !lastReverted; + + isTargetClosed@withrevert(target); + assert !lastReverted; + + getTargetFunctionRole@withrevert(target, selector); + assert !lastReverted; + + // Not covered: + // - getAdminRestrictions (_1, _2 & _3) + // - getSelector +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: admin restrictions are correct │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getAdminRestrictions(env e, bytes data) { + bool restricted = getAdminRestrictions_restricted(e, data); + uint64 roleId = getAdminRestrictions_roleAdminId(e, data); + uint32 delay = getAdminRestrictions_executionDelay(e, data); + bytes4 selector = getSelector(data); + + if (data.length < 4) { + assert restricted == false; + assert roleId == 0; + assert delay == 0; + } else { + assert restricted == + isOnlyAuthorized(selector); + + assert roleId == ( + (restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) || + (restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector )) + ? getRoleAdmin(getFirstArgumentAsUint64(data)) + : ADMIN_ROLE() + ); + + assert delay == ( + (restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector )) || + (restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector )) || + (restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector)) + ? getTargetAdminDelay(e, getFirstArgumentAsAddress(data)) + : 0 + ); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: canCall │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule canCall(env e) { + address caller; + address target; + bytes4 selector; + + // Get relevant values + bool immediate = canCall_immediate(e, caller, target, selector); + uint32 delay = canCall_delay(e, caller, target, selector); + bool closed = isTargetClosed(target); + uint64 roleId = getTargetFunctionRole(target, selector); + bool isMember = hasRole_isMember(e, roleId, caller); + uint32 currentDelay = hasRole_executionDelay(e, roleId, caller); + + // Can only execute without delay in specific cases: + // - target not closed + // - if self-execution: `executionId` must match + // - if third party execution: must be member with no delay + assert immediate <=> ( + !closed && + ( + (caller == currentContract && executionId() == hashExecutionId(target, selector)) + || + (caller != currentContract && isMember && currentDelay == 0) + ) + ); + + // Can only execute with delay in specific cases: + // - target not closed + // - third party execution + // - caller is a member and has an execution delay + assert delay > 0 <=> ( + !closed && + caller != currentContract && + isMember && + currentDelay > 0 + ); + + // If there is a delay, then it must be the caller's execution delay + assert delay > 0 => delay == currentDelay; + + // Immediate execute means no delayed execution + assert immediate => delay == 0; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: canCallExtended │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule canCallExtended(env e) { + address caller; + address target; + bytes data; + bytes4 selector = getSelector(data); + + bool immediate = canCallExtended_immediate(e, caller, target, data); + uint32 delay = canCallExtended_delay(e, caller, target, data); + bool enabled = getAdminRestrictions_restricted(e, data); + uint64 roleId = getAdminRestrictions_roleAdminId(e, data); + uint32 operationDelay = getAdminRestrictions_executionDelay(e, data); + bool inRole = hasRole_isMember(e, roleId, caller); + uint32 executionDelay = hasRole_executionDelay(e, roleId, caller); + + if (target == currentContract) { + // Can only execute without delay in the specific cases: + // - caller is the AccessManager and the executionId is set + // or + // - data matches an admin restricted function + // - caller has the necessary role + // - operation delay is not set + // - execution delay is not set + assert immediate <=> ( + ( + caller == currentContract && + data.length >= 4 && + executionId() == hashExecutionId(target, selector) + ) || ( + caller != currentContract && + enabled && + inRole && + operationDelay == 0 && + executionDelay == 0 + ) + ); + + // Immediate execute means no delayed execution + // This is equivalent to "delay > 0 => !immediate" + assert immediate => delay == 0; + + // Can only execute with delay in specific cases: + // - caller is a third party + // - data matches an admin restricted function + // - caller has the necessary role + // -operation delay or execution delay is set + assert delay > 0 <=> ( + caller != currentContract && + enabled && + inRole && + (operationDelay > 0 || executionDelay > 0) + ); + + // If there is a delay, then it must be the maximum of caller's execution delay and the operation delay + assert delay > 0 => to_mathint(delay) == max(operationDelay, executionDelay); + } else if (data.length < 4) { + assert immediate == false; + assert delay == 0; + } else { + // results are equivalent when targeting third party contracts + assert immediate == canCall_immediate(e, caller, target, selector); + assert delay == canCall_delay(e, caller, target, selector); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getAccess │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getAccessChangeTime(uint64 roleId, address account) { + env e1; + env e2; + + // values before + mathint getAccess1Before = getAccess_since(e1, roleId, account); + mathint getAccess2Before = getAccess_currentDelay(e1, roleId, account); + mathint getAccess3Before = getAccess_pendingDelay(e1, roleId, account); + mathint getAccess4Before = getAccess_effect(e1, roleId, account); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + mathint getAccess1After = getAccess_since(e2, roleId, account); + mathint getAccess2After = getAccess_currentDelay(e2, roleId, account); + mathint getAccess3After = getAccess_pendingDelay(e2, roleId, account); + mathint getAccess4After = getAccess_effect(e2, roleId, account); + + // member "since" cannot change as a consequence of time passing + assert getAccess1Before == getAccess1After; + + // any change of any other value should be a consequence of the effect timepoint being reached + assert ( + getAccess2Before != getAccess2After || + getAccess3Before != getAccess3After || + getAccess4Before != getAccess4After + ) => ( + getAccess4Before != 0 && + getAccess4Before > clock(e1) && + getAccess4Before <= clock(e2) && + getAccess2After == getAccess3Before && + getAccess3After == 0 && + getAccess4After == 0 + ); +} + +rule getAccessChangeCall(uint64 roleId, address account) { + env e; + + // sanity + require sanity(e); + + // values before + mathint getAccess1Before = getAccess_since(e, roleId, account); + mathint getAccess2Before = getAccess_currentDelay(e, roleId, account); + mathint getAccess3Before = getAccess_pendingDelay(e, roleId, account); + mathint getAccess4Before = getAccess_effect(e, roleId, account); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values before + mathint getAccess1After = getAccess_since(e, roleId, account); + mathint getAccess2After = getAccess_currentDelay(e, roleId, account); + mathint getAccess3After = getAccess_pendingDelay(e, roleId, account); + mathint getAccess4After = getAccess_effect(e, roleId, account); + + // transitions + assert ( + getAccess1Before != getAccess1After || + getAccess2Before != getAccess2After || + getAccess3Before != getAccess3After || + getAccess4Before != getAccess4After + ) => ( + ( + f.selector == sig:grantRole(uint64,address,uint32).selector && + getAccess1After > 0 + ) || ( + ( + f.selector == sig:revokeRole(uint64,address).selector || + f.selector == sig:renounceRole(uint64,address).selector + ) && + getAccess1After == 0 && + getAccess2After == 0 && + getAccess3After == 0 && + getAccess4After == 0 + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: isTargetClosed │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule isTargetClosedChangeTime(address target) { + env e1; + env e2; + + // values before + bool isClosedBefore = isTargetClosed(e1, target); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + bool isClosedAfter = isTargetClosed(e2, target); + + // transitions + assert isClosedBefore == isClosedAfter; +} + +rule isTargetClosedChangeCall(address target) { + env e; + + // values before + bool isClosedBefore = isTargetClosed(e, target); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values after + bool isClosedAfter = isTargetClosed(e, target); + + // transitions + assert isClosedBefore != isClosedAfter => ( + f.selector == sig:setTargetClosed(address,bool).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getTargetFunctionRole │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getTargetFunctionRoleChangeTime(address target, bytes4 selector) { + env e1; + env e2; + + // values before + mathint roleIdBefore = getTargetFunctionRole(e1, target, selector); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + mathint roleIdAfter = getTargetFunctionRole(e2, target, selector); + + // transitions + assert roleIdBefore == roleIdAfter; +} + +rule getTargetFunctionRoleChangeCall(address target, bytes4 selector) { + env e; + + // values before + mathint roleIdBefore = getTargetFunctionRole(e, target, selector); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values after + mathint roleIdAfter = getTargetFunctionRole(e, target, selector); + + // transitions + assert roleIdBefore != roleIdAfter => ( + f.selector == sig:setTargetFunctionRole(address,bytes4[],uint64).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getTargetAdminDelay │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getTargetAdminDelayChangeTime(address target) { + env e1; + env e2; + + // values before + mathint delayBefore = getTargetAdminDelay(e1, target); + mathint delayPendingBefore = getTargetAdminDelay_after(e1, target); + mathint delayEffectBefore = getTargetAdminDelay_effect(e1, target); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + mathint delayAfter = getTargetAdminDelay(e2, target); + mathint delayPendingAfter = getTargetAdminDelay_after(e2, target); + mathint delayEffectAfter = getTargetAdminDelay_effect(e2, target); + + assert ( + delayBefore != delayAfter || + delayPendingBefore != delayPendingAfter || + delayEffectBefore != delayEffectAfter + ) => ( + delayEffectBefore > clock(e1) && + delayEffectBefore <= clock(e2) && + delayAfter == delayPendingBefore && + delayPendingAfter == 0 && + delayEffectAfter == 0 + ); +} + +rule getTargetAdminDelayChangeCall(address target) { + env e; + + // values before + mathint delayBefore = getTargetAdminDelay(e, target); + mathint delayPendingBefore = getTargetAdminDelay_after(e, target); + mathint delayEffectBefore = getTargetAdminDelay_effect(e, target); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values after + mathint delayAfter = getTargetAdminDelay(e, target); + mathint delayPendingAfter = getTargetAdminDelay_after(e, target); + mathint delayEffectAfter = getTargetAdminDelay_effect(e, target); + + // if anything changed ... + assert ( + delayBefore != delayAfter || + delayPendingBefore != delayPendingAfter || + delayEffectBefore != delayEffectAfter + ) => ( + ( + // ... it was the consequence of a call to setTargetAdminDelay + f.selector == sig:setTargetAdminDelay(address,uint32).selector + ) && ( + // ... delay cannot decrease instantly + delayAfter >= delayBefore + ) && ( + // ... if setback is not 0, value cannot change instantly + minSetback() > 0 => ( + delayBefore == delayAfter + ) + ) && ( + // ... if the value did not change and there is a minSetback, there must be something scheduled in the future + delayAfter == delayBefore && minSetback() > 0 => ( + delayEffectAfter >= clock(e) + minSetback() + ) + // note: if there is no minSetback, and if the caller "confirms" the current value, + // then this as immediate effect and nothing is scheduled + ) && ( + // ... if the value changed, then no further change should be scheduled + delayAfter != delayBefore => ( + delayPendingAfter == 0 && + delayEffectAfter == 0 + ) + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getRoleGrantDelay │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getRoleGrantDelayChangeTime(uint64 roleId) { + env e1; + env e2; + + // values before + mathint delayBefore = getRoleGrantDelay(e1, roleId); + mathint delayPendingBefore = getRoleGrantDelay_after(e1, roleId); + mathint delayEffectBefore = getRoleGrantDelay_effect(e1, roleId); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + mathint delayAfter = getRoleGrantDelay(e2, roleId); + mathint delayPendingAfter = getRoleGrantDelay_after(e2, roleId); + mathint delayEffectAfter = getRoleGrantDelay_effect(e2, roleId); + + assert ( + delayBefore != delayAfter || + delayPendingBefore != delayPendingAfter || + delayEffectBefore != delayEffectAfter + ) => ( + delayEffectBefore > clock(e1) && + delayEffectBefore <= clock(e2) && + delayAfter == delayPendingBefore && + delayPendingAfter == 0 && + delayEffectAfter == 0 + ); +} + +rule getRoleGrantDelayChangeCall(uint64 roleId) { + env e; + + // values before + mathint delayBefore = getRoleGrantDelay(e, roleId); + mathint delayPendingBefore = getRoleGrantDelay_after(e, roleId); + mathint delayEffectBefore = getRoleGrantDelay_effect(e, roleId); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values after + mathint delayAfter = getRoleGrantDelay(e, roleId); + mathint delayPendingAfter = getRoleGrantDelay_after(e, roleId); + mathint delayEffectAfter = getRoleGrantDelay_effect(e, roleId); + + // if anything changed ... + assert ( + delayBefore != delayAfter || + delayPendingBefore != delayPendingAfter || + delayEffectBefore != delayEffectAfter + ) => ( + ( + // ... it was the consequence of a call to setTargetAdminDelay + f.selector == sig:setGrantDelay(uint64,uint32).selector + ) && ( + // ... delay cannot decrease instantly + delayAfter >= delayBefore + ) && ( + // ... if setback is not 0, value cannot change instantly + minSetback() > 0 => ( + delayBefore == delayAfter + ) + ) && ( + // ... if the value did not change and there is a minSetback, there must be something scheduled in the future + delayAfter == delayBefore && minSetback() > 0 => ( + delayEffectAfter >= clock(e) + minSetback() + ) + // note: if there is no minSetback, and if the caller "confirms" the current value, + // then this as immediate effect and nothing is scheduled + ) && ( + // ... if the value changed, then no further change should be scheduled + delayAfter != delayBefore => ( + delayPendingAfter == 0 && + delayEffectAfter == 0 + ) + ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getRoleAdmin & getRoleGuardian │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getRoleAdminChangeCall(uint64 roleId) { + // values before + mathint adminIdBefore = getRoleAdmin(roleId); + + // arbitrary function call + env e; method f; calldataarg args; f(e, args); + + // values after + mathint adminIdAfter = getRoleAdmin(roleId); + + // transitions + assert adminIdBefore != adminIdAfter => f.selector == sig:setRoleAdmin(uint64,uint64).selector; +} + +rule getRoleGuardianChangeCall(uint64 roleId) { + // values before + mathint guardianIdBefore = getRoleGuardian(roleId); + + // arbitrary function call + env e; method f; calldataarg args; f(e, args); + + // values after + mathint guardianIdAfter = getRoleGuardian(roleId); + + // transitions + assert guardianIdBefore != guardianIdAfter => ( + f.selector == sig:setRoleGuardian(uint64,uint64).selector + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getNonce │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getNonceChangeCall(bytes32 operationId) { + // values before + mathint nonceBefore = getNonce(operationId); + + // reasonable assumption + require nonceBefore < max_uint32; + + // arbitrary function call + env e; method f; calldataarg args; f(e, args); + + // values after + mathint nonceAfter = getNonce(operationId); + + // transitions + assert nonceBefore != nonceAfter => ( + f.selector == sig:schedule(address,bytes,uint48).selector && + nonceAfter == nonceBefore + 1 + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ State transitions: getSchedule │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule getScheduleChangeTime(bytes32 operationId) { + env e1; + env e2; + + // values before + mathint scheduleBefore = getSchedule(e1, operationId); + + // time pass: e1 → e2 + require clock(e1) <= clock(e2); + + // values after + mathint scheduleAfter = getSchedule(e2, operationId); + + // transition + assert scheduleBefore != scheduleAfter => ( + scheduleBefore + expiration() > clock(e1) && + scheduleBefore + expiration() <= clock(e2) && + scheduleAfter == 0 + ); +} + +rule getScheduleChangeCall(bytes32 operationId) { + env e; + + // values before + mathint scheduleBefore = getSchedule(e, operationId); + + // arbitrary function call + method f; calldataarg args; f(e, args); + + // values after + mathint scheduleAfter = getSchedule(e, operationId); + + // transitions + assert scheduleBefore != scheduleAfter => ( + (f.selector == sig:schedule(address,bytes,uint48).selector && scheduleAfter >= clock(e)) || + (f.selector == sig:execute(address,bytes).selector && scheduleAfter == 0 ) || + (f.selector == sig:cancel(address,address,bytes).selector && scheduleAfter == 0 ) || + (f.selector == sig:consumeScheduledOp(address,bytes).selector && scheduleAfter == 0 ) || + (isOnlyAuthorized(to_bytes4(f.selector)) && scheduleAfter == 0 ) + ); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: restricted functions can only be called by owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule restrictedFunctions(env e) { + require nonpayable(e); + require sanity(e); + + method f; + calldataarg args; + + f(e,args); + + assert ( + f.selector == sig:labelRole(uint64,string).selector || + f.selector == sig:setRoleAdmin(uint64,uint64).selector || + f.selector == sig:setRoleGuardian(uint64,uint64).selector || + f.selector == sig:setGrantDelay(uint64,uint32).selector || + f.selector == sig:setTargetAdminDelay(address,uint32).selector || + f.selector == sig:updateAuthority(address,address).selector || + f.selector == sig:setTargetClosed(address,bool).selector || + f.selector == sig:setTargetFunctionRole(address,bytes4[],uint64).selector + ) => ( + hasRole_isMember(e, ADMIN_ROLE(), e.msg.sender) || e.msg.sender == currentContract + ); +} + +rule restrictedFunctionsGrantRole(env e) { + require nonpayable(e); + require sanity(e); + + uint64 roleId; + address account; + uint32 executionDelay; + + // We want to check that the caller has the admin role before we possibly grant it. + bool hasAdminRoleBefore = hasRole_isMember(e, getRoleAdmin(roleId), e.msg.sender); + + grantRole(e, roleId, account, executionDelay); + + assert hasAdminRoleBefore || e.msg.sender == currentContract; +} + +rule restrictedFunctionsRevokeRole(env e) { + require nonpayable(e); + require sanity(e); + + uint64 roleId; + address account; + + // This is needed if roleId is self-administered, the `revokeRole` call could target + // e.msg.sender and remove the very role that is necessary for authorizing the call. + bool hasAdminRoleBefore = hasRole_isMember(e, getRoleAdmin(roleId), e.msg.sender); + + revokeRole(e, roleId, account); + + assert hasAdminRoleBefore || e.msg.sender == currentContract; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Functions: canCall delay is enforced for calls to execute (only for others target) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// getScheduleChangeCall proves that only {schedule} can set an operation schedule to a non 0 value +rule callDelayEnforce_scheduleInTheFuture(env e) { + address target; + bytes data; + uint48 when; + + // Condition: calling a third party with a delay + mathint delay = canCallExtended_delay(e, e.msg.sender, target, data); + require delay > 0; + + // Schedule + schedule(e, target, data, when); + + // Get operation schedule + mathint timepoint = getSchedule(e, hashOperation(e.msg.sender, target, data)); + + // Schedule is far enough in the future + assert timepoint == max(clock(e) + delay, when); +} + +rule callDelayEnforce_executeAfterDelay(env e) { + address target; + bytes data; + + // Condition: calling a third party with a delay + mathint delay = canCallExtended_delay(e, e.msg.sender, target, data); + + // Get operation schedule before + mathint scheduleBefore = getSchedule(e, hashOperation(e.msg.sender, target, data)); + + // Do call + execute@withrevert(e, target, data); + bool success = !lastReverted; + + // Get operation schedule after + mathint scheduleAfter = getSchedule(e, hashOperation(e.msg.sender, target, data)); + + // Can only execute if delay is set and has passed + assert success => ( + delay > 0 => ( + scheduleBefore != 0 && + scheduleBefore <= clock(e) + ) && + scheduleAfter == 0 + ); +} diff --git a/certora/specs/helpers/helpers.spec b/certora/specs/helpers/helpers.spec index a6c1e230248..7125ce2d817 100644 --- a/certora/specs/helpers/helpers.spec +++ b/certora/specs/helpers/helpers.spec @@ -1,7 +1,12 @@ // environment definition nonpayable(env e) returns bool = e.msg.value == 0; definition nonzerosender(env e) returns bool = e.msg.sender != 0; +definition sanity(env e) returns bool = clock(e) > 0 && clock(e) <= max_uint48; // math definition min(mathint a, mathint b) returns mathint = a < b ? a : b; definition max(mathint a, mathint b) returns mathint = a > b ? a : b; + +// time +definition clock(env e) returns mathint = to_mathint(e.block.timestamp); +definition isSetAndPast(env e, uint48 timepoint) returns bool = timepoint != 0 && to_mathint(timepoint) <= clock(e); diff --git a/certora/specs/methods/IAccessManaged.spec b/certora/specs/methods/IAccessManaged.spec new file mode 100644 index 00000000000..886d917d47e --- /dev/null +++ b/certora/specs/methods/IAccessManaged.spec @@ -0,0 +1,5 @@ +methods { + function authority() external returns (address) envfree; + function isConsumingScheduledOp() external returns (bytes4) envfree; + function setAuthority(address) external; +} diff --git a/certora/specs/methods/IAccessManager.spec b/certora/specs/methods/IAccessManager.spec new file mode 100644 index 00000000000..5d305f7b45d --- /dev/null +++ b/certora/specs/methods/IAccessManager.spec @@ -0,0 +1,33 @@ +methods { + function ADMIN_ROLE() external returns (uint64) envfree; + function PUBLIC_ROLE() external returns (uint64) envfree; + function canCall(address,address,bytes4) external returns (bool,uint32); + function expiration() external returns (uint32) envfree; + function minSetback() external returns (uint32) envfree; + function isTargetClosed(address) external returns (bool) envfree; + function getTargetFunctionRole(address,bytes4) external returns (uint64) envfree; + function getTargetAdminDelay(address) external returns (uint32); + function getRoleAdmin(uint64) external returns (uint64) envfree; + function getRoleGuardian(uint64) external returns (uint64) envfree; + function getRoleGrantDelay(uint64) external returns (uint32); + function getAccess(uint64,address) external returns (uint48,uint32,uint32,uint48); + function hasRole(uint64,address) external returns (bool,uint32); + function labelRole(uint64,string) external; + function grantRole(uint64,address,uint32) external; + function revokeRole(uint64,address) external; + function renounceRole(uint64,address) external; + function setRoleAdmin(uint64,uint64) external; + function setRoleGuardian(uint64,uint64) external; + function setGrantDelay(uint64,uint32) external; + function setTargetFunctionRole(address,bytes4[],uint64) external; + function setTargetAdminDelay(address,uint32) external; + function setTargetClosed(address,bool) external; + function hashOperation(address,address,bytes) external returns (bytes32) envfree; + function getNonce(bytes32) external returns (uint32) envfree; + function getSchedule(bytes32) external returns (uint48); + function schedule(address,bytes,uint48) external returns (bytes32,uint32); + function execute(address,bytes) external returns (uint32); + function cancel(address,address,bytes) external returns (uint32); + function consumeScheduledOp(address,bytes) external; + function updateAuthority(address,address) external; +} diff --git a/contracts/access/manager/AccessManager.sol b/contracts/access/manager/AccessManager.sol index 234164f219d..af223b45ce3 100644 --- a/contracts/access/manager/AccessManager.sol +++ b/contracts/access/manager/AccessManager.sol @@ -586,7 +586,7 @@ contract AccessManager is Context, Multicall, IAccessManager { uint48 minWhen = Time.timestamp() + setback; - // if call with delay is not authorized, or if requested timing is too soon + // If call with delay is not authorized, or if requested timing is too soon, revert if (setback == 0 || (when > 0 && when < minWhen)) { revert AccessManagerUnauthorizedCall(caller, target, _checkSelector(data)); } @@ -639,7 +639,7 @@ contract AccessManager is Context, Multicall, IAccessManager { // Fetch restrictions that apply to the caller on the targeted function (bool immediate, uint32 setback) = _canCallExtended(caller, target, data); - // If caller is not authorised, revert + // If call is not authorized, revert if (!immediate && setback == 0) { revert AccessManagerUnauthorizedCall(caller, target, _checkSelector(data)); } diff --git a/requirements.txt b/requirements.txt index fd0ec301991..bdea09aa819 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1 +1 @@ -certora-cli==4.8.0 +certora-cli==4.13.1