diff --git a/certora/harnesses/TimelockControllerHarness.sol b/certora/harnesses/TimelockControllerHarness.sol new file mode 100644 index 000000000..d1ea99065 --- /dev/null +++ b/certora/harnesses/TimelockControllerHarness.sol @@ -0,0 +1,12 @@ +pragma solidity ^0.8.0; + +import "../patched/governance/TimelockController.sol"; + +contract TimelockControllerHarness is TimelockController { + constructor( + uint256 minDelay, + address[] memory proposers, + address[] memory executors, + address admin + ) TimelockController(minDelay, proposers, executors, admin) {} +} diff --git a/certora/specs.js b/certora/specs.js index 8f2a12855..19d62e150 100644 --- a/certora/specs.js +++ b/certora/specs.js @@ -42,6 +42,13 @@ module.exports = [ contract: 'InitializableHarness', files: ['certora/harnesses/InitializableHarness.sol'], }, + // TimelockController + { + spec: 'TimelockController', + contract: 'TimelockControllerHarness', + files: ['certora/harnesses/TimelockControllerHarness.sol'], + options: ['--optimistic_hashing', '--optimistic_loop'] + }, // Governor ...product( ['GovernorInvariants', 'GovernorBaseRules', 'GovernorChanges', 'GovernorStates'], diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index 8e8f6ac9d..35927c5d3 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -1,12 +1,5 @@ import "helpers.spec" - -methods { - hasRole(bytes32, address) returns(bool) envfree - getRoleAdmin(bytes32) returns(bytes32) envfree - grantRole(bytes32, address) - revokeRole(bytes32, address) - renounceRole(bytes32, address) -} +import "methods/IAccessControl.spec" /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec new file mode 100644 index 000000000..e140c11de --- /dev/null +++ b/certora/specs/TimelockController.spec @@ -0,0 +1,275 @@ +import "helpers.spec" +import "methods/IAccessControl.spec" + +methods { + TIMELOCK_ADMIN_ROLE() returns (bytes32) envfree + PROPOSER_ROLE() returns (bytes32) envfree + EXECUTOR_ROLE() returns (bytes32) envfree + CANCELLER_ROLE() returns (bytes32) envfree + isOperation(bytes32) returns (bool) envfree + isOperationPending(bytes32) returns (bool) envfree + isOperationReady(bytes32) returns (bool) + isOperationDone(bytes32) returns (bool) envfree + getTimestamp(bytes32) returns (uint256) envfree + getMinDelay() returns (uint256) envfree + + hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree + hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree + + schedule(address, uint256, bytes, bytes32, bytes32, uint256) + scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256) + execute(address, uint256, bytes, bytes32, bytes32) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) + cancel(bytes32) + + updateDelay(uint256) +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Helpers │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// Uniformly handle scheduling of batched and non-batched operations. +function helperScheduleWithRevert(env e, method f, bytes32 id, uint256 delay) { + if (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector) { + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + require hashOperation(target, value, data, predecessor, salt) == id; // Correlation + schedule@withrevert(e, target, value, data, predecessor, salt, delay); + } else if (f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector) { + address[] targets; uint256[] values; bytes[] payloads; bytes32 predecessor; bytes32 salt; + require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation + scheduleBatch@withrevert(e, targets, values, payloads, predecessor, salt, delay); + } else { + calldataarg args; + f@withrevert(e, args); + } +} + +// Uniformly handle execution of batched and non-batched operations. +function helperExecuteWithRevert(env e, method f, bytes32 id, bytes32 predecessor) { + if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { + address target; uint256 value; bytes data; bytes32 salt; + require hashOperation(target, value, data, predecessor, salt) == id; // Correlation + execute@withrevert(e, target, value, data, predecessor, salt); + } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { + address[] targets; uint256[] values; bytes[] payloads; bytes32 salt; + require hashOperationBatch(targets, values, payloads, predecessor, salt) == id; // Correlation + executeBatch@withrevert(e, targets, values, payloads, predecessor, salt); + } else { + calldataarg args; + f@withrevert(e, args); + } +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Definitions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition DONE_TIMESTAMP() returns uint256 = 1; +definition UNSET() returns uint8 = 0x1; +definition PENDING() returns uint8 = 0x2; +definition DONE() returns uint8 = 0x4; + +definition isUnset(bytes32 id) returns bool = !isOperation(id); +definition isPending(bytes32 id) returns bool = isOperationPending(id); +definition isDone(bytes32 id) returns bool = isOperationDone(id); +definition state(bytes32 id) returns uint8 = (isUnset(id) ? UNSET() : 0) | (isPending(id) ? PENDING() : 0) | (isDone(id) ? DONE() : 0); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariants: consistency of accessors │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant isOperationCheck(bytes32 id) + isOperation(id) <=> getTimestamp(id) > 0 + filtered { f -> !f.isView } + +invariant isOperationPendingCheck(bytes32 id) + isOperationPending(id) <=> getTimestamp(id) > DONE_TIMESTAMP() + filtered { f -> !f.isView } + +invariant isOperationDoneCheck(bytes32 id) + isOperationDone(id) <=> getTimestamp(id) == DONE_TIMESTAMP() + filtered { f -> !f.isView } + +invariant isOperationReadyCheck(env e, bytes32 id) + isOperationReady(e, id) <=> (isOperationPending(id) && getTimestamp(id) <= e.block.timestamp) + filtered { f -> !f.isView } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: a proposal id is either unset, pending or done │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant stateConsistency(bytes32 id, env e) + // Check states are mutually exclusive + (isUnset(id) <=> (!isPending(id) && !isDone(id) )) && + (isPending(id) <=> (!isUnset(id) && !isDone(id) )) && + (isDone(id) <=> (!isUnset(id) && !isPending(id))) && + // Check that the state helper behaves as expected: + (isUnset(id) <=> state(id) == UNSET() ) && + (isPending(id) <=> state(id) == PENDING() ) && + (isDone(id) <=> state(id) == DONE() ) && + // Check substate + isOperationReady(e, id) => isPending(id) + filtered { f -> !f.isView } + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: state transition rules │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule stateTransition(bytes32 id, env e, method f, calldataarg args) { + require e.block.timestamp > 1; // Sanity + + uint8 stateBefore = state(id); + f(e, args); + uint8 stateAfter = state(id); + + // Cannot jump from UNSET to DONE + assert stateBefore == UNSET() => stateAfter != DONE(); + + // UNSET → PENDING: schedule or scheduleBatch + assert stateBefore == UNSET() && stateAfter == PENDING() => ( + f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || + f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector + ); + + // PENDING → UNSET: cancel + assert stateBefore == PENDING() && stateAfter == UNSET() => ( + f.selector == cancel(bytes32).selector + ); + + // PENDING → DONE: execute or executeBatch + assert stateBefore == PENDING() && stateAfter == DONE() => ( + f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || + f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector + ); + + // DONE is final + assert stateBefore == DONE() => stateAfter == DONE(); +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: minimum delay can only be updated through a timelock execution │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule minDelayOnlyChange(env e) { + uint256 delayBefore = getMinDelay(); + + method f; calldataarg args; + f(e, args); + + assert delayBefore != getMinDelay() => (e.msg.sender == currentContract && f.selector == updateDelay(uint256).selector), "Unauthorized delay update"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: schedule liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule schedule(env e, method f, bytes32 id, uint256 delay) filtered { f -> + f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector || + f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector +} { + require nonpayable(e); + + // Basic timestamp assumptions + require e.block.timestamp > 1; + require e.block.timestamp + delay < max_uint256; + require e.block.timestamp + getMinDelay() < max_uint256; + + bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); + + uint8 stateBefore = state(id); + bool isDelaySufficient = delay >= getMinDelay(); + bool isProposerBefore = hasRole(PROPOSER_ROLE(), e.msg.sender); + + helperScheduleWithRevert(e, f, id, delay); + bool success = !lastReverted; + + // liveness + assert success <=> ( + stateBefore == UNSET() && + isDelaySufficient && + isProposerBefore + ); + + // effect + assert success => state(id) == PENDING(), "State transition violation"; + assert success => getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Proposal timestamp not correctly set"; + + // no side effect + assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: execute liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule execute(env e, method f, bytes32 id, bytes32 predecessor) filtered { f -> + f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector || + f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector +} { + bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); + + uint8 stateBefore = state(id); + bool isOperationReadyBefore = isOperationReady(e, id); + bool isExecutorOrOpen = hasRole(EXECUTOR_ROLE(), e.msg.sender) || hasRole(EXECUTOR_ROLE(), 0); + bool predecessorDependency = predecessor == 0 || isDone(predecessor); + + helperExecuteWithRevert(e, f, id, predecessor); + bool success = !lastReverted; + + // The underlying transaction can revert, and that would cause the execution to revert. We can check that all non + // reverting calls meet the requirements in terms of proposal readiness, access control and predecessor dependency. + // We can't however guarantee that these requirements being meet ensure liveness of the proposal, because the + // proposal can revert for reasons beyond our control. + + // liveness, should be `<=>` but can only check `=>` (see comment above) + assert success => ( + stateBefore == PENDING() && + isOperationReadyBefore && + predecessorDependency && + isExecutorOrOpen + ); + + // effect + assert success => state(id) == DONE(), "State transition violation"; + + // no side effect + assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: cancel liveness and effects │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cancel(env e, bytes32 id) { + require nonpayable(e); + + bytes32 otherId; uint256 otherTimestamp = getTimestamp(otherId); + + uint8 stateBefore = state(id); + bool isCanceller = hasRole(CANCELLER_ROLE(), e.msg.sender); + + cancel@withrevert(e, id); + bool success = !lastReverted; + + // liveness + assert success <=> ( + stateBefore == PENDING() && + isCanceller + ); + + // effect + assert success => state(id) == UNSET(), "State transition violation"; + + // no side effect + assert otherTimestamp != getTimestamp(otherId) => id == otherId, "Other proposal affected"; +} diff --git a/certora/specs/methods/IAccessControl.spec b/certora/specs/methods/IAccessControl.spec new file mode 100644 index 000000000..4d41ffda7 --- /dev/null +++ b/certora/specs/methods/IAccessControl.spec @@ -0,0 +1,7 @@ +methods { + hasRole(bytes32, address) returns(bool) envfree + getRoleAdmin(bytes32) returns(bytes32) envfree + grantRole(bytes32, address) + revokeRole(bytes32, address) + renounceRole(bytes32, address) +}