Skip to content

Commit 6204fa5

Browse files
QGarcheryQGarchery
authored
Merge pull request #538 from morpho-org/certora/documentation
[Certora] Documentation
2 parents 0783ddb + e4aca4c commit 6204fa5

File tree

3 files changed

+255
-41
lines changed

3 files changed

+255
-41
lines changed

‎certora/README.md

+238-24
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,242 @@
11
This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language.
22

3-
## High-Level Description
4-
5-
The Morpho Blue protocol relies on several different concepts, which are described below.
3+
The core concepts of the the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf).
64
These concepts have been verified using CVL.
7-
See the description of the specification files below (or those files directly) for more details.
8-
9-
The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.\
10-
**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.\
11-
**Markets**. Markets on Morpho Blue depend on a pair of assets, the borrowable asset that is supplied and borrowed, and the collateral asset.
12-
Markets are independent, which means that loans cannot be impacted by loans from other markets.
13-
Positions of users are also independent, so loans cannot be impacted by loans from other users.
14-
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.\
15-
**Supply.** When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
16-
Shares increase in value as interest is accrued.\
17-
**Borrow.** To borrow on Morpho Blue, collateral must be deposited.
18-
Collateral tokens remain idle, as well as any borrowable token that has not been borrowed.\
19-
**Liquidation.** To ensure proper collateralization, a liquidation system is put in place.
20-
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.\
21-
**Authorization.** Morpho Blue also defines a sound authorization system where users cannot modify positions of other users without proper authorization (except when liquidating).\
22-
**Safety.** Other safety properties are verified, particularly regarding reentrancy attacks and about input validation and revert conditions.\
23-
**Liveness.** Other liveness properties are verified as well, in particular it is always possible to exit a position without concern for the oracle.
24-
25-
## Folder and File Structure
5+
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.
6+
7+
# High-level description
8+
9+
The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens.
10+
11+
## ERC20 tokens and transfers
12+
13+
For a given market, Morpho Blue relies on the fact that the tokens involved respect the ERC20 standard.
14+
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.
15+
16+
The file [Transfer.spec](./specs/Transfer.spec) defines a summary of the transfer functions.
17+
This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected.
18+
19+
```solidity
20+
function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
21+
if (from == currentContract) {
22+
balance[token] = require_uint256(balance[token] - amount);
23+
}
24+
if (to == currentContract) {
25+
balance[token] = require_uint256(balance[token] + amount);
26+
}
27+
}
28+
```
29+
30+
where `balance` is the ERC20 balance of the Morpho Blue contract.
31+
32+
The verification is done for the most common implementations of the ERC20 standard, for which we distinguish three different implementations:
33+
34+
- [ERC20Standard](./dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance.
35+
- [ERC20NoRevert](./dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead).
36+
- [ERC20USDT](./dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions.
37+
38+
Additionally, Morpho Blue always goes through a custom transfer library to handle ERC20 tokens, notably in all the above cases.
39+
This library reverts when the transfer is not successful, and this is checked for the case of insufficient funds or insufficient allowance.
40+
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.
41+
42+
## Markets
43+
44+
The Morpho Blue contract is a singleton contract that defines different markets.
45+
Markets on Morpho Blue depend on a pair of assets, the loan token that is supplied and borrowed, and the collateral token.
46+
Taking out a loan requires to deposit some collateral, which stays idle in the contract.
47+
Additionally, every loan token that is not borrowed also stays idle in the contract.
48+
This is verified by the following property:
49+
50+
```solidity
51+
invariant idleAmountLessThanBalance(address token)
52+
idleAmount[token] <= balance[token]
53+
```
54+
55+
where `idleAmount` is the sum over all the markets of: the collateral amounts plus the supplied amounts minus the borrowed amounts.
56+
In effect, this means that funds can only leave the contract through borrows and withdrawals.
57+
58+
Additionally, it is checked that on a given market the borrowed amounts cannot exceed the supplied amounts.
59+
60+
```solidity
61+
invariant borrowLessThanSupply(MorphoHarness.Id id)
62+
totalBorrowAssets(id) <= totalSupplyAssets(id);
63+
```
64+
65+
This property, along with the previous one ensures that other markets can only impact the balance positively.
66+
Said otherwise, markets are independent: tokens from a given market cannot be impacted by operations done in another market.
67+
68+
## Shares
69+
70+
When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
71+
Shares increase in value as interest is accrued.
72+
The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest.
73+
The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement.
74+
75+
```soldidity
76+
// Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
77+
assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
78+
```
79+
80+
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.
81+
82+
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.
83+
This variable needs to be kept up to date at each corresponding interaction, and it is checked that this accounting is done properly.
84+
For example, for the supply side, this is done by the following invariant.
85+
86+
```solidity
87+
invariant sumSupplySharesCorrect(MorphoHarness.Id id)
88+
to_mathint(totalSupplyShares(id)) == sumSupplyShares[id];
89+
```
90+
91+
where `sumSupplyShares` only exists in the specification, and is defined to be automatically updated whenever any of the shares of the users are modified.
92+
93+
## Positions health and liquidations
94+
95+
To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated.
96+
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.
97+
This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1.
98+
To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected.
99+
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.
100+
101+
Let's define bad debt of a position as the amount borrowed when it is backed by no collateral.
102+
Morpho Blue automatically realizes the bad debt when liquidating a position, by transferring it to the lenders.
103+
In effect, this means that there is no bad debt on Morpho Blue, which is verified by the following invariant.
104+
105+
```solidity
106+
invariant alwaysCollateralized(MorphoHarness.Id id, address borrower)
107+
borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0;
108+
```
109+
110+
More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty).
111+
112+
## Authorization
113+
114+
Morpho Blue also defines primitive authorization system, where users can authorize an account to fully manage their position.
115+
This allows to rebuild more granular control of the position on top by authorizing an immutable contract with limited capabilities.
116+
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).
117+
118+
Let's detail the rule that makes sure that the supply side stays consistent.
119+
120+
```solidity
121+
rule userCannotLoseSupplyShares(env e, method f, calldataarg data)
122+
filtered { f -> !f.isView }
123+
{
124+
MorphoHarness.Id id;
125+
address user;
126+
127+
// Assume that the e.msg.sender is not authorized.
128+
require !isAuthorized(user, e.msg.sender);
129+
require user != e.msg.sender;
130+
131+
mathint sharesBefore = supplyShares(id, user);
132+
133+
f(e, data);
134+
135+
mathint sharesAfter = supplyShares(id, user);
136+
137+
assert sharesAfter >= sharesBefore;
138+
}
139+
```
140+
141+
In the previous rule, an arbitrary function of Morpho Blue `f` is called with arbitrary `data`.
142+
Shares of `user` on the market identified by `id` are recorded before and after this call.
143+
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)`).
144+
145+
## Other safety properties
146+
147+
### Enabled LLTV and IRM
148+
149+
Creating a market is permissionless on Morpho Blue, but some parameters should fall into the range of admitted values.
150+
Notably, the LLTV value should be enabled beforehand.
151+
The following rule checks that no market can ever exist with a LLTV that had not been previously approved.
152+
153+
```solidity
154+
invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
155+
isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
156+
```
157+
158+
Similarly, the interest rate model (IRM) used for the market must have been previously whitelisted.
159+
160+
### Range of the fee
161+
162+
The governance can choose to set a fee to a given market.
163+
Fees are guaranteed to never exceed 25% of the interest accrued, and this is verified by the following rule.
164+
165+
```solidity
166+
invariant feeInRange(MorphoHarness.Id id)
167+
fee(id) <= maxFee();
168+
```
169+
170+
### Sanity checks and input validation
171+
172+
The formal verification is also taking care of other sanity checks, some of which are needed properties to verify other rules.
173+
For example, the following rule checks that the variable storing the last update time is no more than the current time.
174+
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.
175+
176+
```solidity
177+
rule noTimeTravel(method f, env e, calldataarg args)
178+
filtered { f -> !f.isView }
179+
{
180+
MorphoHarness.Id id;
181+
// Assume the property before the interaction.
182+
require lastUpdate(id) <= e.block.timestamp;
183+
f(e, args);
184+
assert lastUpdate(id) <= e.block.timestamp;
185+
}
186+
```
187+
188+
Additional rules are verified to ensure that the sanitization of inputs is done correctly.
189+
190+
```solidity
191+
rule supplyInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
192+
supply@withrevert(e, marketParams, assets, shares, onBehalf, data);
193+
assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted;
194+
}
195+
```
196+
197+
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.
198+
199+
## Liveness properties
200+
201+
On top of verifying that the protocol is secured, the verification also proves that it is usable.
202+
Such properties are called liveness properties, and it is notably checked that the accounting is done when an interaction goes through.
203+
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.
204+
205+
Other liveness properties are verified as well.
206+
Notably, it's also verified that it is always possible to exit a position without concern for the oracle.
207+
This is done through the verification of two rules: the `canRepayAll` rule and the `canWithdrawCollateralAll` rule.
208+
The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any oustanding debt.
209+
The `canWithdrawCollateralAll` rule ensures that in the case where the account has no outstanding debt, then it is possible to withdraw the full collateral.
210+
211+
## Protection against common attack vectors
212+
213+
Other common and known attack vectors are verified to not be possible on the Morpho Blue protocol.
214+
215+
### Reentrancy
216+
217+
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.
218+
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.
219+
The Morpho Blue contract is verified to not be vulnerable to this kind of reentrancy attack thanks to the rule `reentrancySafe`.
220+
221+
### Extraction of value
222+
223+
The Morpho Blue protocol uses a conservative approach to handle arithmetic operations.
224+
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.
225+
226+
The rule `supplyWithdraw` handles the simple scenario of a supply followed by a withdraw, and has the following check.
227+
228+
```solidity
229+
assert withdrawnAssets <= suppliedAssets;
230+
```
231+
232+
The rule `withdrawLiquidity` is more general and defines `owedAssets` as the assets that are owed to the user, rounding in favor of the protocol.
233+
This rule has the following check to ensure that no more than the owed assets can be withdrawn.
234+
235+
```solidity
236+
assert withdrawnAssets <= owedAssets;
237+
```
238+
239+
# Folder and file structure
26240

27241
The [`certora/specs`](./specs) folder contains the following files:
28242

@@ -50,12 +264,12 @@ Notably, this allows handling the fact that library functions should be called f
50264

51265
The [`certora/dispatch`](./dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue.
52266

53-
## Usage
267+
# Getting started
54268

55269
To verify specification files, run the corresponding script in the [`certora/scripts`](./scripts) folder.
56270
It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
57271
You can pass arguments to the script, which allows you to verify specific properties. For example, at the root of the repository:
58272

59273
```
60-
./certora/scripts/verifyConsistentState.sh --rule borrowLessSupply
274+
./certora/scripts/verifyConsistentState.sh --rule borrowLessThanSupply
61275
```

‎certora/specs/ConsistentState.spec

+12-12
Original file line numberDiff line numberDiff line change
@@ -37,12 +37,12 @@ ghost mapping(MorphoHarness.Id => mathint) sumCollateral {
3737
init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0);
3838
}
3939

40-
ghost mapping(address => mathint) myBalances {
41-
init_state axiom (forall address token. myBalances[token] == 0);
40+
ghost mapping(address => mathint) balance {
41+
init_state axiom (forall address token. balance[token] == 0);
4242
}
4343

44-
ghost mapping(address => mathint) sumAmount {
45-
init_state axiom (forall address token. sumAmount[token] == 0);
44+
ghost mapping(address => mathint) idleAmount {
45+
init_state axiom (forall address token. idleAmount[token] == 0);
4646
}
4747

4848
ghost mapping(MorphoHarness.Id => address) idToBorrowable;
@@ -67,25 +67,25 @@ hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares ui
6767

6868
hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE {
6969
sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
70-
sumAmount[idToCollateral[id]] = sumAmount[idToCollateral[id]] - oldAmount + newAmount;
70+
idleAmount[idToCollateral[id]] = idleAmount[idToCollateral[id]] - oldAmount + newAmount;
7171
}
7272

7373
hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE {
74-
sumAmount[idToBorrowable[id]] = sumAmount[idToBorrowable[id]] - oldAmount + newAmount;
74+
idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] - oldAmount + newAmount;
7575
}
7676

7777
hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE {
78-
sumAmount[idToBorrowable[id]] = sumAmount[idToBorrowable[id]] + oldAmount - newAmount;
78+
idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] + oldAmount - newAmount;
7979
}
8080

8181
function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
8282
if (from == currentContract) {
8383
// Safe require because the reference implementation would revert.
84-
myBalances[token] = require_uint256(myBalances[token] - amount);
84+
balance[token] = require_uint256(balance[token] - amount);
8585
}
8686
if (to == currentContract) {
8787
// Safe require because the reference implementation would revert.
88-
myBalances[token] = require_uint256(myBalances[token] + amount);
88+
balance[token] = require_uint256(balance[token] + amount);
8989
}
9090
}
9191

@@ -106,7 +106,7 @@ invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
106106

107107
// Check that a market only allows borrows up to the total supply.
108108
// This invariant shows that markets are independent, tokens from one market cannot be taken by interacting with another market.
109-
invariant borrowLessSupply(MorphoHarness.Id id)
109+
invariant borrowLessThanSupply(MorphoHarness.Id id)
110110
totalBorrowAssets(id) <= totalSupplyAssets(id);
111111

112112
// 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)
116116
idToCollateral[libId(marketParams)] == marketParams.collateralToken;
117117

118118
// 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.
119-
invariant isLiquid(address token)
120-
sumAmount[token] <= myBalances[token]
119+
invariant idleAmountLessThanBalance(address token)
120+
idleAmount[token] <= balance[token]
121121
{
122122
// Safe requires on the sender because the contract cannot call the function itself.
123123
preserved supply(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) {

0 commit comments

Comments
 (0)