Imprecision on liquidity index calculation due to reserve.accruedToTreasury

[eboadom]

Problem

Currently, the depositors on the protocol accrue yield over time via the ever-growing liquidityIndex multiplying their scaled balanced of aToken. This "growth" happens in 3 different places:

1. For what concerns dynamics of debt growth and with it the yield to be given to depositors, on _updateIndexes() https://github.com/aave/aave-v3-core/blob/master/contracts/protocol/libraries/logic/ReserveLogic.sol#L295
2. For flash loan fees to depositors, on _handleFlashLoanRepayment() https://github.com/aave/aave-v3-core/blob/master/contracts/protocol/libraries/logic/FlashLoanLogic.sol#L233
3. For bridging fees (unbacked/portals), on executeBackUnbacked() https://github.com/aave/aave-v3-core/blob/master/contracts/protocol/libraries/logic/BridgeLogic.sol#L127

The problem is that, at the moment, the protocol is not taking into account correctly the entities with "rights to withdraw underlying" that are not aToken holders. Mainly this applies to reserve.accruedToTreasury, which factually should act like aToken scaled balance: not minted yet, but accruing yield like any other holder of aToken.

For example in the case of flash on 2), it is relatively straightforward to see that by using the IERC20(reserveCache.aTokenAddress).totalSupply() (within cumulateToLiquidityIndex() as a divisor) instead of supply + reserve.accruedToTreasury, the effect is that the liquidity index increases on each flash loan fee by more than it should (smaller divisor, bigger result). The situation on the BridgeLogic is the same.
Even if not a totally major one, this is obviously problematic, because as the non-claimed accruedToTreasury is bigger (if not claimed frequently), the imprecision also gets bigger; the liquidity index increases more than it should.

reserveCache.nextLiquidityIndex = reserve.cumulateToLiquidityIndex(
      IERC20(reserveCache.aTokenAddress).totalSupply(),
      premiumToLP
);

Flash loan logic of liquidity index increment

It is important to highlight that the problem of assuming rights to withdraw underlying == aToken.totalSupply() instead of rights to withdraw underlying == aToken.totalSupply() + accruedToTreasury can potentially be affecting in other places like validations involving supply, even if at the moment we don't see any big problem.

Potential solutions
Mainly 2 options here:

1. Adding the accruedToTreasury in all the calculations involving rights to withdraw underlying. Probably the most realistic option, given that the pattern of having multiple sources for those rights (aToken supply, accruedToTreasury) is already in place.
2. Mint always aTokens to the Collector, instead of incrementing accruedToTreasury. Same approach as on v2, but removed because of gas considerations. Less realistic option, but gas profiling is worth it in my opinion.

In addition to the fix itself, it is pretty clear that the current Certora properties are not extensive enough, as this specific case was not caught in multiple places of the codebase. So highly recommended to both add new rules and do a bigger review of all the invariants of the protocol.

[eboadom]

As a reproduction of the problem, this is the state of the protocol when doing:

• Deposit of 1 WETH by single depositor
• Flash loan of 0.8 WETH, paying fees both for depositors and accruedToTreasury
• Another flash loan of 0.8 WETH, adding more fees for both depositors and accruedToTreasury

As expected, there is a diff post-second flash loan, which should not be there

(aWETH scaled balance of depositor + accruedToTreasury) * liquidity index
1001440108809160183
balanceOf() of WETH within the aWETH contract
1001440000000000000

---------------------------------------------
--> Base state: 1 single depositor with 1 WETH
---------------------------------------------

Scaled total supply of aWETH
1000000000000000000
Total supply of aWETH
1000000000000000000
Current liquidity index (same as normalized income intra-action)
1000000000000000000000000000
Fees to liquidity providers
504000000000000
aWETH scaled balance of the only depositor
1000000000000000000
accruedToTreasury (not minted yet)
0
aWETH scaled balance of depositor + accruedToTreasury
1000000000000000000
(aWETH scaled balance of depositor + accruedToTreasury) * liquidity index
1000000000000000000
balanceOf() of WETH within the aWETH contract
1000000000000000000

---------------------------------------------
--> Flash of 0.8 WETH
---------------------------------------------

Scaled total supply of aWETH
1000000000000000000
Total supply of aWETH
1000504000000000000
Current liquidity index (same as normalized income intra-action)
1000504000000000000000000000
Fees to liquidity providers
504000000000000
aWETH scaled balance of the only depositor
1000000000000000000
accruedToTreasury (not minted yet)
215891190839817
aWETH scaled balance of depositor + accruedToTreasury
1000215891190839817
(aWETH scaled balance of depositor + accruedToTreasury) * liquidity index
1000720000000000000
balanceOf() of WETH within the aWETH contract
1000720000000000000

---------------------------------------------
--> Flash of 0.8 WETH
---------------------------------------------

Scaled total supply of aWETH
1000000000000000000
Total supply of aWETH
1001008000000000000
Current liquidity index (same as normalized income intra-action)
1001008000000000000000000000
Fees to liquidity providers
504000000000000
aWETH scaled balance of the only depositor
1000000000000000000
accruedToTreasury (not minted yet)
431673682088638
aWETH scaled balance of depositor + accruedToTreasury
1000431673682088638
(aWETH scaled balance of depositor + accruedToTreasury) * liquidity index
1001440108809160183
balanceOf() of WETH within the aWETH contract
1001440000000000000

[eboadom]

Implementation-wise, after doing some gas profiling and evaluating the consequences of changing to mint all the time aTokens to the Collector, it seems the optimal solution is to just extend the part of the code using totalSupply() (and similar) of aToken, to include accruedToTreasury

[miguelmtzinf]

Thanks for the detailed analysis @eboadom . I agree with the chosen approach