Document the requirements about external contracts

[QGarchery]

A Morpho Blue is setting up a few contracts that can be called in the main functions: the IRM, the oracles, the tokens. We should define what we expect from those contracts so that the code works as expected.

For each token:

• it should respect ERC20. We can imagine many attacks otherwise, such as draining funds from another market.
• it should not be a rebasing token. Even without slashing, on the collateral, it means that the added funds are locked forever in Blue.
• EDIT: it should not be a token with fees on transfer (otherwise our accounting with totalSupply for example is wrong)

The IRM will be whitelisted by governance, but we can expect that the borrowRate function is a function that only modifies its own storage.
EDIT: The IRM is expected to be nonreentrant in the Certora verification, and it seems to be enough to prove functional correctness properties (but probably not enough to prove economical properties). This means that the IRM is allowed to change any other contract's storage.

For the oracles, we could make the same assumption as for the IRM.
EDIT: the oracle is using a view function (which compiles to STATICCALL), this means that it does not change any storage. This seems to be enough to prove functional corecctness properties. It's obviously not enough to prove economical properties: for example we could imagine an oracle that has a preferential treatment when tx.origin == user.

Note that being a user of a market comes with economical risks (for example with a badly tuned oracle). The user should assume those risks, and instead we focus in this issue on smart contract risks. Do you see more assumptions that should be made about those contracts, or can we refine the assumptions above ?

[MerlinEgalite]

The IRM will be whitelisted by governance, but we can expect that the borrowRate function is a function that only modifies its own storage.

I'm not sure it should be a requirement tbh.

For now, I don't see any other things we could add.

[MathisGD]

such as draining funds from another market.

this must not be possible, even with a token that is completely adversarial. The only thing that breaks when an "ERC20" is not compliant should be the markets with this token as borrowable or collateral (and same with IRMs, oracles).

so that the code works as expected

this should also be defined then

[QGarchery]

this must not be possible, even with a token that is completely adversarial. The only thing that breaks when an "ERC20" is not compliant should be the markets with this token as borrowable or collateral (and same with IRMs, oracles).

Yes that's what I meant: what are the requirements about external calls such that a market is sound. This issue does not require to update the code, only the documentation

[QGarchery]

Updated the description of the issue. Right now it sounds like we arrive at a pretty nice specification for the IRM and the oracle, but the token specification seems to be more tricky. In particular there can be many ways in which a particular token would not make for a sound market in Blue

[QGarchery]

In the formal verification, we used the following assumptions:

• for the token, only a transfer can change the balance and by the amount expected: a transfer of x tokens removes x from the sender, except if he is also the receiver. This prevents the use of tokens that have a fee on transfer. It should notably stay the same between two blocks, which means that it prevents the use of rebasing tokens. Tokens are not expected to change the price of the assets too. Permissions and allowances were not tested.
• for the IRM, it's assumed that it is trusted so it should not do any reentrant calls (static calls are fine obviously).
• for the oracle, nothing is required since it is a view function.

Keep in mind that these are only about the functional correctness property and not about the economical properties. Also, reverts in those contracts were not tested.

[MathisGD]

for the token, only a transfer can change the balance and by the amount expected

I feel that it's slightly too conservative: most tokens have a mint function and it should be fine from a correctness perspective. Although the burn function may cause issues.

[MathisGD]

I feel that this spec is really valuable. Concretely, what should we do with it ? Put a comment in IERC20, IIrm and IOracle ?

[QGarchery]

I feel that it's slightly too conservative: most tokens have a mint function and it should be fine from a correctness perspective. Although the burn function may cause issues.

Yes I missed that, we do test with a mint function and it's fine. There is no test with a burn function but it's pretty clear that if the Morpho contract gets its tokens burnt then there is an issue.

Put a comment in IERC20, IIrm and IOracle ?

That sounds good

[MerlinEgalite]

Or maybe a comment in the createMarket function instead?

[Rubilmax]

Or maybe a comment in the createMarket function instead?

This has a very high value to me, because it'll be printed on Etherscan