From 2faa227def3768d2f453e8713f27e609804b1bc5 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 20 Dec 2023 21:11:01 +0100 Subject: [PATCH 01/14] feat: add equivalent input liquidate rule --- certora/specs/Health.spec | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index dc565b909..92601a738 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -106,3 +106,24 @@ filtered { f -> !f.isView } // This invariant ensures that bad debt realization cannot be bypassed. invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; + +// Checks that the debt input or the colleteral input of the liquidate function lead to the same repaid assets amount. +rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + storage init = lastStorage; + + uint256 seizedAssets1; + uint256 repaidAssets1; + seizedAssets1, repaidAssets1 = liquidate(e, marketParams, borrower, 0, repaidShares, data); + + uint256 seizedAssets2; + uint256 repaidAssets2; + seizedAssets2, repaidAssets2 = liquidate(e, marketParams, borrower, seizedAssets1, 0, data) at init; + + // Assume same context, including the oracle answer. + require !priceChanged; + + assert seizedAssets1 == seizedAssets2; + assert repaidAssets1 == repaidAssets2; +} From b9849584f68b071b313a470e7157856472f566c9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 20 Dec 2023 21:16:15 +0100 Subject: [PATCH 02/14] fix: remove unnecessary seized argument --- certora/specs/Health.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 92601a738..a1244f31a 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -108,7 +108,7 @@ invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; // Checks that the debt input or the colleteral input of the liquidate function lead to the same repaid assets amount. -rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) { +rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) { MorphoHarness.Id id = libId(marketParams); storage init = lastStorage; From 7c8a2bda77fa02c7d812fb330bad0fb924e59191 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 21 Dec 2023 12:08:39 +0100 Subject: [PATCH 03/14] fix: use price at the init both times --- certora/specs/Health.spec | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index a1244f31a..bb675e6ea 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -21,12 +21,12 @@ ghost uint256 lastPrice; ghost bool priceChanged; function mockPrice() returns uint256 { - uint256 somePrice; - if (somePrice != lastPrice) { + uint256 newPrice; + if (newPrice != lastPrice) { priceChanged = true; - lastPrice = somePrice; + lastPrice = newPrice; } - return somePrice; + return newPrice; } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { @@ -116,12 +116,11 @@ rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketP uint256 seizedAssets1; uint256 repaidAssets1; seizedAssets1, repaidAssets1 = liquidate(e, marketParams, borrower, 0, repaidShares, data); + require !priceChanged; uint256 seizedAssets2; uint256 repaidAssets2; seizedAssets2, repaidAssets2 = liquidate(e, marketParams, borrower, seizedAssets1, 0, data) at init; - - // Assume same context, including the oracle answer. require !priceChanged; assert seizedAssets1 == seizedAssets2; From f175a23e6f9d6c3de79490fcffd60668d61f1c84 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 21 Dec 2023 16:57:36 +0100 Subject: [PATCH 04/14] fix: use collateral input first --- certora/specs/Health.spec | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index bb675e6ea..99ff061e4 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -107,22 +107,24 @@ filtered { f -> !f.isView } invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; -// Checks that the debt input or the colleteral input of the liquidate function lead to the same repaid assets amount. -rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) { +// Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. +rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); storage init = lastStorage; - uint256 seizedAssets1; + uint256 sharesBefore = borrowShares(id, borrower); + uint256 repaidAssets1; - seizedAssets1, repaidAssets1 = liquidate(e, marketParams, borrower, 0, repaidShares, data); + _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data); require !priceChanged; - uint256 seizedAssets2; + uint256 sharesAfter = borrowShares(id, borrower); + uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter); + uint256 repaidAssets2; - seizedAssets2, repaidAssets2 = liquidate(e, marketParams, borrower, seizedAssets1, 0, data) at init; + _, repaidAssets2 = liquidate(e, marketParams, borrower, 0, repaidShares1, data) at init; require !priceChanged; - assert seizedAssets1 == seizedAssets2; assert repaidAssets1 == repaidAssets2; } From 613ff0aafbce9da4aeac0e82b69a15f651a097d1 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 2 Jan 2024 15:52:58 +0100 Subject: [PATCH 05/14] refactor: testing LIA config --- certora/confs/AccrueInterest.conf | 4 +- certora/confs/AssetsAccounting.conf | 2 +- certora/confs/ConsistentState.conf | 2 +- certora/confs/ExactMath.conf | 5 ++- certora/confs/Health.conf | 2 + certora/confs/LibSummary.conf | 2 +- certora/confs/Liveness.conf | 2 +- certora/confs/RatioMath.conf | 4 +- certora/confs/Reentrancy.conf | 4 +- certora/confs/Reverts.conf | 2 +- certora/confs/Transfer.conf | 2 +- certora/specs/Health.spec | 66 ----------------------------- 12 files changed, 17 insertions(+), 80 deletions(-) diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index 8f8c26d72..3ae9ec84b 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -1,12 +1,12 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", "prover_args": [ "-depth 3", "-smt_hashingScheme plaininjectivity", - "-mediumTimeout 30" + "-mediumTimeout 30", ], "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf index 6dcd57dc6..e8a011349 100644 --- a/certora/confs/AssetsAccounting.conf +++ b/certora/confs/AssetsAccounting.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", "rule_sanity": "basic", diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index fdfa6e17a..45c0c672f 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/ConsistentState.spec", "rule_sanity": "basic", diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 947e98bb4..35d755e27 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,12 +1,13 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/ExactMath.spec", "rule_sanity": "basic", "prover_args": [ + "-depth 3", "-smt_hashingScheme plaininjectivity", - "-mediumTimeout 30" + "-mediumTimeout 30", ], "server": "production", "msg": "Morpho Blue Exact Math" diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index f361bf43d..20a76bc14 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -7,6 +7,8 @@ "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity" + "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic false", ], "server": "production", "msg": "Morpho Blue Health" diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index f931810eb..6f944ed00 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/LibSummary.spec", "rule_sanity": "basic", diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index 211a0897a..b3788c685 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/harness/MorphoInternalAccess.sol" + "certora/harness/MorphoInternalAccess.sol", ], "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", "rule_sanity": "basic", diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf index 9062f1b14..a0ac6df8b 100644 --- a/certora/confs/RatioMath.conf +++ b/certora/confs/RatioMath.conf @@ -1,13 +1,13 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/RatioMath.spec", "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity", "-mediumTimeout 30", - "-timeout 3600" + "-timeout 3600", ], "server": "production", "msg": "Morpho Blue Ratio Math" diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf index 84019dceb..db93b6a23 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -1,11 +1,11 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/Reentrancy.spec", "rule_sanity": "basic", "prover_args": [ - "-enableStorageSplitting false" + "-enableStorageSplitting false", ], "server": "production", "msg": "Morpho Blue Reentrancy" diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index 6992b6b4b..a31c697d4 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -1,6 +1,6 @@ { "files": [ - "certora/harness/MorphoHarness.sol" + "certora/harness/MorphoHarness.sol", ], "verify": "MorphoHarness:certora/specs/Reverts.spec", "rule_sanity": "basic", diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf index 6425f56a5..bedba566c 100644 --- a/certora/confs/Transfer.conf +++ b/certora/confs/Transfer.conf @@ -3,7 +3,7 @@ "certora/harness/TransferHarness.sol", "certora/dispatch/ERC20Standard.sol", "certora/dispatch/ERC20USDT.sol", - "certora/dispatch/ERC20NoRevert.sol" + "certora/dispatch/ERC20NoRevert.sol", ], "verify": "TransferHarness:certora/specs/Transfer.spec", "rule_sanity": "basic", diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 99ff061e4..e561c2e5c 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -41,72 +41,6 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { return require_uint256((x * y) / d); } -function summaryMin(uint256 a, uint256 b) returns uint256 { - return a < b ? a : b; -} - -// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. -// This rule times out for liquidate, repay and borrow. -rule stayHealthy(env e, method f, calldataarg data) -filtered { - f -> !f.isView && - f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector && - f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && - f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector -} -{ - MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); - address user; - - // Assume that the position is healthy before the interaction. - require isHealthy(marketParams, user); - // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. - require marketParams.lltv < 10^18; - // Assumption to ensure that no interest is accumulated. - require lastUpdate(id) == e.block.timestamp; - - priceChanged = false; - f(e, data); - - // Safe require because of the invariant sumBorrowSharesCorrect. - require borrowShares(id, user) <= totalBorrowShares(id); - - bool stillHealthy = isHealthy(marketParams, user); - assert !priceChanged => stillHealthy; -} - -// Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. -rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) -filtered { f -> !f.isView } -{ - MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); - address user; - - // Assume that the e.msg.sender is not authorized. - require !isAuthorized(user, e.msg.sender); - require user != e.msg.sender; - // Assumption to ensure that no interest is accumulated. - require lastUpdate(id) == e.block.timestamp; - // Assume that the user is healthy. - require isHealthy(marketParams, user); - - mathint collateralBefore = collateral(id, user); - - priceChanged = false; - f(e, data); - - mathint collateralAfter = collateral(id, user); - - assert !priceChanged => collateralAfter >= collateralBefore; -} - -// Check that users without collateral also have no debt. -// This invariant ensures that bad debt realization cannot be bypassed. -invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) - borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; - // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); From ae1f7cafd94521df8e1c9e2433daf5edb2de1f39 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 3 Jan 2024 14:55:20 +0100 Subject: [PATCH 06/14] fix: file Health.conf syntax bug --- certora/confs/Health.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 20a76bc14..ef2db9f3d 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -6,7 +6,7 @@ "verify": "MorphoHarness:certora/specs/Health.spec", "rule_sanity": "basic", "prover_args": [ - "-smt_hashingScheme plaininjectivity" + "-smt_hashingScheme plaininjectivity", "-adaptiveSolverConfig false", "-smt_nonLinearArithmetic false", ], From 14ecae8bd8d106c452f9747635e34fb779460c3a Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 3 Jan 2024 14:57:58 +0100 Subject: [PATCH 07/14] fix: add back summaryMin --- certora/specs/Health.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index e561c2e5c..2ecf144ba 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -41,6 +41,10 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { return require_uint256((x * y) / d); } +function summaryMin(uint256 a, uint256 b) returns uint256 { + return a < b ? a : b; +} + // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); From a8b2c470bd9ce5fc1ff411467cf756ed8bb3b949 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 4 Jan 2024 17:14:18 +0100 Subject: [PATCH 08/14] test: with bigger timeout --- certora/confs/Health.conf | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index ef2db9f3d..ee68e0cdc 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -9,6 +9,7 @@ "-smt_hashingScheme plaininjectivity", "-adaptiveSolverConfig false", "-smt_nonLinearArithmetic false", + "-timeout 3600", ], "server": "production", "msg": "Morpho Blue Health" From 04bbb4744050a62283723e4923ac533bd7d49b40 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 4 Jan 2024 17:16:16 +0100 Subject: [PATCH 09/14] feat: assume no interest accrual --- certora/specs/Health.spec | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 2ecf144ba..bc59f0cd2 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -7,6 +7,7 @@ methods { function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function collateral(MorphoHarness.Id, address) external returns uint256 envfree; function isAuthorized(address, address user) external returns bool envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; @@ -49,6 +50,9 @@ function summaryMin(uint256 a, uint256 b) returns uint256 { rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams); + // Assume no interest accrual to ease the verification. + require lastUpdate(id) == e.block.timestamp; + storage init = lastStorage; uint256 sharesBefore = borrowShares(id, borrower); From 070ec8adf271c2daa800062422b2ecb14616c1c9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Wed, 14 Feb 2024 12:09:01 +0100 Subject: [PATCH 10/14] style: renaming --- certora/specs/Health.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index bc59f0cd2..cd40ee968 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -22,12 +22,12 @@ ghost uint256 lastPrice; ghost bool priceChanged; function mockPrice() returns uint256 { - uint256 newPrice; - if (newPrice != lastPrice) { + uint256 updatedPrice; + if (updatedPrice != lastPrice) { priceChanged = true; - lastPrice = newPrice; + lastPrice = updatedPrice; } - return newPrice; + return updatedPrice; } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { From 173c9927490643c1a443ebcd8b6e19382850a2b4 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 20 Feb 2024 09:44:35 +0100 Subject: [PATCH 11/14] chore: test with easy LIA --- certora/confs/Health.conf | 1 + certora/specs/Health.spec | 2 -- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index ee68e0cdc..5ce7e90fc 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -9,6 +9,7 @@ "-smt_hashingScheme plaininjectivity", "-adaptiveSolverConfig false", "-smt_nonLinearArithmetic false", + "-smt_easy_LIA true", "-timeout 3600", ], "server": "production", diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 5ff9dfc8b..01cff57cf 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -54,13 +54,11 @@ rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketP require lastUpdate(id) == e.block.timestamp; storage init = lastStorage; - uint256 sharesBefore = borrowShares(id, borrower); uint256 repaidAssets1; _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data); require !priceChanged; - uint256 sharesAfter = borrowShares(id, borrower); uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter); From 722b1ee8333fcb1fd7a7ba2c0178f8c091d1edc8 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 20 Feb 2024 10:00:50 +0100 Subject: [PATCH 12/14] feat: omit bad debt realization for verification --- certora/specs/Health.spec | 2 ++ 1 file changed, 2 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 01cff57cf..ad833cbf1 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -59,6 +59,8 @@ rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketP uint256 repaidAssets1; _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data); require !priceChanged; + // Omit the bad debt realization case. + require collateral(id, borrower) != 0; uint256 sharesAfter = borrowShares(id, borrower); uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter); From 20d6f9c9a79fbfc5978553c493c95b226877bda0 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 20 Feb 2024 10:34:53 +0100 Subject: [PATCH 13/14] chore: remove special setting for Health --- certora/confs/Health.conf | 4 ---- 1 file changed, 4 deletions(-) diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 5ce7e90fc..9238fde6b 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -7,10 +7,6 @@ "rule_sanity": "basic", "prover_args": [ "-smt_hashingScheme plaininjectivity", - "-adaptiveSolverConfig false", - "-smt_nonLinearArithmetic false", - "-smt_easy_LIA true", - "-timeout 3600", ], "server": "production", "msg": "Morpho Blue Health" From a52b262df8e6d383e1730267be02bdb9b793d99b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Tue, 20 Feb 2024 10:51:36 +0100 Subject: [PATCH 14/14] feat: add back Health verification --- certora/specs/Health.spec | 62 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index ad833cbf1..45c535187 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -46,6 +46,68 @@ function summaryMin(uint256 a, uint256 b) returns uint256 { return a < b ? a : b; } +// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. +// This rule times out for liquidate, repay and borrow. +rule stayHealthy(env e, method f, calldataarg data) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector && + f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && + f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector +} +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the position is healthy before the interaction. + require isHealthy(marketParams, user); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + priceChanged = false; + f(e, data); + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + assert !priceChanged => stillHealthy; +} + +// Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. +rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + // Assume that the user is healthy. + require isHealthy(marketParams, user); + + mathint collateralBefore = collateral(id, user); + + priceChanged = false; + f(e, data); + + mathint collateralAfter = collateral(id, user); + + assert !priceChanged => collateralAfter >= collateralBefore; +} + +// Check that users without collateral also have no debt. +// This invariant ensures that bad debt realization cannot be bypassed. +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; + // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { MorphoHarness.Id id = libId(marketParams);