diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 575ed04e..1aa6ec65 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -22,6 +22,7 @@ jobs: - Immutability - LastUpdated - Liveness + - MarketInteractions - PendingValues - Range - Reentrancy diff --git a/certora/README.md b/certora/README.md index 660f827e..c2156b68 100644 --- a/certora/README.md +++ b/certora/README.md @@ -103,6 +103,7 @@ function isEnabledHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams ``` This checks that each market in the withdraw queue has a consistent asset. +Additionally, every supply and withdraw on Morpho Blue is checked to target an enabled market in [`MarketInteractions.spec`](specs/MarketInteractions.spec). ### Enabled flag @@ -192,12 +193,13 @@ The [`certora/specs`](specs) folder contains the following files: - [`Immutability.spec`](specs/Immutability.spec) checks that MetaMorpho is immutable. - [`LastUpdated.spec`](specs/LastUpdated.spec) checks that all Morpho Blue markets that MetaMorpho interacts with are created markets. - [`Liveness.spec`](specs/Liveness.spec) checks some liveness properties of MetaMorpho, notably that some emergency procedures are always available. +- [`MarketInteractions.spec`](specs/MarketInteractions.spec) checks that every supply and withdraw from MetaMorpho is targeting an enabled market. - [`PendingValues.spec`](specs/PendingValues.spec) checks properties on the values that are still under timelock. Those properties are notably useful to prove that actual storage variables, when set to the pending value, use a consistent value. - [`Range.spec`](specs/Range.spec) checks the bounds (if any) of storage variables. - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that MetaMorpho is reentrancy safe by making sure that there are no untrusted external calls. - [`Reverts.spec`](specs/Reverts.spec) checks the revert conditions on entrypoints. - [`Roles.spec`](specs/Roles.spec) checks the access control and authorization granted by the respective MetaMorpho roles. In particular it checks the hierarchy of roles. -- [`Timelock.spec`](specs/Timelock.spec) gives computations (and verifies them) for periods during which we know the values are under timelock. +- [`Timelock.spec`](specs/Timelock.spec) verifies computations for periods during which we know the values are under timelock. - [`Tokens.spec`](specs/Tokens.spec) checks that tokens are not kept on the MetaMorpho contract. Any deposit ends up in Morpho Blue and any withdrawal is forwarded to the user. The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. @@ -211,12 +213,13 @@ The [`certora/dispatch`](dispatch) folder contains different contracts similar ```mermaid graph -Tokens --> ConsistentState -Liveness --> ConsistentState -Reverts --> ConsistentState +Tokens --> LastUpdated +Liveness --> LastUpdated +Reverts --> LastUpdated +LastUpdated --> ConsistentState +MarketInteractions --> ConsistentState ConsistentState --> Timelock -Timelock --> LastUpdated -LastUpdated --> Enabled +Timelock --> Enabled Enabled --> DistinctIdentifiers DistinctIdentifiers --> PendingValues PendingValues --> Range diff --git a/certora/applyMunging.patch b/certora/applyMunging.patch index b77f8391..31937cc4 100644 --- a/certora/applyMunging.patch +++ b/certora/applyMunging.patch @@ -1,6 +1,6 @@ diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol ---- interfaces/IMetaMorpho.sol 2024-01-03 14:41:15.012185229 +0100 -+++ interfaces/IMetaMorpho.sol 2024-03-04 17:27:18.336468241 +0100 +--- interfaces/IMetaMorpho.sol 2024-03-20 15:13:25.818251404 +0100 ++++ interfaces/IMetaMorpho.sol 2024-03-22 11:22:35.598510490 +0100 @@ -1,9 +1,9 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity >=0.5.0; @@ -24,8 +24,8 @@ diff -ruN interfaces/IMetaMorpho.sol interfaces/IMetaMorpho.sol /// @notice The address of the curator. diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol ---- libraries/ErrorsLib.sol 2024-01-03 14:27:38.058744959 +0100 -+++ libraries/ErrorsLib.sol 2024-02-13 10:07:21.879957695 +0100 +--- libraries/ErrorsLib.sol 2024-03-20 15:13:25.802251714 +0100 ++++ libraries/ErrorsLib.sol 2024-03-22 11:22:35.598510490 +0100 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity ^0.8.0; @@ -36,8 +36,8 @@ diff -ruN libraries/ErrorsLib.sol libraries/ErrorsLib.sol /// @title ErrorsLib /// @author Morpho Labs diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol ---- libraries/EventsLib.sol 2023-11-27 12:37:13.369852625 +0100 -+++ libraries/EventsLib.sol 2024-02-13 10:07:21.879957695 +0100 +--- libraries/EventsLib.sol 2024-03-20 15:13:25.802251714 +0100 ++++ libraries/EventsLib.sol 2024-03-22 11:22:35.598510490 +0100 @@ -1,7 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity ^0.8.0; @@ -48,8 +48,8 @@ diff -ruN libraries/EventsLib.sol libraries/EventsLib.sol import {PendingAddress} from "./PendingLib.sol"; diff -ruN MetaMorpho.sol MetaMorpho.sol ---- MetaMorpho.sol 2024-02-02 13:00:21.238074050 +0100 -+++ MetaMorpho.sol 2024-03-04 23:26:21.562604750 +0100 +--- MetaMorpho.sol 2024-03-20 15:13:25.862250553 +0100 ++++ MetaMorpho.sol 2024-03-22 14:27:33.670423544 +0100 @@ -9,24 +9,22 @@ IMetaMorphoBase, IMetaMorphoStaticTyping @@ -114,10 +114,14 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol /// @notice OpenZeppelin decimals offset used by the ERC4626 implementation. /// @dev Calculated to be max(0, 18 - underlyingDecimals) at construction, so the initial conversion rate maximizes -@@ -107,6 +103,15 @@ +@@ -107,6 +103,19 @@ /// @inheritdoc IMetaMorphoBase uint256 public lastTotalAssets; ++ // HARNESS ++ // The index of the identifier of the last market withdrawn. ++ uint256 public lastIndexWithdraw; ++ + // HARNESS + // The rank of a market identifier in the withdraw queue. + // Returns 0 if the corresponding market is not in the withdraw queue. @@ -130,7 +134,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol /* CONSTRUCTOR */ /// @dev Initializes the contract. -@@ -126,7 +131,7 @@ +@@ -126,7 +135,7 @@ ) ERC4626(IERC20(_asset)) ERC20Permit(_name) ERC20(_name, _symbol) Ownable(owner) { if (morpho == address(0)) revert ErrorsLib.ZeroAddress(); @@ -139,7 +143,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol DECIMALS_OFFSET = uint8(uint256(18).zeroFloorSub(IERC20Metadata(_asset).decimals())); _checkTimelockBounds(initialTimelock); -@@ -338,6 +343,9 @@ +@@ -338,6 +347,9 @@ seen[prevIndex] = true; newWithdrawQueue[i] = id; @@ -149,7 +153,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol } for (uint256 i; i < currLength; ++i) { -@@ -355,6 +363,10 @@ +@@ -355,6 +367,10 @@ } } @@ -160,7 +164,7 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol delete config[id]; } } -@@ -743,6 +755,9 @@ +@@ -743,6 +759,9 @@ if (supplyCap > 0) { if (!marketConfig.enabled) { @@ -170,3 +174,13 @@ diff -ruN MetaMorpho.sol MetaMorpho.sol withdrawQueue.push(id); if (withdrawQueue.length > ConstantsLib.MAX_QUEUE_LENGTH) revert ErrorsLib.MaxQueueLengthExceeded(); +@@ -802,6 +821,9 @@ + /// @dev Withdraws `assets` from Morpho. + function _withdrawMorpho(uint256 assets) internal { + for (uint256 i; i < withdrawQueue.length; ++i) { ++ // HARNESS ++ lastIndexWithdraw = i; ++ + Id id = withdrawQueue[i]; + MarketParams memory marketParams = _marketParams(id); + (uint256 supplyAssets,, Market memory market) = _accruedSupplyBalance(marketParams, id); diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index 366d4e4c..5da45284 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,12 +1,9 @@ { "files": [ - "lib/morpho-blue/certora/harness/MorphoHarness.sol", "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol", ], - "solc_map": { - "MorphoHarness": "solc-0.8.19", - "MetaMorphoHarness": "solc-0.8.21", - }, + "solc": "solc-0.8.21", "parametric_contracts": [ "MetaMorphoHarness", ], diff --git a/certora/confs/LastUpdated.conf b/certora/confs/LastUpdated.conf index 855c7359..81bc168c 100644 --- a/certora/confs/LastUpdated.conf +++ b/certora/confs/LastUpdated.conf @@ -2,10 +2,12 @@ "files": [ "lib/morpho-blue/certora/harness/MorphoHarness.sol", "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol", ], "solc_map": { "MorphoHarness": "solc-0.8.19", "MetaMorphoHarness": "solc-0.8.21", + "Util": "solc-0.8.21", }, "verify": "MetaMorphoHarness:certora/specs/LastUpdated.spec", "loop_iter": "2", diff --git a/certora/confs/MarketInteractions.conf b/certora/confs/MarketInteractions.conf new file mode 100644 index 00000000..02b6ea2e --- /dev/null +++ b/certora/confs/MarketInteractions.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "certora/helpers/MetaMorphoHarness.sol", + "certora/helpers/Util.sol", + ], + "solc": "solc-0.8.21", + "parametric_contracts": [ + "MetaMorphoHarness", + ], + "verify": "MetaMorphoHarness:certora/specs/MarketInteractions.spec", + "loop_iter": "2", + "optimistic_loop": true, + "prover_args": [ + "-depth 3", + "-mediumTimeout 20", + "-timeout 120", + ], + "server": "production", + "msg": "MetaMorpho Market Interactions" +} diff --git a/certora/helpers/Util.sol b/certora/helpers/Util.sol index e713bd38..b38f9e03 100644 --- a/certora/helpers/Util.sol +++ b/certora/helpers/Util.sol @@ -1,11 +1,21 @@ // SPDX-License-Identifier: GPL-2.0-or-later pragma solidity 0.8.21; -import {IERC20, SafeERC20, IMorphoHarness, SharesMathLib, Id, Market} from "../munged/MetaMorpho.sol"; +import { + MarketParams, + MarketParamsLib, + IERC20, + SafeERC20, + IMorphoHarness, + SharesMathLib, + Id, + Market +} from "../munged/MetaMorpho.sol"; contract Util { using SafeERC20 for IERC20; using SharesMathLib for uint256; + using MarketParamsLib for MarketParams; function balanceOf(address token, address user) external view returns (uint256) { return IERC20(token).balanceOf(user); @@ -31,4 +41,8 @@ contract Util { return shares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares); } } + + function libId(MarketParams memory marketParams) external pure returns (Id) { + return marketParams.id(); + } } diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 8185f85b..c9a20a75 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -1,16 +1,14 @@ // SPDX-License-Identifier: GPL-2.0-or-later import "Timelock.spec"; -function hasCuratorRole(address user) returns bool { - return user == owner() || user == curator(); -} - -function hasAllocatorRole(address user) returns bool { - return user == owner() || user == curator() || isAllocator(user); -} - -function hasGuardianRole(address user) returns bool { - return user == owner() || user == guardian(); +using Util as Util; + +methods { + function Util.libId(MetaMorphoHarness.MarketParams) external returns(MetaMorphoHarness.Id) envfree; + function Util.balanceOf(address, address) external returns(uint256) envfree; + function Util.totalSupply(address) external returns(uint256) envfree; + function Util.safeTransferFrom(address, address, address, uint256) external envfree; + function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree; } // Check that fee cannot accrue to an unset fee recipient. @@ -29,7 +27,7 @@ invariant supplyCapIsEnabled(MetaMorphoHarness.Id id) hasSupplyCapIsEnabled(id); function hasPendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams) returns bool { - MetaMorphoHarness.Id id = Morpho.libId(marketParams); + MetaMorphoHarness.Id id = Util.libId(marketParams); return pendingCap_(id).validAt > 0 => marketParams.loanToken == asset(); } @@ -39,7 +37,7 @@ invariant pendingSupplyCapHasConsistentAsset(MetaMorphoHarness.MarketParams mark hasPendingSupplyCapHasConsistentAsset(marketParams); function isEnabledHasConsistentAsset(MetaMorphoHarness.MarketParams marketParams) returns bool { - MetaMorphoHarness.Id id = Morpho.libId(marketParams); + MetaMorphoHarness.Id id = Util.libId(marketParams); return config_(id).enabled => marketParams.loanToken == asset(); } diff --git a/certora/specs/LastUpdated.spec b/certora/specs/LastUpdated.spec index d123cfc7..a7a75001 100644 --- a/certora/specs/LastUpdated.spec +++ b/certora/specs/LastUpdated.spec @@ -1,11 +1,22 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "Enabled.spec"; +import "ConsistentState.spec"; using MorphoHarness as Morpho; methods { function Morpho.lastUpdate(MorphoHarness.Id) external returns(uint256) envfree; - function Morpho.libId(MorphoHarness.MarketParams) external returns(MorphoHarness.Id) envfree; +} + +function hasCuratorRole(address user) returns bool { + return user == owner() || user == curator(); +} + +function hasAllocatorRole(address user) returns bool { + return user == owner() || user == curator() || isAllocator(user); +} + +function hasGuardianRole(address user) returns bool { + return user == owner() || user == guardian(); } // Check that any market with positive cap is created on Morpho Blue. diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index d8abb025..fe3160e5 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -1,5 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "ConsistentState.spec"; +import "LastUpdated.spec"; // Check that having the allocator role allows to pause supply on the vault. rule canPauseSupply() { @@ -25,7 +25,7 @@ rule canPauseSupply() { } rule canForceRemoveMarket(MetaMorphoHarness.MarketParams marketParams) { - MetaMorphoHarness.Id id = Morpho.libId(marketParams); + MetaMorphoHarness.Id id = Util.libId(marketParams); // Safe require because it is a verified invariant. require hasSupplyCapIsEnabled(id); diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec new file mode 100644 index 00000000..cbfc6d09 --- /dev/null +++ b/certora/specs/MarketInteractions.spec @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +import "ConsistentState.spec"; + +methods { + function _.supply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) external => summarySupply(marketParams, assets, shares, onBehalf, data) expect (uint256, uint256) ALL; + function _.withdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external => summaryWithdraw(marketParams, assets, shares, onBehalf, receiver) expect (uint256, uint256) ALL; + function _.idToMarketParams(MetaMorphoHarness.Id id) external => summaryIdToMarketParams(id) expect MetaMorphoHarness.MarketParams ALL; + + function lastIndexWithdraw() external returns(uint256) envfree; +} + +function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarness.MarketParams { + MetaMorphoHarness.MarketParams marketParams; + + // Safe require because: + // - markets in the supply/withdraw queue have positive lastUpdate (see LastUpdated.spec) + // - lastUpdate(id) > 0 => marketParams.id() == id is a verified invariant in Morpho Blue. + require Util.libId(marketParams) == id; + + return marketParams; +} + +function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) returns(uint256, uint256) { + assert shares == 0; + assert assets != 0; + assert onBehalf == currentContract; + assert data.length == 0; + + MetaMorphoHarness.Id id = Util.libId(marketParams); + // Safe require because it is a verified invariant + require hasSupplyCapIsEnabled(id); + + // Check that all markets on which MetaMorpho supplies are enabled markets. + assert config_(id).enabled; + + // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away. + return (_, _); +} + +function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) returns (uint256, uint256) { + assert shares == 0 <=> assets != 0; + assert onBehalf == currentContract; + assert receiver == currentContract; + + MetaMorphoHarness.Id id = Util.libId(marketParams); + uint256 index = lastIndexWithdraw(); + // Safe require because it is a verified invariant. + require isInWithdrawQueueIsEnabled(index); + + // Check that all markets from which MetaMorpho withdraws are enabled markets. + assert config_(id).enabled; + + // NONDET summary, which is sound because all non view functions in Morpho Blue are abstracted away. + return (_, _); +} + +// Check assertions in the summaries. +// This requires to turn off sanity checks for this invariant that appears vacuous. +invariant checkSummaries() + true; diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 9e91e6f4..5394efe9 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -1,12 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "ConsistentState.spec"; - -using Util as Util; +import "LastUpdated.spec"; methods { - function Util.totalSupply(address) external returns(uint256) envfree; - function Util.balanceOf(address, address) external returns(uint256) envfree; - function _.transfer(address, uint256) external => DISPATCHER(true); function _.balanceOf(address) external => DISPATCHER(true); } @@ -104,7 +99,7 @@ rule submitGuardianRevertCondition(env e, address newGuardian) { // Check all the revert conditions of the submitCap function. rule submitCapRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams, uint256 newSupplyCap) { - MorphoHarness.Id id = Morpho.libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); bool hasCuratorRole = hasCuratorRole(e.msg.sender); address asset = asset(); @@ -134,7 +129,7 @@ rule submitCapRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams // Check all the revert conditions of the submitMarketRemoval function. rule submitMarketRemovalRevertCondition(env e, MetaMorphoHarness.MarketParams marketParams) { - MorphoHarness.Id id = Morpho.libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); bool hasCuratorRole = hasCuratorRole(e.msg.sender); uint256 pendingCapValidAt = pendingCap_(id).validAt; @@ -283,7 +278,7 @@ rule acceptGuardianRevertCondition(env e) { // Check the input validation conditions under which the acceptCap function reverts. // This function can also revert if interest accrual reverts or if it would lead to growing the withdraw queue past the max length. rule acceptCapInputValidation(env e, MetaMorphoHarness.MarketParams marketParams) { - MetaMorphoHarness.Id id = Morpho.libId(marketParams); + MetaMorphoHarness.Id id = Util.libId(marketParams); uint256 pendingCapValidAt = pendingCap_(id).validAt; diff --git a/certora/specs/Timelock.spec b/certora/specs/Timelock.spec index 51c2acb1..3b880965 100644 --- a/certora/specs/Timelock.spec +++ b/certora/specs/Timelock.spec @@ -1,5 +1,5 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "LastUpdated.spec"; +import "Enabled.spec"; methods { function _.supplyShares(MetaMorphoHarness.Id id, address user) external => summarySupplyshares(id, user) expect uint256; diff --git a/certora/specs/Tokens.spec b/certora/specs/Tokens.spec index fa9a19ab..703e874c 100644 --- a/certora/specs/Tokens.spec +++ b/certora/specs/Tokens.spec @@ -1,13 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later -import "ConsistentState.spec"; - -using Util as Util; +import "LastUpdated.spec"; methods { - function Util.balanceOf(address, address) external returns(uint256) envfree; - function Util.safeTransferFrom(address, address, address, uint256) external envfree; - function Util.withdrawnAssets(address, MetaMorphoHarness.Id, uint256, uint256) external returns (uint256) envfree; - function _.transfer(address, uint256) external => DISPATCHER(true); function _.transferFrom(address, address, uint256) external => DISPATCHER(true); function _.balanceOf(address) external => DISPATCHER(true); @@ -27,7 +21,7 @@ function summaryIdToMarketParams(MetaMorphoHarness.Id id) returns MetaMorphoHarn // Safe require because markets in the supply/withdraw queue have positive last update (see LastUpdated.spec). require lastUpdated > 0; // Safe require because it is a verified invariant in Morpho Blue. - require lastUpdated > 0 => Morpho.libId(marketParams) == id; + require lastUpdated > 0 => Util.libId(marketParams) == id; return marketParams; } @@ -38,7 +32,7 @@ function summarySupply(MetaMorphoHarness.MarketParams marketParams, uint256 asse assert data.length == 0; // Safe require because it is a verified invariant. - require hasSupplyCapIsEnabled(Morpho.libId(marketParams)); + require hasSupplyCapIsEnabled(Util.libId(marketParams)); // Safe require because it is a verified invariant. require isEnabledHasConsistentAsset(marketParams); @@ -52,11 +46,9 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as assert onBehalf == currentContract; assert receiver == currentContract; - MetaMorphoHarness.Id id = Morpho.libId(marketParams); + MetaMorphoHarness.Id id = Util.libId(marketParams); - // Safe require because: - // - for reallocate this is checked in the code - // - for withdraw, it is verified that markets in the withdraw queue are enabled. + // Safe require because it is verifed in MarketInteractions. require config_(id).enabled; // Safe require because it is a verified invariant. require isEnabledHasConsistentAsset(marketParams);