From 3d2d6b2c3959317728fb2b8a4504f22a45862b0a Mon Sep 17 00:00:00 2001 From: fyang1024 Date: Mon, 27 Jun 2022 20:52:30 +1000 Subject: [PATCH 1/2] add more astETH rules --- certora/harness/DummyERC20Impl.sol | 2 +- certora/scripts/runFyang1024.sh | 13 ++ certora/specs/AStETH_fyang1024.spec | 211 ++++++++++++++++++++++++++++ 3 files changed, 225 insertions(+), 1 deletion(-) create mode 100644 certora/scripts/runFyang1024.sh create mode 100644 certora/specs/AStETH_fyang1024.spec diff --git a/certora/harness/DummyERC20Impl.sol b/certora/harness/DummyERC20Impl.sol index 247b3f93b..b16a56783 100644 --- a/certora/harness/DummyERC20Impl.sol +++ b/certora/harness/DummyERC20Impl.sol @@ -11,7 +11,7 @@ contract DummyERC20Impl is IERC20 { mapping (address => mapping (address => uint256)) allowances; string public name; - string public symbol;is + string public symbol; uint public decimals; function totalSupply() external view override returns (uint256) { diff --git a/certora/scripts/runFyang1024.sh b/certora/scripts/runFyang1024.sh new file mode 100644 index 000000000..a76670345 --- /dev/null +++ b/certora/scripts/runFyang1024.sh @@ -0,0 +1,13 @@ +if [[ "$1" ]] +then + RULE="--rule $1" +fi + +certoraRun certora/harness/AStETHHarness.sol certora/harness/IncentivesControllerMock.sol certora/harness/SymbolicLendingPool.sol certora/harness/DummyERC20A.sol certora/harness/DummyERC20B.sol \ + --verify AStETHHarness:certora/specs/AStETH_fyang1024.spec \ + --link AStETHHarness:UNDERLYING_ASSET_ADDRESS=DummyERC20A AStETHHarness:POOL=SymbolicLendingPool AStETHHarness:_incentivesController=IncentivesControllerMock AStETHHarness:RESERVE_TREASURY_ADDRESS=DummyERC20B SymbolicLendingPool:aToken=AStETHHarness SymbolicLendingPool:Asset=DummyERC20A \ + --solc solc6.12 \ + --optimistic_loop \ + --settings -smt_nonLinearArithmetic=true \ + $RULE \ + --msg "AStETH $RULE $2" diff --git a/certora/specs/AStETH_fyang1024.spec b/certora/specs/AStETH_fyang1024.spec new file mode 100644 index 000000000..b9d00fded --- /dev/null +++ b/certora/specs/AStETH_fyang1024.spec @@ -0,0 +1,211 @@ +import "./AStETH.spec" + +methods { + RESERVE_TREASURY_ADDRESS() returns (address) envfree +} + +/* + @Rule + + @Description: + scaledBalance / internalBalance should be always equal to scaledTotalSupply / internalTotalSupply, + that is, + internalBalance * scaledTotalSupply should be always equal to scaledBalance * internalTotalSupply, + similarly, + scaledBalance * totalSupply should be always equal to balance * scaledTotalSupply, and + internalBalance * totalSupply should be always equal to balance * internalTotalSupply + + @Formula: + { + _ATokenInternalBalance * _ATokenScaledTotalSupply == _ATokenScaledBalance * _ATokenInternalTotalSupply && + _ATokenScaledBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenScaledTotalSupply && + _ATokenInternalBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenInternalTotalSupply + } + + < call any function > + + { + ATokenInternalBalance_ * ATokenScaledTotalSupply_ == ATokenScaledBalance_ * ATokenInternalTotalSupply_ && + ATokenScaledBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenScaledTotalSupply_ && + ATokenInternalBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenInternalTotalSupply_ + } + + @Note: + + @Link: +*/ + +rule proportionalBalancesAndTotalSupplies(address user) { + + mathint _ATokenInternalBalance = internalBalanceOf(user); + mathint _ATokenScaledBalance = scaledBalanceOf(user); + mathint _ATokenBalance = balanceOf(user); + mathint _ATokenInternalTotalSupply = internalTotalSupply(); + mathint _ATokenScaledTotalSupply = scaledTotalSupply(); + mathint _ATokenTotalSupply = totalSupply(); + + require _ATokenInternalBalance * _ATokenScaledTotalSupply == _ATokenScaledBalance * _ATokenInternalTotalSupply; + require _ATokenScaledBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenScaledTotalSupply; + require _ATokenInternalBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenInternalTotalSupply; + + env e; calldataarg args; method f; + f(e, args); + + mathint ATokenInternalBalance_ = internalBalanceOf(user); + mathint ATokenScaledBalance_ = scaledBalanceOf(user); + mathint ATokenBalance_ = balanceOf(user); + mathint ATokenInternalTotalSupply_ = internalTotalSupply(); + mathint ATokenScaledTotalSupply_ = scaledTotalSupply(); + mathint ATokenTotalSupply_ = totalSupply(); + + assert ATokenInternalBalance_ * ATokenScaledTotalSupply_ == ATokenScaledBalance_ * ATokenInternalTotalSupply_; + assert ATokenScaledBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenScaledTotalSupply_; + assert ATokenInternalBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenInternalTotalSupply_; +} + +/* + @Rule + + @Description: + the mint function and the mintToTreasury function should be equivalent + + @Formula: + { + storage init = lastStorage + } + + mintToTreasury(amount, index) + mathint _ATokenInternalBalance = internalBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenScaledBalance = scaledBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenBalance = balanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenInternalTotalSupply = internalTotalSupply(); + mathint _ATokenScaledTotalSupply = scaledTotalSupply(); + mathint _ATokenTotalSupply = totalSupply(); + + mint(RESERVE_TREASURY_ADDRESS(), amount, index) at init + mathint ATokenInternalBalance_ = internalBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenScaledBalance_ = scaledBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenBalance_ = balanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenInternalTotalSupply_ = internalTotalSupply(); + mathint ATokenScaledTotalSupply_ = scaledTotalSupply(); + mathint ATokenTotalSupply_ = totalSupply(); + + { + _ATokenInternalBalance == ATokenInternalBalance_ && + _ATokenScaledBalance == ATokenScaledBalance_ && + _ATokenBalance == ATokenBalance_ && + _ATokenInternalTotalSupply == ATokenInternalTotalSupply_ && + _ATokenScaledTotalSupply == ATokenScaledTotalSupply_ && + _ATokenTotalSupply == ATokenTotalSupply_ + } + + @Note: + + @Link: +*/ + +rule equivalenceOfMint(uint256 amount, uint256 index) { + env e; + storage init = lastStorage; + + mintToTreasury(e, amount, index); + mathint _ATokenInternalBalance = internalBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenScaledBalance = scaledBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenBalance = balanceOf(RESERVE_TREASURY_ADDRESS()); + mathint _ATokenInternalTotalSupply = internalTotalSupply(); + mathint _ATokenScaledTotalSupply = scaledTotalSupply(); + mathint _ATokenTotalSupply = totalSupply(); + + mint(e, RESERVE_TREASURY_ADDRESS(), amount, index) at init; + mathint ATokenInternalBalance_ = internalBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenScaledBalance_ = scaledBalanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenBalance_ = balanceOf(RESERVE_TREASURY_ADDRESS()); + mathint ATokenInternalTotalSupply_ = internalTotalSupply(); + mathint ATokenScaledTotalSupply_ = scaledTotalSupply(); + mathint ATokenTotalSupply_ = totalSupply(); + + assert _ATokenInternalBalance == ATokenInternalBalance_ && + _ATokenScaledBalance == ATokenScaledBalance_ && + _ATokenBalance == ATokenBalance_ && + _ATokenInternalTotalSupply == ATokenInternalTotalSupply_ && + _ATokenScaledTotalSupply == ATokenScaledTotalSupply_ && + _ATokenTotalSupply == ATokenTotalSupply_; +} + +/* + @Rule + + @Description: + The balance of a receiver in transferOnLiquidation() should increase by amount + The balance of a sender in transferOnLiquidation() should decrease by amount + + @Formula: + { + sender != receiver; + } + + transferOnLiquidation(sender, receiver, amount) + + { + balanceOfSenderAfter == balanceOfSenderBefore - amount; + balanceOfReceiverAfter == balanceOfReceiverBefore + amount; + totalSupplyAfter == totalSupplyBefore; + } + + @Note: + + @Link: +*/ + +rule integrityOfTransferOnLiquidation(address sender, address receiver, uint256 amount) { + require sender != receiver; + + mathint totalSupplyBefore = totalSupply(); + mathint balanceOfSenderBefore = balanceOf(sender); + mathint balanceOfReceiverBefore = balanceOf(receiver); + + env e; + transferOnLiquidation(e, sender, receiver, amount); + + mathint totalSupplyAfter = totalSupply(); + mathint balanceOfSenderAfter = balanceOf(sender); + mathint balanceOfReceiverAfter = balanceOf(receiver); + + assert balanceOfSenderAfter == balanceOfSenderBefore - amount; + assert balanceOfReceiverAfter == balanceOfReceiverBefore + amount; + assert totalSupplyAfter == totalSupplyBefore; +} + +/* + @Rule + + @Description: + If sender is the same as receiver or the amount is 0, transferOnLiquidation should revert. + Liquidating astETH to the account itself does not make sense and should fail the transaction. + Liquidating 0 value does not make sense either and should fail the transaction. + ** The code violates the rule, which I think should be fixed. + + @Formula: + { + sender == receiver || amount == 0; + } + + transferOnLiquidation(sender, receiver, amount) + + { + lastReverted + } + + @Note: + + @Link: +*/ + +rule invalidLiquidationShouldRevert(address sender, address receiver, uint256 amount) { + require sender == receiver || amount == 0; + + env e; + transferOnLiquidation@withrevert(e, sender, receiver, amount); + + assert lastReverted; +} \ No newline at end of file From 2a2d075784883e7e14ba04c957dccb433a8cf07f Mon Sep 17 00:00:00 2001 From: fyang1024 Date: Mon, 27 Jun 2022 21:05:40 +1000 Subject: [PATCH 2/2] add burnMintInvertability rule --- certora/specs/AStETH_fyang1024.spec | 56 +++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/certora/specs/AStETH_fyang1024.spec b/certora/specs/AStETH_fyang1024.spec index b9d00fded..0e536928c 100644 --- a/certora/specs/AStETH_fyang1024.spec +++ b/certora/specs/AStETH_fyang1024.spec @@ -63,6 +63,62 @@ rule proportionalBalancesAndTotalSupplies(address user) { assert ATokenInternalBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenInternalTotalSupply_; } +/* + @Rule + + @Description: + Burning and minting are invert operations within the AStETH context + + @Formula: + { + + } + + burn() + mint() + + { + _ATokenInternalBalance == ATokenInternalBalance_ && + _ATokenScaledBalance == ATokenScaledBalance_ && + _ATokenBalance == ATokenBalance_ && + _ATokenInternalTotalSupply == ATokenInternalTotalSupply_ && + _ATokenScaledTotalSupply == ATokenScaledTotalSupply_ && + _ATokenTotalSupply == ATokenTotalSupply_ + } + + @Note: + + @Link: +*/ + +rule burnMintInvertability(address user, uint256 amount, uint256 index, address receiver){ + env e; + + mathint _ATokenInternalBalance = internalBalanceOf(user); + mathint _ATokenScaledBalance = scaledBalanceOf(user); + mathint _ATokenBalance = balanceOf(user); + mathint _ATokenInternalTotalSupply = internalTotalSupply(); + mathint _ATokenScaledTotalSupply = scaledTotalSupply(); + mathint _ATokenTotalSupply = totalSupply(); + + burn(e, user, receiver, amount, index); + mint(e, user, amount, index); + + mathint ATokenInternalBalance_ = internalBalanceOf(user); + mathint ATokenScaledBalance_ = scaledBalanceOf(user); + mathint ATokenBalance_ = balanceOf(user); + mathint ATokenInternalTotalSupply_ = internalTotalSupply(); + mathint ATokenScaledTotalSupply_ = scaledTotalSupply(); + mathint ATokenTotalSupply_ = totalSupply(); + + assert _ATokenInternalBalance == ATokenInternalBalance_; + assert _ATokenScaledBalance == ATokenScaledBalance_; + assert _ATokenBalance == ATokenBalance_; + assert _ATokenInternalTotalSupply == ATokenInternalTotalSupply_; + assert _ATokenScaledTotalSupply == ATokenScaledTotalSupply_; + assert _ATokenTotalSupply == ATokenTotalSupply_; +} + /* @Rule