Formal verification of AccessManager (#4611)

Co-authored-by: Ernesto García <[email protected]>
Co-authored-by: Francisco Giordano <[email protected]>

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 _,/,$@)) \

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]);
+     }
+ }

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));
+    }
+}

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();
+    }
+}

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",

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
+        )
+    );
+}