From 2e166ef880962fa8d1077351d1dcac1ff354797c Mon Sep 17 00:00:00 2001 From: Victor Martinez Date: Fri, 5 Aug 2022 15:16:57 +0200 Subject: [PATCH] added Certora Rules and invariants --- certora/scripts/setup.sh | 15 +- certora/specs/setup.spec | 480 ++++++++++++++++++++++++++++++++++++++- package.json | 4 - 3 files changed, 481 insertions(+), 18 deletions(-) diff --git a/certora/scripts/setup.sh b/certora/scripts/setup.sh index 03df365..56b5556 100644 --- a/certora/scripts/setup.sh +++ b/certora/scripts/setup.sh @@ -1,13 +1,2 @@ -if [[ "$1" ]] -then - RULE="--rule $1" -fi - -certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \ - --verify AaveTokenV3:certora/specs/setup.spec \ - $RULE \ - --solc solc8.13 \ - --optimistic_loop \ - --send_only \ - --cloud \ - --msg "AaveTokenV3:setup.spec $1" +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 --verify AaveTokenV3:certora/specs/setup.spec --solc solc815 --optimistic_loop --send_only --cloud --msg "AaveTokenV3:setup.spec" +certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 --verify AaveTokenV3:certora/specs/setup.spec --solc solc815 --optimistic_loop --send_only --cloud --msg "AaveTokenV3 setup" diff --git a/certora/specs/setup.spec b/certora/specs/setup.spec index 077401f..de4337e 100644 --- a/certora/specs/setup.spec +++ b/certora/specs/setup.spec @@ -135,4 +135,482 @@ hook Sstore _balances[KEY address user].balance uint104 balance */ invariant totalSupplyEqualsBalances() - sumBalances == totalSupply() \ No newline at end of file + sumBalances == totalSupply() + +//NEW RULES + +/** + 1- + Invariant: + Verify that zero address cannot have balance. + +*/ + +invariant zeroAddressHasNoBalance() + balanceOf(0) == 0 + +/** + 2- + Invariant: + Verify that zero address has no power. + +*/ +invariant zeroAddrNoPower() + getPowerCurrent(0, VOTING_POWER()) == 0 && getPowerCurrent(0, PROPOSITION_POWER()) == 0 + {preserved { + requireInvariant zeroAddressHasNoBalance(); + }} + +/** + 3- + Invariant: + Verify that the (voting power) of an address that isn't delegating his power and isn't calling any delegate function, equals (balance + delegatedVotingBalance). + +*/ +invariant accountVotingPower(address someone) + balanceOf(someone) + getDelegatedVotingBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, VOTING_POWER()) + //coverage of all fuctions except delegate ones + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + + {preserved { + //require user "someone" is not delegating before + require(!getDelegatingVoting(someone)); + }} + +/** + 4- + Invariant: + Verify that the (proposition power) of an address that isn't delegating his power and isn't calling any delegate function, equals (balance + delegatedPropositionBalance). + +*/ +invariant accountPropositionPower(address someone) + balanceOf(someone) + getDelegatedPropositionBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, PROPOSITION_POWER()) + //coverage of all fuctions except delegate ones + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + + {preserved { + //require user "someone" is not delegating before + require(!getDelegatingProposition(someone)); + }} + +/** + 5- + Invariant: + Verify that the (voting power) of an address that is delegating his power and isn't calling any delegate function, equals (delegatedVotingBalance) + +*/ +invariant delegatingAccountVotingPower(address someone) + getDelegatedVotingBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, VOTING_POWER()) + //coverage of all fuctions except delegate ones + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + + {preserved { + //require user "someone" is delegating before + require(getDelegatingVoting(someone)); + }} + +/** + 6- + Invariant: + Verify that the (proposition power) of an address that is delegating his power and isn't calling any delegate function, equals (delegatedPropositionBalance). + +*/ +invariant delegatingAccountPropositionPower(address someone) + getDelegatedPropositionBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, PROPOSITION_POWER()) + //coverage of all fuctions except delegate ones + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + + {preserved { + //require user "someone" is delegating before + require(getDelegatingProposition(someone)); + }} + + +/** + 7- + Invariant: + Verify that the (voting power) of an address that is delegating his power and calls a delegate function, equals (balance + delegatedVotingBalance) + +*/ +invariant delegatingAccountVotingPowerCallingDelegate(address someone) + balanceOf(someone) + getDelegatedVotingBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, VOTING_POWER()) + //coverage of delegate fuctions + filtered { + f -> f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + {preserved { + //require user "someone" is delegating before + require(getDelegatingVoting(someone)); + }} + +/** + 8- + Invariant: + Verify that the (Proposition power) of an address that is delegating his power and calls a delegate function, equals (balance + delegatedPropositionBalance) + +*/ +invariant delegatingAccountPropositionPowerCallingDelegate(address someone) + balanceOf(someone) + getDelegatedPropositionBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, PROPOSITION_POWER()) + //coverage of delegate fuctions + filtered { + f -> f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + {preserved { + //require user "someone" is delegating before + require(getDelegatingProposition(someone)); + }} + +/** + 9- + Invariant: + Verify that the (voting power) of an address that is not delegating his power and calls a delegate function, equals (delegatedVotingBalance) + +*/ +invariant noDelegatingAccountVotingPowerCallingDelegate(address someone) + getDelegatedVotingBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, VOTING_POWER()) + //coverage of delegate fuctions + filtered { + f -> f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + {preserved { + //require user "someone" is not delegating before + require(!getDelegatingVoting(someone)); + }} + +/** + 10- + Invariant + Verify that the (Proposition power) of an address that is not delegating his power and calls a delegate function, equals (delegatedPropositionBalance) + +*/ +invariant noDelegatingAccountPropositionPowerCallingDelegate(address someone) + getDelegatedPropositionBalance(someone)*DELEGATED_POWER_DIVIDER() == getPowerCurrent(someone, PROPOSITION_POWER()) + //coverage of delegate fuctions + filtered { + f -> f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector + } + {preserved { + //require user "someone" is not delegating before + require(!getDelegatingProposition(someone)); + }} + +/** + 11- + Verify that only ERC20 functions can change someone's balance. + +*/ +rule balanceChanges(address alice, method f) { + env e; + calldataarg args; + + uint aliceBalanceBefore = balanceOf(alice); + + f(e, args); + + uint aliceBalanceAfter = balanceOf(alice); + + // only these four function may change the delegate of an address + assert aliceBalanceBefore != aliceBalanceAfter => + f.selector == transfer(address,uint256).selector || + f.selector == transferFrom(address,address,uint256).selector; +} + +/** + 12- + The delegator can always revoke his voting power only by calling delegating functions + +*/ +rule checkRevokingVotingPower(address someone, method f) { + env e; + calldataarg args; + + //store voting delegating state before + bool delegatingStateBefore = getDelegatingVoting(someone); + //transacction + f(e, args); + //store voting delegating state after + bool delegatingStateAfter = getDelegatingVoting(someone); + + assert (delegatingStateBefore => (delegatingStateAfter || !delegatingStateAfter)); + //assert that any delagation granted can be rovoked or changed to another delegatee using delegate functions + assert ((delegatingStateBefore && !delegatingStateAfter )=> + f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector); +} + +/** + 13- + The delegator can always revoke his proposition power only by calling delegating functions + +*/ +rule checkRevokingPropositionPower(address someone, method f) { + env e; + calldataarg args; + + //store proposition delegating state before + bool delegatingStateBefore = getDelegatingProposition(someone); + //transacction + f(e, args); + //store proposition delegating state after + bool delegatingStateAfter = getDelegatingProposition(someone); + + assert (delegatingStateBefore => (delegatingStateAfter || !delegatingStateAfter)); + //assert that any delagation granted can be rovoked or changed to another delegatee using delegate functions + assert ((delegatingStateBefore && !delegatingStateAfter )=> + f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector || + f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector); +} + +/** + 14- + Any change to one type of delegation does not affect the other type + +*/ +rule checkIndividualDelegationChange(address bob){ + env e; + // delegate not to self or to zero + require bob != e.msg.sender && bob != 0; + uint8 delegateType; + + //powers before transaction + uint256 votingPowerBefore = getDelegatedVotingBalance(bob); + uint256 proposalPowerBefore = getDelegatedPropositionBalance(bob); + // avoid unrealistic delegated balance + require(votingPowerBefore < MAX_DELEGATED_BALANCE()); + require(proposalPowerBefore < MAX_DELEGATED_BALANCE()); + + // verify that the sender doesn't already delegate to bob + address delegatePropositionBefore = getPropositionDelegate(e.msg.sender); + address delegateVotingBefore = getVotingDelegate(e.msg.sender); + require delegatePropositionBefore != bob; + require delegateVotingBefore != bob; + + delegateByType(e, bob, delegateType); + + uint256 votingPowerAfter = getDelegatedVotingBalance(bob); + uint256 proposalPowerAfter = getDelegatedPropositionBalance(bob); + + + //verify that if the type selected is voting, proposition power has not change and viceversa + assert delegateType == VOTING_POWER() => proposalPowerBefore == proposalPowerAfter; + assert delegateType != VOTING_POWER() => votingPowerBefore == votingPowerAfter; +} + +/* + 15- + The voting delegatee of some account changes only if they are the one requesting it + +**/ +rule delegateeVotingChange(method f){ + address account; + env e; + calldataarg args; + + //check that both addresses are different + require account != e.msg.sender; + + //store delegatee of account before the transaction and require it is delegating + address delegateeBefore = getVotingDelegate(account); + require getDelegatingVoting(account); + + //call delegate transactions from e.msg.sender + f(e, args); + //only for Normal Delegate transanctions + require (f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector); + + //store delegatee of account after the transaction + address delegateeAfter = getVotingDelegate(account); + + //check account delegatee has not change + assert delegateeBefore == delegateeAfter; +} + +/* + 16- + The Proposition delegatee of some account changes only if they are the one requesting + +**/ +rule delegateePropositionChange(method f){ + address account; + env e; + calldataarg args; + + //check that both addresses are different + require account != e.msg.sender; + + //store delegatee of account before the transaction and require it is delegating + address delegateeBefore = getPropositionDelegate(account); + require getDelegatingProposition(account); + + //call delegate transactions from e.msg.sender + f(e, args); + //only for Normal Delegate transanctions + require (f.selector == delegate(address).selector || + f.selector == delegateByType(address,uint8).selector); + + //store delegatee of account after the transaction + address delegateeAfter = getPropositionDelegate(account); + + //check account delegatee has not change + assert delegateeBefore == delegateeAfter; +} + + +/* + 17- + With MetaDelegate functions if a user changes another account's voting delegatee, his delegatee wont change + +**/ +rule delegateeVotingMetaChange(method f){ + address account; + env e; + calldataarg args; + + //check that both addresses are different + require account != e.msg.sender; + + //store delegatees of account and msg.sender before transaction + address delegateeBefore = getVotingDelegate(account); + address delegateeBeforeSender = getVotingDelegate(e.msg.sender); + + //require account is delegating + require getDelegatingVoting(account); + + //Call Meta-delegate transactions from e.msg.sender + f(e, args); + require (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector); + + //store delegatees of account and msg.sender after transaction + address delegateeAfter = getVotingDelegate(account); + address delegateeAfterSender = getVotingDelegate(e.msg.sender); + + //if account delegate has changed msg.sender delegate should not change + assert delegateeBefore != delegateeAfter => delegateeBeforeSender == delegateeAfterSender; +} + +/* + 18- + With MetaDelegate functions if a user changes another account's delegatee, his delegatee wont change + +**/ +rule delegateePropositionMetaChange(method f){ + address account; + env e; + calldataarg args; + + //check that both addresses are different + require account != e.msg.sender; + + //store delegatees of account and msg.sender before transaction + address delegateeBefore = getPropositionDelegate(account); + address delegateeBeforeSender = getPropositionDelegate(e.msg.sender); + + //require account is delegating + require getDelegatingProposition(account); + + //Meta-delegate transactions + f(e, args); + require (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || + f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector); + + //store delegatees of account and msg.sender after transaction + address delegateeAfter = getPropositionDelegate(account); + address delegateeAfterSender = getPropositionDelegate(e.msg.sender); + + //if account delegate has changed msg.sender delegate should not change + assert delegateeBefore != delegateeAfter => delegateeBeforeSender == delegateeAfterSender; +} + +/* + 19- + Voting Power of a delegatee is always Equal or bigger than the balanace of the delegator + +*/ + +invariant VotingPowerEqualBiggerDelegator(address someone) + getDelegatedVotingBalance(getVotingDelegate(someone))*DELEGATED_POWER_DIVIDER() >= balanceOf(someone) + + //Filter out delegating and transfer functions that do internal changes on balances and delegating balances + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector && + f.selector != transfer(address,uint256).selector && + f.selector != transferFrom(address,address,uint256).selector && + f.selector != _governancePowerTransferByType(uint104,uint104,address,uint8).selector + } + //Require that delegator is delegating + {preserved { + require(getDelegatingVoting(someone)); + }} + +/* + 20- + Proposition Power of a delegatee is always Equal or bigger than the balanace of the delegator + +*/ + +invariant PropositionPowerEqualBiggerDelegator(address someone) + getDelegatedPropositionBalance(getPropositionDelegate(someone))*DELEGATED_POWER_DIVIDER() >= balanceOf(someone) + + //Filter out delegating and transfer functions that do internal changes on balances and delegating balances + filtered { + f -> f.selector != delegate(address).selector && + f.selector != delegateByType(address,uint8).selector && + f.selector != metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector && + f.selector != metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector && + f.selector != transfer(address,uint256).selector && + f.selector != transferFrom(address,address,uint256).selector && + f.selector != _governancePowerTransferByType(uint104,uint104,address,uint8).selector + } + //Require that delegator is delegating + {preserved { + require(getDelegatingProposition(someone)); + }} + + + + + + + + diff --git a/package.json b/package.json index a542486..2c63c08 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,2 @@ { - "devDependencies": { - "prettier": "^2.7.1", - "prettier-plugin-solidity": "^1.0.0-beta.19" - } }