[Certora] Check allowance to untrusted contracts are reset

[colin-morpho]

This PR checks that allowances to untrusted contract are reset.
A malicious ERC20 called within a bundle could steal tokens within some transactions, for this reason we wish to check that that untrusted contracts are allowed only during the execution of some calls before resetting the allowance to zero.
We check this only for untrusted contracts (Morpho, WETH, ST_ETH) by checking that the allowance equals zero for approved untrusted contracts on entrypoints of interest.

Please ensure that:

• the documentation is updates;
• the verification succeeds;
• the CI has been configured.

[colin-morpho]

Note: I haven't managed to write a spec for Compound versions 2 and 3 migration adapters as it seems that we need concrete implementations that are able to resolve the underlying ERC20 contracts.

Namely, in this line https://github.com/morpho-org/bundler-v3/blob/a3a2d6ccf3002bde2a654bd20a76accf40985642/certora/specs/CompoundV2Approvals.spec#L12, we do not have an implementation for a CToken similarly for this line https://github.com/morpho-org/bundler-v3/blob/a3a2d6ccf3002bde2a654bd20a76accf40985642/certora/specs/CompoundV3Approvals.spec#L12 can't resolve the instance for obvious reasons. I don't know how to deal whit this, @QGarchery do you think we should either dispatch (adding the necessary implementations) or adding a helper that returns an address to an ERC20 to summarize these calls?

[colin-morpho]

The Paraswap adatper verification doesn't go through since the summary in https://github.com/morpho-org/bundler-v3/blob/a3a2d6ccf3002bde2a654bd20a76accf40985642/certora/specs/ParaswapApprovals.spec#L8 doesn't seem to resolve the call to approve because of the call to the augustus. In d74106b I tried using an unresolved-catchall summary which does not work because the summary is too strong (it resolves view functions to HAVOC_ECF). In 3a0cee3 I replace the default case to NONDET, which goes through but doens't seem to be sound. I think this over-approximation is not sound here, what's your take @QGarchery ?

[QGarchery]

I don't know how to deal whit this, @QGarchery do you think we should either dispatch (adding the necessary implementations) or adding a helper that returns an address to an ERC20 to summarize these calls?

I think it's completely fine to use the PER_CALLEE_CONSTANT summary here. The calls to instance.baseToken() and cToken.underlying() should be constant for the purpose of these rules, as we just want talk about the value returned by those calls that is used in the corresponding bundler functions. Another way to see it is that, if we could have done it, we would have added a specification at the end the bundler functions that would describe the approvals of those assets. For example, in compoundV2RepayErc20, we could have written at the end, something like assert IERC20(underlying).allowance(address(this), cToken) == 0

[QGarchery]

I think this over-approximation is not sound here, what's your take @QGarchery ?

I agree that it's not sound, and probably too big of an over-approximation. This is because it makes so the call to the augustus is not changing the state, but this call is central to the adapter

I tried using an unresolved-catchall summary which does not work because the summary is too strong (it resolves view functions to HAVOC_ECF).

We could try an intermediate solution, and add the view functions to the dispatch list. This way the call to the augustus is HAVOC_ECF and the view functions can be NONDET

[colin-morpho]

We could try an intermediate solution, and add the view functions to the dispatch list. This way the call to the augustus is HAVOC_ECF and the view functions can be NONDET

@QGarchery I think this what I did here d74106b#diff-4a5172dbceb3687fac0c19042e758db96ebfe6166c9649e2429f508ed2caf6a1R8, or am I missing something?

[colin-morpho]

I think it's completely fine to use the PER_CALLEE_CONSTANT summary here. The calls to instance.baseToken() and cToken.underlying() should be constant for the purpose of these rules, as we just want talk about the value returned by those calls that is used in the corresponding bundler functions. Another way to see it is that, if we could have done it, we would have added a specification at the end the bundler functions that would describe the approvals of those assets. For example, in compoundV2RepayErc20, we could have written at the end, something like assert IERC20(underlying).allowance(address(this), cToken) == 0

Sorry @QGarchery , I wasn't completely clear. To able to use PER_CALLEE_CONSTANT we still need to provide an implementation, if I understand properly (c.f. d65ccdb). The prover complains as the call to token.underlying() in the spec can't be resolved.

Compiling test/helpers/mocks/ERC20Mock.sol to expose internal function information and local variables...
ERROR: Failed to run Certora Prover locally. Please check the errors below for problems in the specifications (.spec files) or the prover_args defined in the .conf file.
CRITICAL: [main] ERROR ALWAYS - Found errors in certora/specs/CompoundV2Approvals.spec:
CRITICAL: [main] ERROR ALWAYS - Error in spec file (CompoundV2Approvals.spec:12:12): Did not find any contract functions that match the given name and arguments

CVL specification syntax and type check failed

[QGarchery]

Sorry @QGarchery , I wasn't completely clear. To able to use PER_CALLEE_CONSTANT we still need to provide an implementation, if I understand properly (c.f. d65ccdb). The prover complains as the call to token.underlying() in the spec can't be resolved.

Oh right, yes you need it because you call it in the spec. Then I guess you could have a summary that depends on the e.msg.sender

[colin-morpho]

Oh right, yes you need it because you call it in the spec. Then I guess you could have a summary that depends on the e.msg.sender

Sorry, I don't understand why it should depend on e.msg.sender? Could you give me an intuition please?

[QGarchery]

Sorry, I don't understand why it should depend on e.msg.sender? Could you give me an intuition please?

It's wrong, it should not depend on e.msg.sender (I was thinking that token.underlying() was an external call, but it isn't). Honestly using a summary that is essentially constant may be enough, similarly to what we did with mockPrice in morpho-blue

[colin-morpho]

It's wrong, it should not depend on e.msg.sender (I was thinking that token.underlying() was an external call, but it isn't). Honestly using a summary that is essentially constant may be enough, similarly to what we did with mockPrice in morpho-blue

I've tried this in aa18540 it looks like it's working. Only the Paraswap case is missing now!

[MathisGD]

We check this only for untrusted contracts (Morpho, WETH, ST_ETH)

Note that we never allow WETH, actually

And that we don't reset the allowance for the MORPHO wrapper as well

[QGarchery]

Could we also check that there is no allowance given for the destToken ? It should hold as well, because allowances are not changed for this token. See this related thread

[colin-morpho]

@QGarchery should I still do this or not?

[MathisGD]

here, we could have messed up the token for which we are doing the verif, and actually have an error. We could have checked that for a given address, if there was a call to approve, the last one was with amount=0.

[colin-morpho]

On a second thought, I'm not completely convinced of specifying things like this. I don't find it nice to read because you can't convince yourself that the approve 0 has been done on the token of interest. Also, a malicious token could make a dummy approve 0 and internally not change the allowance, here we actually check the allowance.

[colin-morpho]

I've pushed an alternative (much simpler specification) see #238, let me know which one you prefer.

[MathisGD]

Replaced by #238