From df8e27f65f9050f62d75bb06e8a3329fca088a10 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Wed, 16 Aug 2023 10:32:28 +0200 Subject: [PATCH 1/2] More generic rules --- certora/specs/Blue.spec | 126 +++++++++++++++++++++++++++++++++++++- certora/specs/Health.spec | 36 ++++++++++- 2 files changed, 159 insertions(+), 3 deletions(-) diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec index 69e5408d5..cc598dd25 100644 --- a/certora/specs/Blue.spec +++ b/certora/specs/Blue.spec @@ -1,9 +1,11 @@ methods { - function supply(MorphoHarness.Market, uint256, uint256, address, bytes) external; function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree; function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function totalSupply(MorphoHarness.Id) external returns uint256 envfree; function totalBorrow(MorphoHarness.Id) external returns uint256 envfree; + function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address user) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address user) external returns uint256 envfree; function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; @@ -11,6 +13,7 @@ methods { function idToMarket(MorphoHarness.Id) external returns (address, address, address, address, uint256) envfree; function isAuthorized(address, address) external returns bool envfree; + function isHealthy(MorphoHarness.Market, address user) external returns bool envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function isLltvEnabled(uint256) external returns bool envfree; function isIrmEnabled(address) external returns bool envfree; @@ -167,3 +170,124 @@ rule marketIdUnique() { assert market1.irm == market2.irm; assert market1.lltv == market2.lltv; } + +rule onlyUserCanAuthorizeWithoutSig(method f, calldataarg data) +filtered { + f -> !f.isView && f.selector != sig:setAuthorizationWithSig(MorphoHarness.Authorization memory, MorphoHarness.Signature calldata).selector +} +{ + address user; + address someone; + env e; + + require user != e.msg.sender; + bool authorizedBefore = isAuthorized(user, someone); + + f(e, data); + + assert isAuthorized(user, someone) == authorizedBefore; +} + +rule supplyMovesTokensAndIncreasesShares() { + MorphoHarness.Market market; + uint256 assets; + uint256 shares; + uint256 suppliedAssets; + uint256 suppliedShares; + address onbehalf; + bytes data; + MorphoHarness.Id id = getMarketId(market); + env e; + + require e.msg.sender != currentContract; + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = supplyShares(id, onbehalf); + mathint balanceBefore = myBalances[market.borrowableToken]; + + suppliedAssets, suppliedShares = supply(e, market, assets, shares, onbehalf, data); + assert assets != 0 => suppliedAssets == assets && shares == 0; + assert assets == 0 => suppliedShares == shares && shares != 0; + + mathint sharesAfter = supplyShares(id, onbehalf); + mathint balanceAfter = myBalances[market.borrowableToken]; + assert sharesAfter == sharesBefore + suppliedShares; + assert balanceAfter == balanceBefore + suppliedAssets; +} + +rule userCannotLoseSupplyShares(method f, calldataarg data) +filtered { + f -> !f.isView +} +{ + MorphoHarness.Market market; + uint256 assets; + uint256 shares; + uint256 suppliedAssets; + uint256 suppliedShares; + address user; + MorphoHarness.Id id = getMarketId(market); + env e; + + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = supplyShares(id, user); + + f(e, data); + + mathint sharesAfter = supplyShares(id, user); + assert sharesAfter >= sharesBefore; +} + +rule userCannotGainBorrowShares(method f, calldataarg data) +filtered { + f -> !f.isView +} +{ + MorphoHarness.Market market; + uint256 assets; + uint256 shares; + uint256 suppliedAssets; + uint256 suppliedShares; + address user; + MorphoHarness.Id id = getMarketId(market); + env e; + + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = borrowShares(id, user); + + f(e, data); + + mathint sharesAfter = borrowShares(id, user); + assert sharesAfter <= sharesBefore; +} + + +rule userWithoutBorrowCannotLoseCollateral(method f, calldataarg data) +filtered { + f -> !f.isView +} +{ + MorphoHarness.Market market; + uint256 assets; + uint256 shares; + uint256 suppliedAssets; + uint256 suppliedShares; + address user; + MorphoHarness.Id id = getMarketId(market); + env e; + + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + require borrowShares(id, user) == 0; + mathint collateralBefore = collateral(id, user); + + f(e, data); + + mathint collateralAfter = collateral(id, user); + assert borrowShares(id, user) == 0; + assert collateralAfter >= collateralBefore; +} diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index bf73fcb59..116e908ee 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -1,6 +1,8 @@ methods { function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address) external returns uint256 envfree; function isHealthy(MorphoHarness.Market, address user) external returns bool envfree; + function isAuthorized(address, address user) external returns bool envfree; function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; function _.price() external => mockPrice() expect uint256; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); @@ -32,9 +34,11 @@ function summaryMin(uint256 a, uint256 b) returns uint256 { return a < b ? a : b; } -rule stayHealthy(method f, env e, calldataarg data) filtered { +rule stayHealthy(method f, env e, calldataarg data) +filtered { f -> !f.isView -} { +} +{ MorphoHarness.Market market; MorphoHarness.Id id = getMarketId(market); address user; @@ -50,3 +54,31 @@ rule stayHealthy(method f, env e, calldataarg data) filtered { bool stillHealthy = isHealthy(market, user); assert !priceChanged => stillHealthy; } + +rule healthyUserCannotLoseCollateral(method f, calldataarg data) +filtered { + f -> !f.isView +} +{ + MorphoHarness.Market market; + uint256 assets; + uint256 shares; + uint256 suppliedAssets; + uint256 suppliedShares; + address user; + MorphoHarness.Id id = getMarketId(market); + env e; + + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + require lastUpdate(id) == e.block.timestamp; + require isHealthy(market, user); + mathint collateralBefore = collateral(id, user); + priceChanged = false; + + f(e, data); + + require !priceChanged; + mathint collateralAfter = collateral(id, user); + assert collateralAfter >= collateralBefore; +} From f3fc7079b9c0acf6d785bdc12f2e9a0e26b44a11 Mon Sep 17 00:00:00 2001 From: Jochen Hoenicke Date: Thu, 17 Aug 2023 21:57:02 +0200 Subject: [PATCH 2/2] Rule for withdrawing everything --- certora/specs/Blue.spec | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec index cc598dd25..4c2a537d6 100644 --- a/certora/specs/Blue.spec +++ b/certora/specs/Blue.spec @@ -1,6 +1,7 @@ methods { function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree; function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree; function totalSupply(MorphoHarness.Id) external returns uint256 envfree; function totalBorrow(MorphoHarness.Id) external returns uint256 envfree; function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree; @@ -291,3 +292,38 @@ filtered { assert borrowShares(id, user) == 0; assert collateralAfter >= collateralBefore; } + +rule noTimeTravel(method f, env e, calldataarg data) filtered { + f -> !f.isView +} { + MorphoHarness.Id id; + require lastUpdate(id) <= e.block.timestamp; + f(e, data); + assert lastUpdate(id) <= e.block.timestamp; +} + +rule canWithdrawAll() { + MorphoHarness.Market market; + uint256 withdrawnAssets; + uint256 withdrawnShares; + address receiver; + env e; + + MorphoHarness.Id id = getMarketId(market); + uint256 shares = supplyShares(id, e.msg.sender); + + require isInitialized(id); + require e.msg.sender != 0; + require receiver != 0; + require e.msg.value == 0; + require shares > 0; + require totalBorrow(id) == 0; + require lastUpdate(id) <= e.block.timestamp; + require shares < totalSupplyShares(id); + require totalSupplyShares(id) < 10^40 && totalSupply(id) < 10^30; + + withdrawnAssets, withdrawnShares = withdraw@withrevert(e, market, 0, shares, e.msg.sender, receiver); + + assert withdrawnShares == shares; + assert !lastReverted, "Can withdraw all assets if nobody borrows"; +}