From 479118fcd1ce4cdce646231fd3c350e577ce13f0 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Mon, 4 Apr 2022 21:33:31 +0100 Subject: [PATCH] push to report issues --- certora/specs/TimelockController.spec | 68 ++++++++++++++++++--------- 1 file changed, 47 insertions(+), 21 deletions(-) diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 65aedeba8..9e08fcf98 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -1,8 +1,7 @@ -using AccessControlHarness as AC - methods { getTimestamp(bytes32) returns(uint256) envfree _DONE_TIMESTAMP() returns(uint256) envfree + PROPOSER_ROLE() returns(bytes32) envfree _minDelay() returns(uint256) envfree getMinDelay() returns(uint256) envfree hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree @@ -10,6 +9,8 @@ methods { cancel(bytes32) schedule(address, uint256, bytes32, bytes32, bytes32, uint256) execute(address, uint256, bytes, bytes32, bytes32) + executeBatch(address[], uint256[], bytes[], bytes32, bytes32) + _checkRole(bytes32) => DISPATCHER(true) } //////////////////////////////////////////////////////////////////////////// @@ -76,7 +77,7 @@ rule keccakCheck(method f, env e){ address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; address targetRand; uint256 valueRand; bytes dataRand; bytes32 predecessorRand; bytes32 saltRand; - require data.length < 4; + require data.length < 7; // uint256 freshIndex; // require freshIndex <= data.length @@ -111,7 +112,7 @@ rule unsetPendingTransitionGeneral(method f, env e){ } -// STATUS - +// STATUS - verified // unset() -> pending() via schedule() and scheduleBatch() only rule unsetPendingTransitionMethods(method f, env e){ bytes32 id; @@ -178,8 +179,8 @@ rule doneToNothingTransition(method f, env e){ // STATUS - verified -// only TimelockController contract can change minDealy -rule minDealyOnlyChange(method f, env e){ +// only TimelockController contract can change minDelay +rule minDelayOnlyChange(method f, env e){ uint256 delayBefore = _minDelay(); calldataarg args; @@ -191,7 +192,7 @@ rule minDealyOnlyChange(method f, env e){ } -// STATUS - in progress (need working hash) +// STATUS - in progress // execute() is the only way to set timestamp to 1 rule getTimestampOnlyChange(method f, env e){ bytes32 id; @@ -211,7 +212,7 @@ rule getTimestampOnlyChange(method f, env e){ } -// STATUS - in progress (need working hash) +// STATUS - verified // scheduled operation timestamp == block.timestamp + delay (kind of unit test) rule scheduleCheck(method f, env e){ bytes32 id; @@ -219,16 +220,15 @@ rule scheduleCheck(method f, env e){ 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"; + assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls"; } -// STATUS - in progress (need working hash) +// STATUS - verified // 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; @@ -243,9 +243,9 @@ rule cannotCallExecute(method f, env e){ } -// STATUS - in progress +// STATUS - verified // in unset() execute() reverts -rule executeRevertFromUnset(method f, env e, env e2){ +rule executeRevertsFromUnset(method f, env e, env e2){ address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; bytes32 id; @@ -258,9 +258,9 @@ rule executeRevertFromUnset(method f, env e, env e2){ } -// STATUS - +// STATUS - verified // Execute reverts => state returns to pending -rule executeRevertEffectCheck(method f, env e){ +rule executeRevertsEffectCheck(method f, env e){ address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; bytes32 id; @@ -289,21 +289,47 @@ rule cancelledNotExecuted(method f, env e){ } -// STATUS - in progress (add schedule batch) +// STATUS - broken // Only proposers can schedule an operation -rule onlyProposer(method f, env e){ +rule onlyProposerCertorafallbackFail(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes32, bytes32, bytes32, uint256).selector + || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } { 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); + // hashIdCorrelation(id, target, value, data, predecessor, salt); + + _checkRole@withrevert(e, PROPOSER_ROLE()); + + bool isCheckRoleReverted = lastReverted; + + // schedule@withrevert(e, target, value, data, predecessor, salt, delay); + + calldataarg args; + f@withrevert(e, args); + + bool isScheduleReverted = lastReverted; + + assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +} + + +// STATUS - verified +// Only proposers can schedule an operation +rule onlyProposer1(method f, env e){ + bytes32 id; + bytes32 role; + // address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + address[] targets; uint256[] values; bytes[] datas; bytes32 predecessor; bytes32 salt; uint256 delay; + + // hashIdCorrelation(id, target, value, data, predecessor, salt); - AC._checkRole@withrevert(e, role); + _checkRole@withrevert(e, PROPOSER_ROLE()); bool isCheckRoleReverted = lastReverted; - schedule@withrevert(e, target, value, data, predecessor, salt, delay); + // schedule@withrevert(e, target, value, data, predecessor, salt, delay); + scheduleBatch@withrevert(e, targets, values, datas, predecessor, salt, delay); bool isScheduleReverted = lastReverted;