diff --git a/certora/harnesses/AccessControlHarness.sol b/certora/harnesses/AccessControlHarness.sol new file mode 100644 index 000000000..3ae6e7e8c --- /dev/null +++ b/certora/harnesses/AccessControlHarness.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts (last updated v4.5.0) (access/AccessControl.sol) + +pragma solidity ^0.8.0; + +import "../munged/access/AccessControl.sol"; + +contract AccessControlHarness is AccessControl { + +} diff --git a/certora/munged/access/AccessControl.sol b/certora/munged/access/AccessControl.sol index 2ac203867..dec22fe8e 100644 --- a/certora/munged/access/AccessControl.sol +++ b/certora/munged/access/AccessControl.sol @@ -93,7 +93,7 @@ abstract contract AccessControl is Context, IAccessControl, ERC165 { * * _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 --git a/certora/munged/governance/TimelockController.sol b/certora/munged/governance/TimelockController.sol index 621ebd87b..da38df8f3 100644 --- a/certora/munged/governance/TimelockController.sol +++ b/certora/munged/governance/TimelockController.sol @@ -24,10 +24,10 @@ contract TimelockController is AccessControl { bytes32 public constant TIMELOCK_ADMIN_ROLE = keccak256("TIMELOCK_ADMIN_ROLE"); bytes32 public constant PROPOSER_ROLE = keccak256("PROPOSER_ROLE"); bytes32 public constant EXECUTOR_ROLE = keccak256("EXECUTOR_ROLE"); - uint256 internal constant _DONE_TIMESTAMP = uint256(1); + uint256 public constant _DONE_TIMESTAMP = uint256(1); // HARNESS: internal -> public mapping(bytes32 => uint256) private _timestamps; - uint256 private _minDelay; + uint256 public _minDelay; // HARNESS: private -> public /** * @dev Emitted when a call is scheduled as part of operation `id`. diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh index e8ac5548b..696ab2595 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -1,7 +1,9 @@ certoraRun \ - certora/harnesses/TimelockControllerHarness.sol \ + certora/harnesses/TimelockControllerHarness.sol certora/harnesses/AccessControlHarness.sol \ --verify TimelockControllerHarness:certora/specs/TimelockController.spec \ --solc solc8.2 \ --optimistic_loop \ - --cloud \ - --msg "sanity" \ No newline at end of file + --cloud alex/uhf-more-precision \ + --rule_sanity \ + --msg "sanity flag check" + \ No newline at end of file diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 9c0b99c5f..b8a15cbe3 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,36 +1,323 @@ +using AccessControlHarness as AC + methods { - // hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) => uniqueHashGhost(target, value, data, predecessor, salt) + getTimestamp(bytes32) returns(uint256) envfree + _DONE_TIMESTAMP() returns(uint256) envfree + _minDelay() returns(uint256) envfree + getMinDelay() returns(uint256) envfree + + cancel(bytes32) + schedule(address, uint256, bytes, bytes32, bytes32, uint256) + execute(address, uint256, bytes, bytes32, bytes32) + + hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree // => uniqueHashGhost(target, value, data, predecessor, salt) } -// ghost uniqueHashGhost(address, uint256, bytes, bytes32, bytes32) returns bytes32; -// -// Assuming the hash is deterministic, and correlates the trio properly -// function hashUniquness(address target1, uint256 value1, bytes data1, bytes32 predecessor1, bytes32 salt1, -// address target2, uint256 value2, bytes data2, bytes32 predecessor2, bytes32 salt2){ -// require ((target1 != target2) || (value1 != value2) || (data1 != data2) || (predecessor1 != predecessor2) || (salt1 != salt2)) <=> -// (uniqueHashGhost(target1, value1, data1, predecessor1, salt1) != uniqueHashGhost(target2, value2, data2, predecessor2, salt2)); -// } -// -// -// rule keccakCheck(method f, env e){ -// address target; -// uint256 value; -// bytes data; -// bytes32 predecessor; -// bytes32 salt; -// -// hashUniquness(target, value, data, predecessor, salt, -// target, value, data, predecessor, salt); -// -// bytes32 a = hashOperation(e, target, value, data, predecessor, salt); -// bytes32 b = hashOperation(e, target, value, data, predecessor, salt); -// -// assert a == b, "hashes are different"; -// } -rule sanity(method f) { - env e; - calldataarg arg; - f(e, arg); - assert false; + +//////////////////////////////////////////////////////////////////////////// +// Definitions // +//////////////////////////////////////////////////////////////////////////// + + +definition unset(bytes32 id) returns bool = + getTimestamp(id) == 0; + +definition pending(bytes32 id) returns bool = + getTimestamp(id) > _DONE_TIMESTAMP(); + +definition ready(bytes32 id, env e) returns bool = + getTimestamp(id) > _DONE_TIMESTAMP() && getTimestamp(id) <= e.block.timestamp; + +definition done(bytes32 id) returns bool = + getTimestamp(id) == _DONE_TIMESTAMP(); + + + +//////////////////////////////////////////////////////////////////////////// +// Functions // +//////////////////////////////////////////////////////////////////////////// + + +function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ + require data.length < 3; + require hashOperation(target, value, data, predecessor, salt) == id; +} + + +//////////////////////////////////////////////////////////////////////////// +// Ghosts // +//////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////////// +// Invariants // +//////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////////// +// Rules // +//////////////////////////////////////////////////////////////////////////// + + +rule keccakCheck(method f, env e){ + address target; + uint256 value; + bytes data; + bytes32 predecessor; + bytes32 salt; + + require data.length < 3; + + bytes32 a = hashOperation(target, value, data, predecessor, salt); + bytes32 b = hashOperation(target, value, data, predecessor, salt); + + assert a == b, "hashes are different"; +} + + + +///////////////////////////////////////////////////////////// +// STATE TRANSITIONS +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// unset() -> unset() || pending() only +rule unsetPendingTransitionGeneral(method f, env e){ + bytes32 id; + + require unset(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert pending(id) || unset(id); +} + + +// STATUS - verified +// unset() -> pending() via schedule() and scheduleBatch() only +rule unsetPendingTransitionMethods(method f, env e){ + bytes32 id; + + require unset(id); + + calldataarg args; + f(e, args); + + assert pending(id) => f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector , "Why do we need to follow the schedule?"; +} + + +// STATUS - verified +// ready() -> done() via execute() and executeBatch() only +rule readyDoneTransition(method f, env e){ + bytes32 id; + + require ready(id, e); + + calldataarg args; + f(e, args); + + assert done(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not done yet!"; +} + + +// STATUS - verified +// pending() -> cancelled() via cancel() only +rule pendingCancelledTransition(method f, env e){ + bytes32 id; + + require pending(id); + + calldataarg args; + f(e, args); + + assert unset(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; +} + + +// STATUS - verified +// done() -> nowhere +rule doneToNothingTransition(method f, env e){ + bytes32 id; + + require done(id); + + calldataarg args; + f(e, args); + + assert done(id), "Did you find a way to escape? There is no way! HA-HA-HA"; +} + + + +///////////////////////////////////////////////////////////// +// THE REST +///////////////////////////////////////////////////////////// + + +// STATUS - verified +// only TimelockController contract can change minDealy +rule minDealyOnlyChange(method f, env e){ + uint256 delayBefore = _minDelay(); + + calldataarg args; + f(e, args); + + uint256 delayAfter = _minDelay(); + + assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!"; +} + + +// STATUS - verified +// Only proposers can schedule an operation +rule scheduleOnlyWay(method f, env e){ + uint256 delayBefore = _minDelay(); + + calldataarg args; + f(e, args); + + uint256 delayAfter = _minDelay(); + + assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!"; +} + + +// STATUS - in progress (need working hash) +// execute() is the only way to set timestamp to 1 +rule getTimestampOnlyChange(method f, env e){ + bytes32 id; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require getTimestamp(id) != 1; + hashIdCorrelation(id, target, value, data, predecessor, salt); + + calldataarg args; + // write helper function with values from hashOperation() call; + f(e, args); + + assert getTimestamp(id) == 1 => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "Did you find a way to break the system?"; +} + + +// STATUS - in progress (need working hash) +// scheduled operation timestamp == block.timestamp + delay (kind of unit test) +rule scheduleCheck(method f, env e){ + bytes32 id; + + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require getTimestamp(id) < e.block.timestamp; + // require getMinDelay() > 0; + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert getTimestamp(id) == to_uint256(e.block.timestamp + getMinDelay()), "Time doesn't obey to mortal souls"; +} + + +// STATUS - in progress (need working hash) +// Cannot call execute on a pending (not ready) operation +rule cannotCallExecute(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require pending(id) && !ready(id, e); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - in progress (need working hash) +// in unset() execute() reverts +rule executeRevertFromUnset(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require unset(id); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Execute reverts => state returns to pending +rule executeRevertEffectCheck(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require pending(id) && !ready(id, e); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted => pending(id) && !ready(id, e), "you go against execution nature"; +} + + +// STATUS - verified +// Canceled operations cannot be executed → can’t move from canceled to ready +rule cancelledNotExecuted(method f, env e){ + bytes32 id; + + require unset(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert !done(id), "The ship is not a creature of the air"; +} + + +// STATUS - in progress (need working hash) +// Only proposers can schedule an operation +rule onlyProposer(method f, env e){ + bytes32 id; + bytes32 role; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + require unset(id); + hashIdCorrelation(id, target, value, data, predecessor, salt); + + AC._checkRole@withrevert(e, role); + + bool isCheckRoleReverted = lastReverted; + + schedule@withrevert(e, target, value, data, predecessor, salt, delay); + + bool isScheduleReverted = lastReverted; + + assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +} + + +// STATUS - in progress +// Ready = has waited minimum period after pending +rule cooldown(method f, env e, env e2){ + bytes32 id; + + require unset(id); + + calldataarg args; + f(e, args); + + // e.block.timestamp - delay > time scheduled => ready() + assert e.block.timestamp >= getTimestamp(id) => ready(id, e), "No rush! When I'm ready, I'm ready"; } \ No newline at end of file