From a6b46673c4e975f4b401b04fe2d24ed87be8dccc Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 6 Oct 2023 10:27:54 +0200 Subject: [PATCH 1/9] docs: certora documentation layout --- certora/README.md | 73 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 58 insertions(+), 15 deletions(-) diff --git a/certora/README.md b/certora/README.md index 48e987103..11a128e14 100644 --- a/certora/README.md +++ b/certora/README.md @@ -2,25 +2,68 @@ This folder contains the verification of the Morpho Blue protocol using CVL, Cer ## High-Level Description -The Morpho Blue protocol relies on several different concepts, which are described below. +The Morpho Blue protocol relies on several different concepts, which are described in the Whitepaper. These concepts have been verified using CVL. -See the description of the specification files below (or those files directly) for more details. +For more details, see the description of the specification below or the description of the specification files in the next section. -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. +The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. + +```solidity +rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + supply(e, marketParams, assets, shares, onBehalf, data); + storage afterBoth = lastStorage; + + supply(e, marketParams, assets, shares, onBehalf, data) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} +``` + +### 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. +Morpho Blue uses a transfer library to handle different tokens, including tokens that do not strictly respect the standard, in particular, when the return value on transfer and transferFrom function are missing, such as for the USDT token. This is difficult for the prover, so a summary is used to ease the verification of rules that rely on the transfer of tokens. This summary is verified to behave as expected in the Transfer.spec file. + +### 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. +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 From b4271a2ef369c66ee3a2731a6a6a8885672f81f9 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 12 Oct 2023 16:03:30 +0200 Subject: [PATCH 2/9] docs: certora documentation of transfers --- certora/README.md | 48 ++++++++++++++++++++++++++--------------------- 1 file changed, 27 insertions(+), 21 deletions(-) diff --git a/certora/README.md b/certora/README.md index 11a128e14..ad1a68dfa 100644 --- a/certora/README.md +++ b/certora/README.md @@ -1,35 +1,41 @@ 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 in the Whitepaper. +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. -For more details, see the description of the specification below or the description of the specification files in the next section. +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. -The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. +## High-Level description -```solidity -rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - // Safe require because timestamps cannot realistically be that large. - require e.block.timestamp < 2^128; +The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. - storage init = lastStorage; +### Transfers - accrueInterest(e, marketParams); - supply(e, marketParams, assets, shares, onBehalf, data); - storage afterBoth = lastStorage; +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. - supply(e, marketParams, assets, shares, onBehalf, data) at init; - storage afterOne = lastStorage; +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. - assert afterBoth == afterOne; +```solidity +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + myBalances[token] = require_uint256(myBalances[token] - amount); + } + if (to == currentContract) { + myBalances[token] = require_uint256(myBalances[token] + amount); + } } ``` -### Transfers +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. -Token transfers are verified to behave as expected for the most common implementations, in particular the transferred amount is the amount passed as input. -Morpho Blue uses a transfer library to handle different tokens, including tokens that do not strictly respect the standard, in particular, when the return value on transfer and transferFrom function are missing, such as for the USDT token. This is difficult for the prover, so a summary is used to ease the verification of rules that rely on the transfer of tokens. This summary is verified to behave as expected in the Transfer.spec file. +Additionally, Morpho Blue always goes through a custom transfer library to handle tokens 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 @@ -65,7 +71,7 @@ Other safety properties are verified, particularly regarding reentrancy attacks 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 +## Folder and file structure The [`certora/specs`](./specs) folder contains the following files: @@ -93,7 +99,7 @@ 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. From f75498074b307e942e5a54e719e1b72735cea5b1 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 12 Oct 2023 17:20:13 +0200 Subject: [PATCH 3/9] docs: certora documentation of markets --- certora/README.md | 60 ++++++++++++++++++++---------- certora/specs/ConsistentState.spec | 22 +++++------ 2 files changed, 52 insertions(+), 30 deletions(-) diff --git a/certora/README.md b/certora/README.md index ad1a68dfa..3e6d61111 100644 --- a/certora/README.md +++ b/certora/README.md @@ -4,11 +4,11 @@ The core concepts of the the Morpho Blue protocol are described in the [Whitepap These concepts have been verified using CVL. 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 +# High-level description The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. -### Transfers +## 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. @@ -19,10 +19,10 @@ This summary is taken as the reference implementation to check that the balance ```solidity function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { if (from == currentContract) { - myBalances[token] = require_uint256(myBalances[token] - amount); + balance[token] = require_uint256(balance[token] - amount); } if (to == currentContract) { - myBalances[token] = require_uint256(myBalances[token] + amount); + balance[token] = require_uint256(balance[token] + amount); } } ``` @@ -37,41 +37,63 @@ Additionally, Morpho Blue always goes through a custom transfer library to handl 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 +## 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. +Morpho Blue 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 idleAmountLessBalance(address token) + idleAmount[token] <= balance[token] +``` -### Supply +where `balance` is the ERC20 balance of the singleton, and 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 borrowLessSupply(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. -### Borrow +The accounting of the markets has been verified (such as the total shares), . -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 +## Health 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. +## Safety + ### Authorization Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating). -### Safety +Positions of users are also independent, so loans cannot be impacted by loans from other users. + +### Others Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions. -### Liveness +as well as the fact that only market with enabled parameters are created + +## 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 +# Folder and file structure The [`certora/specs`](./specs) folder contains the following files: @@ -99,7 +121,7 @@ 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. -## Getting started +# 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. diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 3b78703fc..1f2fd51c5 100644 --- a/certora/specs/ConsistentState.spec +++ b/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); } } @@ -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 idleAmountLessBalance(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) { From 375a86b4543ac99b2c3d6c83eb38ce3208deef04 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Thu, 12 Oct 2023 17:45:23 +0200 Subject: [PATCH 4/9] docs: certora documentation of shares --- certora/README.md | 30 +++++++++++++++++++++++++----- certora/specs/ConsistentState.spec | 4 ++-- certora/specs/RatioMath.spec | 10 +++++----- 3 files changed, 32 insertions(+), 12 deletions(-) diff --git a/certora/README.md b/certora/README.md index 3e6d61111..c1e3edd31 100644 --- a/certora/README.md +++ b/certora/README.md @@ -27,6 +27,8 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 } ``` +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. @@ -39,24 +41,24 @@ The use of the library can make it difficult for the provers, so the summary is ## Markets -Morpho Blue is a singleton contract that defines different 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 idleAmountLessBalance(address token) +invariant idleAmountLessThanBalance(address token) idleAmount[token] <= balance[token] ``` -where `balance` is the ERC20 balance of the singleton, and where `idleAmount` is the sum over all the markets of: the collateral amounts plus the supplied amounts minus the borrowed amounts. +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 borrowLessSupply(MorphoHarness.Id id) +invariant borrowLessThanSupply(MorphoHarness.Id id) totalBorrowAssets(id) <= totalSupplyAssets(id); ``` @@ -67,8 +69,26 @@ Said otherwise, markets are independent: tokens from a given market cannot be im 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]; +``` -The accounting of the markets has been verified (such as the total shares), . +where `sumSupplyShares` only exists in the specification, and is defined to be automatically updated whenever any of the shares of the users are modified. ## Health diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 1f2fd51c5..5324bd5b4 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -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,7 +116,7 @@ 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 idleAmountLessBalance(address token) +invariant idleAmountLessThanBalance(address token) idleAmount[token] <= balance[token] { // Safe requires on the sender because the contract cannot call the function itself. diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec index 21dc1050a..af690462e 100644 --- a/certora/specs/RatioMath.spec +++ b/certora/specs/RatioMath.spec @@ -51,7 +51,7 @@ rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams market mathint assetsAfter = virtualTotalSupplyAssets(id); mathint sharesAfter = virtualTotalSupplyShares(id); - // Check that ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; } @@ -69,7 +69,7 @@ rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams market mathint assetsAfter = virtualTotalBorrowAssets(id); mathint sharesAfter = virtualTotalBorrowShares(id); - // Check that ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; } @@ -95,7 +95,7 @@ filtered { mathint assetsAfter = virtualTotalSupplyAssets(id); mathint sharesAfter = virtualTotalSupplyShares(id); - // Check that ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; } @@ -123,7 +123,7 @@ filtered { mathint assetsAfter = virtualTotalBorrowAssets(id); mathint sharesAfter = virtualTotalBorrowShares(id); - // Check that ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; } @@ -151,6 +151,6 @@ rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u mathint sharesAfter = virtualTotalBorrowShares(id); assert assetsAfter == assetsBefore - repaidAssets; - // Check that ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; } From 8a4d786a4d09516f388c7714590efe6ba432d941 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 13 Oct 2023 10:40:22 +0200 Subject: [PATCH 5/9] docs: certora documentation of health --- certora/README.md | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/certora/README.md b/certora/README.md index c1e3edd31..af2067f8c 100644 --- a/certora/README.md +++ b/certora/README.md @@ -35,7 +35,7 @@ The verification is done for the most common implementations of the ERC20 standa - [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 tokens in all the above cases. +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. @@ -92,8 +92,22 @@ where `sumSupplyShares` only exists in the specification, and is defined to be a ## Health -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. +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 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). ## Safety From b90cdb2200eaa31f42947a289a7f3c1675f1d435 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 13 Oct 2023 11:06:15 +0200 Subject: [PATCH 6/9] docs: certora documentation of authorization --- certora/README.md | 35 +++++++++++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 4 deletions(-) diff --git a/certora/README.md b/certora/README.md index af2067f8c..c4f8738ac 100644 --- a/certora/README.md +++ b/certora/README.md @@ -109,13 +109,40 @@ invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty). -## Safety +## 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; -### Authorization + mathint sharesBefore = supplyShares(id, user); -Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating). + f(e, data); -Positions of users are also independent, so loans cannot be impacted by loans from other users. + 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)`). + +## Safety ### Others From a32acdba306cf9618a4f4fed1494a9e1b7a227c2 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 13 Oct 2023 11:57:22 +0200 Subject: [PATCH 7/9] docs: certora documentation of other safety properties --- certora/README.md | 64 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 58 insertions(+), 6 deletions(-) diff --git a/certora/README.md b/certora/README.md index c4f8738ac..cec52be1d 100644 --- a/certora/README.md +++ b/certora/README.md @@ -93,7 +93,7 @@ where `sumSupplyShares` only exists in the specification, and is defined to be a ## Health 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 LLTV of that market. +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. @@ -142,18 +142,70 @@ In the previous rule, an arbitrary function of Morpho Blue `f` is called with ar 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)`). -## Safety +## Other safety properties -### Others +### Enabled LLTV and IRM -Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions. +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. -as well as the fact that only market with enabled parameters are created +```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; +} +``` -## Liveness +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 Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle. +## Protection against common attack vectors + +### Reentrancy + +### Extraction of value + # Folder and file structure The [`certora/specs`](./specs) folder contains the following files: From 35de6cf5771b0bf7d272ca3a2f2445aadd38ea20 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 13 Oct 2023 13:12:24 +0200 Subject: [PATCH 8/9] docs: certora documentation of liveness properties --- certora/README.md | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/certora/README.md b/certora/README.md index cec52be1d..aa9ebc41e 100644 --- a/certora/README.md +++ b/certora/README.md @@ -90,7 +90,7 @@ invariant sumSupplySharesCorrect(MorphoHarness.Id 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. -## Health +## 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. @@ -198,7 +198,15 @@ The previous rule checks that the `supply` function reverts whenever the `onBeha ## Liveness properties -Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle. +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 From e4aca4ce5ec01fe919c9c4067ee17c12fd11991b Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Fri, 13 Oct 2023 14:08:42 +0200 Subject: [PATCH 9/9] docs: certora documentation of protection against common attack vectors --- certora/README.md | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/certora/README.md b/certora/README.md index aa9ebc41e..df41364b3 100644 --- a/certora/README.md +++ b/certora/README.md @@ -210,10 +210,32 @@ The `canWithdrawCollateralAll` rule ensures that in the case where the account h ## 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: @@ -249,5 +271,5 @@ It requires having set the `CERTORAKEY` environment variable to a valid Certora 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 ```