added min protection to restrict underflow on `bucketTake`

ith-harvey commented 11 months ago

Description

removed possible underflow that could occur when repaying a loans debt in bucketTake flow by adding a min(t0RepayAmount, t0Debt)

Purpose

This change was suggested in our Certora audit L1 here is a lengthier description of their issue:

This points to the repayAmount that can underflow -> https://github.com/ajna-finance/ajna-core/blob/main/src/libraries/external/TakerActions.sol#L756 which points to the quote token constraint. Certora states the "round-down which computes repayAmount together with the computation of the debt collateral constraint can lead to a higher value than intended, since the later rounds up."

Here is the code:

// Collateral taken in bucket takes is constrained by the deposit available at the price including the reward.  This is moot in the case of takes.
vars.depositCollateralConstraint = (vars.unscaledDeposit != type(uint256).max) ? _roundToScale(Math.mulDiv(vars.unscaledDeposit, vars.bucketScale, netRewardedPrice), collateralScale_) : type(uint256).max;
...
vars.collateralAmount         = vars.depositCollateralConstraint;
...
vars.t0RepayAmount            = Math.mulDiv(vars.collateralAmount, borrowerPrice, inflator_);

Certora says that the repayAmount rounds down, I believe this is due to the a * b / c which can truncate any fractional part if it exceeds uint256, makes sense to me.

Then they are saying debtcollateralConstraint rounds up... well that could cause the first if to execute when the deposit in the bucket actually exceeded debt -> https://github.com/ajna-finance/ajna-core/blob/14e8655948efdb84af1a7eb96083cf9bec09d98b/src/libraries/external/TakerActions.sol#L752-L753 If that occurs then the depositCollateralConstraint -> https://github.com/ajna-finance/ajna-core/blob/14e8655948efdb84af1a7eb96083cf9bec09d98b/src/libraries/external/TakerActions.sol#L747-L748 could actually be larger than what is in the bucket. I think this is what results in the underflow since then repayAmount would exceed the debt.

Impact

Increase of a 100 gas on bucketTake

Tasks

[ ] Changes to protocol contracts are covered by unit tests executed by CI.
[ ] Protocol contract size limits have not been exceeded.
[ ] Gas consumption for impacted transactions have been compared with the target branch, and nontrivial changes cited in the Impact section above.
[ ] Scope labels have been assigned as appropriate.
[ ] Invariant tests have been manually executed as appropriate for the nature of the change.

mattcushman commented 11 months ago

I am in favor of a general change, made in _calculateTakeFlowsAndBondChange function where vars.t0RepayAmount is computed, e.g. in TakerAction#L770 to add
             vars.quoteTokenAmount         = Maths.wmul(vars.collateralAmount, vars.auctionPrice);
         }

+        // repaid amount cannot exceed the borrower owned debt
+        vars.t0RepayAmount = Maths.min(vars.t0RepayAmount, vars.t0BorrowerDebt);
+
         if (vars.isRewarded) {

I agree with this. To be honest, I'd like to see a case where this actually occurs, because we've never seen it actually happen, they didn't produce an example, and it's not clear whether is can or not (really the middle clause should trigger in most cases).

ith-harvey commented 11 months ago

Should

I am in favor of a general change, made in _calculateTakeFlowsAndBondChange function where vars.t0RepayAmount is computed, e.g. in TakerAction#L770 to add
             vars.quoteTokenAmount         = Maths.wmul(vars.collateralAmount, vars.auctionPrice);
         }

+        // repaid amount cannot exceed the borrower owned debt
+        vars.t0RepayAmount = Maths.min(vars.t0RepayAmount, vars.t0BorrowerDebt);
+
         if (vars.isRewarded) {

updated -> https://github.com/ajna-finance/contracts/pull/1033/commits/401e52bbdd32cbf3765d2eef04d5733beed64679

ajna-finance / ajna-core