From 75417fbf9f6660c32fe42e20444db51f8d8cc3c1 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 8 Apr 2022 15:38:26 +0100 Subject: [PATCH 1/3] finilized rules --- certora/scripts/verifyERC20Wrapper.sh | 2 +- certora/scripts/verifyTimelock.sh | 1 + certora/specs/AccessControl.spec | 4 +- certora/specs/ERC1155.spec | 67 ++--- certora/specs/ERC20Wrapper.spec | 16 +- certora/specs/TimelockController.spec | 411 +++++++++++++------------- 6 files changed, 246 insertions(+), 255 deletions(-) diff --git a/certora/scripts/verifyERC20Wrapper.sh b/certora/scripts/verifyERC20Wrapper.sh index c4aaef9ff..15654d84e 100644 --- a/certora/scripts/verifyERC20Wrapper.sh +++ b/certora/scripts/verifyERC20Wrapper.sh @@ -6,5 +6,5 @@ certoraRun \ --optimistic_loop \ --staging \ --rule_sanity \ - --msg "wrapper spec sanity check fixes" + --msg "ERC20wrapper spec" \ No newline at end of file diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh index 93bb92f75..2876d5f92 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -6,6 +6,7 @@ certoraRun \ --loop_iter 3 \ --staging alex/new-dt-hashing-alpha \ --rule_sanity \ + --settings -byteMapHashingPrecision=32 \ --rule "$1" \ --msg "$1" \ No newline at end of file diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec index 83f925d86..b57ce3113 100644 --- a/certora/specs/AccessControl.spec +++ b/certora/specs/AccessControl.spec @@ -11,7 +11,7 @@ methods { // STATUS - verified -// check onlyRole modifier for grantRole() +// If `onlyRole` modifier reverts then `grantRole()` reverts rule onlyRoleModifierCheckGrant(env e){ bytes32 role; address account; @@ -58,7 +58,7 @@ rule grantRoleEffect(env e){ // STATUS - verified -// grantRole() does not affect another accounts +// revokeRole() does not affect another accounts rule revokeRoleEffect(env e){ bytes32 role; address account; bytes32 anotherRole; address nonEffectedAcc; diff --git a/certora/specs/ERC1155.spec b/certora/specs/ERC1155.spec index 3ecca54ca..9b5839031 100644 --- a/certora/specs/ERC1155.spec +++ b/certora/specs/ERC1155.spec @@ -52,7 +52,7 @@ rule onlyOwnerCanApprove(env e){ // STATUS - verified -// chech in which scenarios (if any) isApprovedForAll() revertes +// Chech that isApprovedForAll() revertes in planned scenarios and no more. rule approvalRevertCases(env e){ address account; address operator; isApprovedForAll@withrevert(account, operator); @@ -104,7 +104,7 @@ rule unexpectedBalanceChange(method f, env e) // STATUS - verified -// chech in which scenarios balanceOf() revertes +// Chech that `balanceOf()` revertes in planned scenarios and no more (only if `account` is 0) rule balanceOfRevertCases(env e){ address account; uint256 id; balanceOf@withrevert(account, id); @@ -113,7 +113,7 @@ rule balanceOfRevertCases(env e){ // STATUS - verified -// chech in which scenarios balanceOfBatch() revertes +// Chech that `balanceOfBatch()` revertes in planned scenarios and no more (only if at least one of `account`s is 0) rule balanceOfBatchRevertCases(env e){ address[] accounts; uint256[] ids; address account1; address account2; address account3; @@ -131,7 +131,7 @@ rule balanceOfBatchRevertCases(env e){ ///////////////////////////////////////////////// -// Transfer (14/14) +// Transfer (13/13) ///////////////////////////////////////////////// @@ -178,7 +178,7 @@ rule transferCorrectness(env e){ // STATUS - verified -// cannot transfer more than allowed (safeBatchTransferFrom version) +// safeBatchTransferFrom updates `from` and `to` balances) rule transferBatchCorrectness(env e){ address from; address to; uint256[] ids; uint256[] amounts; bytes data; uint256 idToCheck1; uint256 amountToCheck1; @@ -230,7 +230,6 @@ rule cannotTransferMoreSingle(env e){ safeTransferFrom@withrevert(e, from, to, id, amount, data); assert amount > balanceBefore => lastReverted, "Achtung! Scammer!"; - assert to == 0 => lastReverted, "Achtung! Scammer!"; } @@ -258,21 +257,6 @@ rule cannotTransferMoreBatch(env e){ } -// STATUS - verified -// safeBatchTransferFrom should revert if `to` is 0 address or if arrays length is different -rule revertOfTransferBatch(env e){ - address from; address to; uint256[] ids; uint256[] amounts; bytes data; - - require ids.length < 100000000; - require amounts.length < 100000000; - - safeBatchTransferFrom@withrevert(e, from, to, ids, amounts, data); - - assert ids.length != amounts.length => lastReverted, "Achtung! Scammer!"; - assert to == 0 => lastReverted, "Achtung! Scammer!"; -} - - // STATUS - verified // Sender calling safeTransferFrom should only reduce 'from' balance and not other's if sending amount is greater than 0 rule transferBalanceReduceEffect(env e){ @@ -293,7 +277,7 @@ rule transferBalanceReduceEffect(env e){ // STATUS - verified -// Sender calling safeTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0 +// Sender calling safeTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 rule transferBalanceIncreaseEffect(env e){ address from; address to; address other; uint256 id; uint256 amount; @@ -338,7 +322,7 @@ rule transferBatchBalanceFromEffect(env e){ // STATUS - verified -// Sender calling safeBatchTransferFrom should only reduce 'to' balance and not other's if sending amount is greater than 0 +// Sender calling safeBatchTransferFrom should only increase 'to' balance and not other's if sending amount is greater than 0 rule transferBatchBalanceToEffect(env e){ address from; address to; address other; uint256[] ids; uint256[] amounts; @@ -434,12 +418,12 @@ rule noTransferBatchEffectOnApproval(env e){ ///////////////////////////////////////////////// -// Mint (9/9) +// Mint (7/9) ///////////////////////////////////////////////// // STATUS - verified -// mint additivity +// Additivity of _mint: _mint(a); _mint(b) has same effect as _mint(a+b) rule mintAdditivity(env e){ address to; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; bytes data; require amount == amount1 + amount2; @@ -459,8 +443,8 @@ rule mintAdditivity(env e){ } -// STATUS - verified -// mint should revert if `from` is 0 +// STATUS - verified +// Chech that `_mint()` revertes in planned scenario(s) (only if `to` is 0) rule mintRevertCases(env e){ address to; uint256 id; uint256 amount; bytes data; @@ -471,28 +455,27 @@ rule mintRevertCases(env e){ // STATUS - verified -// mintBatch should revert if `from` is 0 or arrays have different length +// Chech that `_mintBatch()` revertes in planned scenario(s) (only if `to` is 0 or arrays have different length) rule mintBatchRevertCases(env e){ address to; uint256[] ids; uint256[] amounts; bytes data; - require ids.length < 100000000; - require amounts.length < 100000000; + require ids.length < 1000000000; + require amounts.length < 1000000000; _mintBatch@withrevert(e, to, ids, amounts, data); - assert to == 0 => lastReverted, "Should revert"; - assert ids.length != amounts.length => lastReverted, "Should revert"; + assert (ids.length != amounts.length || to == 0) => lastReverted, "Should revert"; } // STATUS - verified -// check that mint updates `to` balance correctly +// Check that mint updates `to` balance correctly rule mintCorrectWork(env e){ address to; uint256 id; uint256 amount; bytes data; uint256 otherBalanceBefore = balanceOf(to, id); - _mint(e, to, id, amount, data); + _mint(e, to, id, amount, data); uint256 otherBalanceAfter = balanceOf(to, id); @@ -534,7 +517,7 @@ rule mintBatchCorrectWork(env e){ // STATUS - verified -// the user cannot mint more than max_uint256 +// The user cannot mint more than max_uint256 rule cantMintMoreSingle(env e){ address to; uint256 id; uint256 amount; bytes data; @@ -571,7 +554,7 @@ rule cantMintMoreBatch(env e){ // STATUS - verified -// mint changes only `to` balance +// `_mint()` changes only `to` balance rule cantMintOtherBalances(env e){ address to; uint256 id; uint256 amount; bytes data; address other; @@ -618,7 +601,7 @@ rule cantMintBatchOtherBalances(env e){ // STATUS - verified -// burn additivity +// Additivity of _burn: _burn(a); _burn(b) has same effect as _burn(a+b) rule burnAdditivity(env e){ address from; uint256 id; uint256 amount; uint256 amount1; uint256 amount2; require amount == amount1 + amount2; @@ -639,7 +622,7 @@ rule burnAdditivity(env e){ // STATUS - verified -// burn should revert if `from` is 0 +// Chech that `_burn()` revertes in planned scenario(s) (if `from` is 0) rule burnRevertCases(env e){ address from; uint256 id; uint256 amount; @@ -650,16 +633,16 @@ rule burnRevertCases(env e){ // STATUS - verified -// burnBatch should revert if `from` is 0 or arrays have different length +// Chech that `balanceOf()` revertes in planned scenario(s) (if `from` is 0 or arrays have different length) rule burnBatchRevertCases(env e){ address from; uint256[] ids; uint256[] amounts; - require ids.length < 100000000; + require ids.length < 1000000000; + require amounts.length < 1000000000; _burnBatch@withrevert(e, from, ids, amounts); - assert from == 0 => lastReverted, "Should revert"; - assert ids.length != amounts.length => lastReverted, "Should revert"; + assert (from == 0 || ids.length != amounts.length) => lastReverted, "Should revert"; } diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 3ea288545..01c1b4295 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -40,7 +40,7 @@ invariant underTotalAndContractBalanceOfCorrelation(env e) // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecBasic(env e){ address account; uint256 amount; @@ -64,11 +64,10 @@ rule depositForSpecBasic(env e){ // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecWrapper(env e){ address account; uint256 amount; - // require e.msg.sender != currentContract; require underlying() != currentContract; uint256 wrapperUserBalanceBefore = balanceOf(e, account); @@ -88,7 +87,7 @@ rule depositForSpecWrapper(env e){ // STATUS - verified -// check correct values update by depositFor() +// Check that values are updated correctly by `depositFor()` rule depositForSpecUnderlying(env e){ address account; uint256 amount; @@ -116,7 +115,7 @@ rule depositForSpecUnderlying(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// Check that values are updated correctly by `withdrawTo()` rule withdrawToSpecBasic(env e){ address account; uint256 amount; @@ -136,7 +135,7 @@ rule withdrawToSpecBasic(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// Check that values are updated correctly by `withdrawTo()` rule withdrawToSpecWrapper(env e){ address account; uint256 amount; @@ -159,7 +158,7 @@ rule withdrawToSpecWrapper(env e){ // STATUS - verified -// check correct values update by withdrawTo() +// cCheck that values are updated correctly by `withdrawTo()` rule withdrawToSpecUnderlying(env e){ address account; uint256 amount; @@ -189,14 +188,13 @@ rule withdrawToSpecUnderlying(env e){ // STATUS - verified -// check correct values update by _recover() +// Check that values are updated correctly by `_recover()` rule recoverSpec(env e){ address account; uint256 amount; uint256 wrapperTotalBefore = totalSupply(e); uint256 wrapperUserBalanceBefore = balanceOf(e, account); uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); - uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 9e08fcf98..fbce17bfd 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -5,7 +5,11 @@ methods { _minDelay() returns(uint256) envfree getMinDelay() returns(uint256) envfree hashOperation(address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt) returns(bytes32) envfree - + isOperation(bytes32) returns(bool) envfree + isOperationPending(bytes32) returns(bool) envfree + isOperationDone(bytes32) returns(bool) envfree + + isOperationReady(bytes32) returns(bool) cancel(bytes32) schedule(address, uint256, bytes32, bytes32, bytes32, uint256) execute(address, uint256, bytes, bytes32, bytes32) @@ -13,23 +17,6 @@ methods { _checkRole(bytes32) => DISPATCHER(true) } -//////////////////////////////////////////////////////////////////////////// -// 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(); - //////////////////////////////////////////////////////////////////////////// @@ -38,7 +25,7 @@ definition done(bytes32 id) returns bool = function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){ - require data.length < 7; + require data.length < 32; require hashOperation(target, value, data, predecessor, salt) == id; } @@ -56,15 +43,35 @@ function executionsCall(method f, env e, address target, uint256 value, bytes da } } + + //////////////////////////////////////////////////////////////////////////// -// Ghosts // +// Invariants // //////////////////////////////////////////////////////////////////////////// +// STATUS - verified +// `isOperation()` correctness check +invariant operationCheck(bytes32 id) + getTimestamp(id) > 0 <=> isOperation(id) -//////////////////////////////////////////////////////////////////////////// -// Invariants // -//////////////////////////////////////////////////////////////////////////// + +// STATUS - verified +// `isOperationPending()` correctness check +invariant pendingCheck(bytes32 id) + getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id) + + +// STATUS - verified +// `isOperationReady()` correctness check +invariant readyCheck(env e, bytes32 id) + (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id) + + +// STATUS - verified +// `isOperationDone()` correctness check +invariant doneCheck(bytes32 id) + getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id) @@ -73,102 +80,81 @@ function executionsCall(method f, env e, address target, uint256 value, bytes da //////////////////////////////////////////////////////////////////////////// -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 < 7; - // uint256 freshIndex; - // require freshIndex <= data.length - - // require target != targetRand || value != valueRand || data[freshIndex] != dataRand[freshIndex] || predecessor != predecessorRand || salt != saltRand; - - bytes32 a = hashOperation(target, value, data, predecessor, salt); - bytes32 b = hashOperation(target, value, data, predecessor, salt); - // bytes32 c = hashOperation(targetRand, valueRand, dataRand, predecessorRand, saltRand); - - assert a == b, "hashes are different"; - // assert a != c, "hashes are the same"; -} - - ///////////////////////////////////////////////////////////// // STATE TRANSITIONS ///////////////////////////////////////////////////////////// // STATUS - verified -// unset() -> unset() || pending() only +// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only rule unsetPendingTransitionGeneral(method f, env e){ bytes32 id; - require unset(id); + require !isOperation(id); require e.block.timestamp > 1; calldataarg args; f(e, args); - assert pending(id) || unset(id); + assert isOperationPending(id) || !isOperation(id); } // STATUS - verified -// unset() -> pending() via schedule() and scheduleBatch() only +// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only rule unsetPendingTransitionMethods(method f, env e){ bytes32 id; - require unset(id); + require !isOperation(id); calldataarg args; f(e, args); - bool tmp = pending(id); - - assert pending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector + assert isOperationPending(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 +// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only rule readyDoneTransition(method f, env e){ bytes32 id; - require ready(id, e); + require isOperationReady(e, id); 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!"; + assert isOperationDone(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector + || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not isOperationDone yet!"; } // STATUS - verified -// pending() -> cancelled() via cancel() only +// isOperationPending() -> cancelled() via cancel() only rule pendingCancelledTransition(method f, env e){ bytes32 id; - require pending(id); + require isOperationPending(id); calldataarg args; f(e, args); - assert unset(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; + assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?"; } // STATUS - verified -// done() -> nowhere +// isOperationDone() -> nowhere rule doneToNothingTransition(method f, env e){ bytes32 id; - require done(id); + require isOperationDone(id); calldataarg args; f(e, args); - assert done(id), "Did you find a way to escape? There is no way! HA-HA-HA"; + assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA"; } @@ -192,7 +178,170 @@ rule minDelayOnlyChange(method f, env e){ } -// STATUS - in progress +// STATUS - verified +// 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; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls"; +} + + +// STATUS - verified +// Cannot call `execute()` on a isOperationPending (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 isOperationPending(id) && !isOperationReady(e, id); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Cannot call `execute()` on a !isOperation operation +rule executeRevertsFromUnset(method f, env e, env e2){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require !isOperation(id); + + execute@withrevert(e, target, value, data, predecessor, salt); + + assert lastReverted, "you go against execution nature"; +} + + +// STATUS - verified +// Execute reverts => state returns to isOperationPending +rule executeRevertsEffectCheck(method f, env e){ + address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt; + bytes32 id; + + hashIdCorrelation(id, target, value, data, predecessor, salt); + require isOperationPending(id) && !isOperationReady(e, id); + + execute@withrevert(e, target, value, data, predecessor, salt); + bool reverted = lastReverted; + + assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature"; +} + + +// STATUS - verified +// Canceled operations cannot be executed → can’t move from canceled to isOperationDone +rule cancelledNotExecuted(method f, env e){ + bytes32 id; + + require !isOperation(id); + require e.block.timestamp > 1; + + calldataarg args; + f(e, args); + + assert !isOperationDone(id), "The ship is not a creature of the air"; +} + + +// STATUS - verified +// Only proposers can schedule +rule onlyProposer(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes, 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; + + _checkRole@withrevert(e, PROPOSER_ROLE()); + + bool isCheckRoleReverted = lastReverted; + + calldataarg args; + f@withrevert(e, args); + + bool isScheduleReverted = lastReverted; + + assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected"; +} + + +// STATUS - verified +// if `ready` then has waited minimum period after isOperationPending() +rule cooldown(method f, env e, env e2){ + bytes32 id; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + uint256 minDelay = getMinDelay(); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + calldataarg args; + f(e, args); + + assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready"; +} + + +// STATUS - verified +// `schedule()` should change only one id's timestamp +rule scheduleChange(env e){ + bytes32 id; bytes32 otherId; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay; + + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + schedule(e, target, value, data, predecessor, salt, delay); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} + + +// STATUS - verified +// `execute()` should change only one id's timestamp +rule executeChange(env e){ + bytes32 id; bytes32 otherId; + address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + execute(e, target, value, data, predecessor, salt); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} + + +// STATUS - verified +// `cancel()` should change only one id's timestamp +rule cancelChange(env e){ + bytes32 id; bytes32 otherId; + + uint256 otherIdTimestampBefore = getTimestamp(otherId); + + cancel(e, id); + + assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; +} + + + + + + +// STATUS - in progress // execute() is the only way to set timestamp to 1 rule getTimestampOnlyChange(method f, env e){ bytes32 id; @@ -210,143 +359,3 @@ rule getTimestampOnlyChange(method f, env e){ 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 - verified -// 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; - hashIdCorrelation(id, target, value, data, predecessor, salt); - - schedule(e, target, value, data, predecessor, salt, delay); - - assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls"; -} - - -// 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; - 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 - verified -// in unset() execute() reverts -rule executeRevertsFromUnset(method f, env e, env e2){ - 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 executeRevertsEffectCheck(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); - bool reverted = lastReverted; - - 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 - broken -// Only proposers can schedule an operation -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; - - // 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); - - _checkRole@withrevert(e, PROPOSER_ROLE()); - - bool isCheckRoleReverted = lastReverted; - - // schedule@withrevert(e, target, value, data, predecessor, salt, delay); - scheduleBatch@withrevert(e, targets, values, datas, 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 From 66c72f2b5d0199ed6059a6632ad900725849100b Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 8 Apr 2022 20:52:38 +0100 Subject: [PATCH 2/3] CI preparations --- certora/scripts/verifyAccessControl.sh | 5 ++--- certora/scripts/verifyAllSasha.sh | 5 +++++ certora/scripts/verifyERC1155.sh | 6 ++---- certora/scripts/verifyERC20FlashMint.sh | 5 ++--- certora/scripts/verifyERC20Wrapper.sh | 5 ++--- certora/scripts/verifyTimelock.sh | 4 +--- certora/specs/ERC20Wrapper.spec | 1 + certora/specs/RulesInProgress.spec | 26 ++++++++++++++++++++++++- certora/specs/TimelockController.spec | 24 ----------------------- 9 files changed, 40 insertions(+), 41 deletions(-) create mode 100644 certora/scripts/verifyAllSasha.sh diff --git a/certora/scripts/verifyAccessControl.sh b/certora/scripts/verifyAccessControl.sh index 6b1a7ba05..eb706d063 100644 --- a/certora/scripts/verifyAccessControl.sh +++ b/certora/scripts/verifyAccessControl.sh @@ -3,7 +3,6 @@ certoraRun \ --verify AccessControlHarness:certora/specs/AccessControl.spec \ --solc solc8.2 \ --optimistic_loop \ - --staging \ - --rule_sanity \ - --msg "modifier check" + --cloud \ + --msg "AccessControl verification" \ No newline at end of file diff --git a/certora/scripts/verifyAllSasha.sh b/certora/scripts/verifyAllSasha.sh new file mode 100644 index 000000000..e87893bf9 --- /dev/null +++ b/certora/scripts/verifyAllSasha.sh @@ -0,0 +1,5 @@ +sh certora/scripts/verifyTimelock.sh +sh certora/scripts/verifyERC1155.sh +sh certora/scripts/verifyERC20FlashMint.sh +sh certora/scripts/verifyERC20Wrapper.sh +sh certora/scripts/verifyAccessControl.sh diff --git a/certora/scripts/verifyERC1155.sh b/certora/scripts/verifyERC1155.sh index 169df616d..84c59fc47 100644 --- a/certora/scripts/verifyERC1155.sh +++ b/certora/scripts/verifyERC1155.sh @@ -4,8 +4,6 @@ certoraRun \ --solc solc8.2 \ --optimistic_loop \ --loop_iter 3 \ - --staging \ - --rule_sanity \ - --rule "$1" \ - --msg "$1 check" + --cloud \ + --msg "ERC1155 verification" \ No newline at end of file diff --git a/certora/scripts/verifyERC20FlashMint.sh b/certora/scripts/verifyERC20FlashMint.sh index cd29f5b1a..0af81e006 100644 --- a/certora/scripts/verifyERC20FlashMint.sh +++ b/certora/scripts/verifyERC20FlashMint.sh @@ -4,7 +4,6 @@ certoraRun \ --verify ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec \ --solc solc8.2 \ --optimistic_loop \ - --staging \ - --rule_sanity \ - --msg "flashMint" + --cloud \ + --msg "ERC20FlashMint verification" \ No newline at end of file diff --git a/certora/scripts/verifyERC20Wrapper.sh b/certora/scripts/verifyERC20Wrapper.sh index 15654d84e..e1ef85ef0 100644 --- a/certora/scripts/verifyERC20Wrapper.sh +++ b/certora/scripts/verifyERC20Wrapper.sh @@ -4,7 +4,6 @@ certoraRun \ --verify ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec \ --solc solc8.2 \ --optimistic_loop \ - --staging \ - --rule_sanity \ - --msg "ERC20wrapper spec" + --cloud \ + --msg "ERC20Wrapper verification" \ No newline at end of file diff --git a/certora/scripts/verifyTimelock.sh b/certora/scripts/verifyTimelock.sh index 2876d5f92..5afc11911 100644 --- a/certora/scripts/verifyTimelock.sh +++ b/certora/scripts/verifyTimelock.sh @@ -5,8 +5,6 @@ certoraRun \ --optimistic_loop \ --loop_iter 3 \ --staging alex/new-dt-hashing-alpha \ - --rule_sanity \ --settings -byteMapHashingPrecision=32 \ - --rule "$1" \ - --msg "$1" + --msg "TimelockController verification" \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 01c1b4295..bc95288e9 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -195,6 +195,7 @@ rule recoverSpec(env e){ uint256 wrapperTotalBefore = totalSupply(e); uint256 wrapperUserBalanceBefore = balanceOf(e, account); uint256 wrapperSenderBalanceBefore = balanceOf(e, e.msg.sender); + uint256 underlyingThisBalanceBefore = underlyingBalanceOf(currentContract); mathint value = underlyingThisBalanceBefore - wrapperTotalBefore; diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec index cbad3336e..d0e2a6b74 100644 --- a/certora/specs/RulesInProgress.spec +++ b/certora/specs/RulesInProgress.spec @@ -136,4 +136,28 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { uint256 ps = proposalSnapshot(pId); assert tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId)), "bla bla bla"; -} \ No newline at end of file +} + + + +/////////////////// 2nd iteration with OZ ////////////////////////// + +// STATUS - in progress +// 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; + address[] targets; uint256[] values; bytes[] datas; + + require (targets[0] == target && values[0] == value && datas[0] == data) + || (targets[1] == target && values[1] == value && datas[1] == data) + || (targets[2] == target && values[2] == value && datas[2] == data); + + hashIdCorrelation(id, target, value, data, predecessor, salt); + + executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); + + 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?"; +} + diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index fbce17bfd..29aeaee69 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -335,27 +335,3 @@ rule cancelChange(env e){ assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings"; } - - - - - - -// STATUS - in progress -// 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; - address[] targets; uint256[] values; bytes[] datas; - - require (targets[0] == target && values[0] == value && datas[0] == data) - || (targets[1] == target && values[1] == value && datas[1] == data) - || (targets[2] == target && values[2] == value && datas[2] == data); - - hashIdCorrelation(id, target, value, data, predecessor, salt); - - executionsCall(f, e, target, value, data, predecessor, salt, delay, targets, values, datas); - - 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?"; -} From 741e9a8b6d1c210dd055661971b2092d1b341959 Mon Sep 17 00:00:00 2001 From: Aleksander Kryukov Date: Fri, 8 Apr 2022 20:57:53 +0100 Subject: [PATCH 3/3] timelock function moved --- certora/specs/RulesInProgress.spec | 13 +++++++++++++ certora/specs/TimelockController.spec | 14 -------------- 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/certora/specs/RulesInProgress.spec b/certora/specs/RulesInProgress.spec index d0e2a6b74..18a79d619 100644 --- a/certora/specs/RulesInProgress.spec +++ b/certora/specs/RulesInProgress.spec @@ -142,6 +142,19 @@ rule possibleTotalVotes(uint256 pId, uint8 sup, env e, method f) { /////////////////// 2nd iteration with OZ ////////////////////////// +function executionsCall(method f, env e, address target, uint256 value, bytes data, + bytes32 predecessor, bytes32 salt, uint256 delay, + address[] targets, uint256[] values, bytes[] datas) { + if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { + execute(e, target, value, data, predecessor, salt); + } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { + executeBatch(e, targets, values, datas, predecessor, salt); + } else { + calldataarg args; + f(e, args); + } +} + // STATUS - in progress // execute() is the only way to set timestamp to 1 rule getTimestampOnlyChange(method f, env e){ diff --git a/certora/specs/TimelockController.spec b/certora/specs/TimelockController.spec index 29aeaee69..2277fecb1 100644 --- a/certora/specs/TimelockController.spec +++ b/certora/specs/TimelockController.spec @@ -30,20 +30,6 @@ function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data } -function executionsCall(method f, env e, address target, uint256 value, bytes data, - bytes32 predecessor, bytes32 salt, uint256 delay, - address[] targets, uint256[] values, bytes[] datas) { - if (f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector) { - execute(e, target, value, data, predecessor, salt); - } else if (f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector) { - executeBatch(e, targets, values, datas, predecessor, salt); - } else { - calldataarg args; - f(e, args); - } -} - - //////////////////////////////////////////////////////////////////////////// // Invariants //