[Certora] Documentation

certora/README.md

@@ -1,28 +1,242 @@
 This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language.
 
-## High-Level Description
-
-The Morpho Blue protocol relies on several different concepts, which are described below.
+The core concepts of the the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf).
 These concepts have been verified using CVL.
-See the description of the specification files below (or those files directly) for more details.
-
-The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.\
-**Transfers.** Token transfers are verified to behave as expected for the most common implementations, in particular the transferred amount is the amount passed as input.\
-**Markets**. Markets on Morpho Blue depend on a pair of assets, the borrowable asset that is supplied and borrowed, and the collateral asset.
-Markets are independent, which means that loans cannot be impacted by loans from other markets.
-Positions of users are also independent, so loans cannot be impacted by loans from other users.
-The accounting of the markets has been verified (such as the total amounts), as well as the fact that only market with enabled parameters are created.\
-**Supply.** When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
-Shares increase in value as interest is accrued.\
-**Borrow.** To borrow on Morpho Blue, collateral must be deposited.
-Collateral tokens remain idle, as well as any borrowable token that has not been borrowed.\
-**Liquidation.** To ensure proper collateralization, a liquidation system is put in place.
-In the absence of accrued interest, for example when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.\
-**Authorization.** Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating).\
-**Safety.** Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions.\
-**Liveness.** Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle.
-
-## Folder and File Structure
+We first give a [high-level description](#high-level-description) of the verification and then describe the [folder and file structure](#folder-and-file-structure) of the specification files.
+
+# High-level description
+
+The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.
+
+## ERC20 tokens and transfers
+
+For a given market, Morpho Blue relies on the fact that the tokens involved respect the ERC20 standard.
+In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if its the recipient or the sender) of the amount transferred.
+
+The file [Transfer.spec](./specs/Transfer.spec) defines a summary of the transfer functions.
+This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected.
+
+```solidity
+function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
+    if (from == currentContract) {
+        balance[token] = require_uint256(balance[token] - amount);
+    }
+    if (to == currentContract) {
+        balance[token] = require_uint256(balance[token] + amount);
+    }
+}
+```
+
+where `balance` is the ERC20 balance of the Morpho Blue contract.
+
+The verification is done for the most common implementations of the ERC20 standard, for which we distinguish three different implementations:
+
+- [ERC20Standard](./dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance.
+- [ERC20NoRevert](./dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead).
+- [ERC20USDT](./dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions.
+
+Additionally, Morpho Blue always goes through a custom transfer library to handle ERC20 tokens, notably in all the above cases.
+This library reverts when the transfer is not successful, and this is checked for the case of insufficient funds or insufficient allowance.
+The use of the library can make it difficult for the provers, so the summary is sometimes used in other specification files to ease the verification of rules that rely on the transfer of tokens.
+
+## Markets
+
+The Morpho Blue contract is a singleton contract that defines different markets.
+Markets on Morpho Blue depend on a pair of assets, the loan token that is supplied and borrowed, and the collateral token.
+Taking out a loan requires to deposit some collateral, which stays idle in the contract.
+Additionally, every loan token that is not borrowed also stays idle in the contract.
+This is verified by the following property:
+
+```solidity
+invariant idleAmountLessThanBalance(address token)
+    idleAmount[token] <= balance[token]
+```
+
+where `idleAmount` is the sum over all the markets of: the collateral amounts plus the supplied amounts minus the borrowed amounts.
+In effect, this means that funds can only leave the contract through borrows and withdrawals.
+
+Additionally, it is checked that on a given market the borrowed amounts cannot exceed the supplied amounts.
+
+```solidity
+invariant borrowLessThanSupply(MorphoHarness.Id id)
+    totalBorrowAssets(id) <= totalSupplyAssets(id);
+```
+
+This property, along with the previous one ensures that other markets can only impact the balance positively.
+Said otherwise, markets are independent: tokens from a given market cannot be impacted by operations done in another market.
+
+## Shares
+
+When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
+Shares increase in value as interest is accrued.
+The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest.
+The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement.
+
+```soldidity
+    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+```
+
+where `assetsBefore` and `sharesBefore` represents respectively the supplied assets and the supplied shares before accruing the interest. Similarly, `assetsAfter` and `sharesAfter` represent the supplied assets and shares after an interest accrual.
+
+The accounting of the shares mechanism relies on another variable to store the total number of shares, in order to compute what is the relative part of each user.
+This variable needs to be kept up to date at each corresponding interaction, and it is checked that this accounting is done properly.
+For example, for the supply side, this is done by the following invariant.
+
+```solidity
+invariant sumSupplySharesCorrect(MorphoHarness.Id id)
+    to_mathint(totalSupplyShares(id)) == sumSupplyShares[id];
+```
+
+where `sumSupplyShares` only exists in the specification, and is defined to be automatically updated whenever any of the shares of the users are modified.
+
+## Positions health and liquidations
+
+To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated.
+A position is said to be healthy if the ratio of the borrowed value over collateral value is smaller than the liquidation loan-to-value (LLTV) of that market.
+This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1.
+To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected.
+Notably, it is verified that in the absence of accrued interest, which is the case when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy.
+
+Let's define bad debt of a position as the amount borrowed when it is backed by no collateral.
+Morpho Blue automatically realizes the bad debt when liquidating a position, by transferring it to the lenders.
+In effect, this means that there is no bad debt on Morpho Blue, which is verified by the following invariant.
+
+```solidity
+invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
+    borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;
+```
+
+More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty).
+
+## Authorization
+
+Morpho Blue also defines primitive authorization system, where users can authorize an account to fully manage their position.
+This allows to rebuild more granular control of the position on top by authorizing an immutable contract with limited capabilities.
+The authorization is verified to be sound in the sense that no user can modify the position of another user without proper authorization (except when liquidating).
+
+Let's detail the rule that makes sure that the supply side stays consistent.
+
+```solidity
+rule userCannotLoseSupplyShares(env e, method f, calldataarg data)
+filtered { f -> !f.isView }
+{
+    MorphoHarness.Id id;
+    address user;
+
+    // Assume that the e.msg.sender is not authorized.
+    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;
+}
+```
+
+In the previous rule, an arbitrary function of Morpho Blue `f` is called with arbitrary `data`.
+Shares of `user` on the market identified by `id` are recorded before and after this call.
+In this way, it is checked that the supply shares are increasing when the caller of the function is neither the owner of those shares (`user != e.msg.sender`) nor authorized (`!isAuthorized(user, e.msg.sender)`).
+
+## Other safety properties
+
+### Enabled LLTV and IRM
+
+Creating a market is permissionless on Morpho Blue, but some parameters should fall into the range of admitted values.
+Notably, the LLTV value should be enabled beforehand.
+The following rule checks that no market can ever exist with a LLTV that had not been previously approved.
+
+```solidity
+invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
+    isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
+```
+
+Similarly, the interest rate model (IRM) used for the market must have been previously whitelisted.
+
+### Range of the fee
+
+The governance can choose to set a fee to a given market.
+Fees are guaranteed to never exceed 25% of the interest accrued, and this is verified by the following rule.
+
+```solidity
+invariant feeInRange(MorphoHarness.Id id)
+    fee(id) <= maxFee();
+```
+
+### Sanity checks and input validation
+
+The formal verification is also taking care of other sanity checks, some of which are needed properties to verify other rules.
+For example, the following rule checks that the variable storing the last update time is no more than the current time.
+This is a sanity check, but it is also useful to ensure that there will be no underflow when computing the time elapsed since the last update.
+
+```solidity
+rule noTimeTravel(method f, env e, calldataarg args)
+filtered { f -> !f.isView }
+{
+    MorphoHarness.Id id;
+    // Assume the property before the interaction.
+    require lastUpdate(id) <= e.block.timestamp;
+    f(e, args);
+    assert lastUpdate(id) <= e.block.timestamp;
+}
+```
+
+Additional rules are verified to ensure that the sanitization of inputs is done correctly.
+
+```solidity
+rule supplyInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+    supply@withrevert(e, marketParams, assets, shares, onBehalf, data);
+    assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted;
+}
+```
+
+The previous rule checks that the `supply` function reverts whenever the `onBehalf` parameter is the address zero, or when either both `assets` and `shares` are zero or both are non-zero.
+
+## Liveness properties
+
+On top of verifying that the protocol is secured, the verification also proves that it is usable.
+Such properties are called liveness properties, and it is notably checked that the accounting is done when an interaction goes through.
+As an example, the `withdrawChangesTokensAndShares` rule checks that calling the `withdraw` function successfully will decrease the shares of the concerned account and increase the balance of the receiver.
+
+Other liveness properties are verified as well.
+Notably, it's also verified that it is always possible to exit a position without concern for the oracle.
+This is done through the verification of two rules: the `canRepayAll` rule and the `canWithdrawCollateralAll` rule.
+The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any oustanding debt.
+The `canWithdrawCollateralAll` rule ensures that in the case where the account has no outstanding debt, then it is possible to withdraw the full collateral.
+
+## Protection against common attack vectors
+
+Other common and known attack vectors are verified to not be possible on the Morpho Blue protocol.
+
+### Reentrancy
+
+Reentrancy is a common attack vector that happen when a call to a contract allows, when in a temporary state, to call the same contract again.
+The state of the contract usually refers to the storage variables, which can typically hold values that are meant to be used only after the full execution of the current function.
+The Morpho Blue contract is verified to not be vulnerable to this kind of reentrancy attack thanks to the rule `reentrancySafe`.
+
+### Extraction of value
+
+The Morpho Blue protocol uses a conservative approach to handle arithmetic operations.
+Rounding is done such that potential (small) errors are in favor of the protocol, which ensures that it is not possible to extract value from other users.
+
+The rule `supplyWithdraw` handles the simple scenario of a supply followed by a withdraw, and has the following check.
+
+```solidity
+assert withdrawnAssets <= suppliedAssets;
+```
+
+The rule `withdrawLiquidity` is more general and defines `owedAssets` as the assets that are owed to the user, rounding in favor of the protocol.
+This rule has the following check to ensure that no more than the owed assets can be withdrawn.
+
+```solidity
+assert withdrawnAssets <= owedAssets;
+```
+
+# Folder and file structure
 
 The [`certora/specs`](./specs) folder contains the following files:
 
@@ -50,12 +264,12 @@ Notably, this allows handling the fact that library functions should be called f
 
 The [`certora/dispatch`](./dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue.
 
-## Usage
+# Getting started
 
 To verify specification files, run the corresponding script in the [`certora/scripts`](./scripts) folder.
 It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
 You can pass arguments to the script, which allows you to verify specific properties. For example, at the root of the repository:
 
 ```
-./certora/scripts/verifyConsistentState.sh --rule borrowLessSupply
+./certora/scripts/verifyConsistentState.sh --rule borrowLessThanSupply
 ```

certora/specs/ConsistentState.spec

@@ -37,12 +37,12 @@ ghost mapping(MorphoHarness.Id => mathint) sumCollateral {
     init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
 }
 
-ghost mapping(address => mathint) myBalances {
-    init_state axiom (forall address token. myBalances[token] == 0);
+ghost mapping(address => mathint) balance {
+    init_state axiom (forall address token. balance[token] == 0);
 }
 
-ghost mapping(address => mathint) sumAmount {
-    init_state axiom (forall address token. sumAmount[token] == 0);
+ghost mapping(address => mathint) idleAmount {
+    init_state axiom (forall address token. idleAmount[token] == 0);
 }
 
 ghost mapping(MorphoHarness.Id => address) idToBorrowable;
@@ -67,25 +67,25 @@ hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares ui
 
 hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
-    sumAmount[idToCollateral[id]] = sumAmount[idToCollateral[id]] - oldAmount + newAmount;
+    idleAmount[idToCollateral[id]] = idleAmount[idToCollateral[id]] - oldAmount + newAmount;
 }
 
 hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE {
-    sumAmount[idToBorrowable[id]] = sumAmount[idToBorrowable[id]] - oldAmount + newAmount;
+    idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] - oldAmount + newAmount;
 }
 
 hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE {
-    sumAmount[idToBorrowable[id]] = sumAmount[idToBorrowable[id]] + oldAmount - newAmount;
+    idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] + oldAmount - newAmount;
 }
 
 function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
     if (from == currentContract) {
         // Safe require because the reference implementation would revert.
-        myBalances[token] = require_uint256(myBalances[token] - amount);
+        balance[token] = require_uint256(balance[token] - amount);
     }
     if (to == currentContract) {
         // Safe require because the reference implementation would revert.
-        myBalances[token] = require_uint256(myBalances[token] + amount);
+        balance[token] = require_uint256(balance[token] + amount);
     }
 }
 
@@ -106,7 +106,7 @@ invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
 
 // Check that a market only allows borrows up to the total supply.
 // This invariant shows that markets are independent, tokens from one market cannot be taken by interacting with another market.
-invariant borrowLessSupply(MorphoHarness.Id id)
+invariant borrowLessThanSupply(MorphoHarness.Id id)
     totalBorrowAssets(id) <= totalSupplyAssets(id);
 
 // This invariant is useful in the following rule, to link an id back to a market.
@@ -116,8 +116,8 @@ invariant marketInvariant(MorphoHarness.MarketParams marketParams)
     idToCollateral[libId(marketParams)] == marketParams.collateralToken;
 
 // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow.
-invariant isLiquid(address token)
-    sumAmount[token] <= myBalances[token]
+invariant idleAmountLessThanBalance(address token)
+    idleAmount[token] <= balance[token]
 {
     // Safe requires on the sender because the contract cannot call the function itself.
     preserved supply(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) {