Badger eBTC Audit + Certora Formal Verification Competition - Weed0607's results

Lines of code

https://github/code-423n4/2023-10-badger/blob/main/packages/contracts/contracts/CdpManager.sol#L320

Vulnerability details

Impact

Attacker with enough eBTC can lower the system's TCR below MCR using CdpMananger.sol#redeemCollateral function. This will block other users redemptions due to the system's logic. If this happens, to recover the system there has to be a borrower creates Cdp with lots of collateral or add lots of collateral to existing Cdp. But this is loss in perspective of borrower.

Proof of Concept

Even if isRecoveryMode is true, with CdpManager.sol#redeemCollateral functoin, the malicious user can lower the TCR below MCR.

File: packages/contracts/contracts/CdpManager.sol

350: _requireTCRisNotBelowMCR(totals.price, totals.tcrAtStart);

At L350 there is a check for TCR being higher than MCR. However there is no check for TCR after redeeming. This will lead the system delinquent and will block further redemptions.

Tools Used

Manual Review

Recommended Mitigation Steps

Need to correct CdpManager.sol#redeemCollateral function to check TCR after the redemption.

458: totals.collSharesToRedeemer = totals.collSharesDrawn - totals.feeCollShares;
459+: uint256 newTotalCollShare = totals.systemCollSharesAtStart - totals.collSharesDrawn - totals.totalCollSharesSurplus;
460+: uint256 newTotalDebt = totals.systemDebtAtStart - totals.debtToRedeem;
461+: uint256 newSthEthBalance = collateral.getPooledEthByshares(new TotalCollShare);
462+: uint256 newTCR = EbtcMath._computeCR(newStEthBalance.newTotalDebt, _price);
463+: _requireTCRRisNotBelowMCR(total.price, totals.newTCR);

464+: _syncGracePeriodForGivenValues(
465+:  newTotalCollShare,
466+:  newTotalDebt,
467+: totals.price
468+);


460-: _syncGracePeriodForGivenValues(
461-:            totals.systemCollSharesAtStart - totals.collSharesDrawn - totals.totalCollSharesSurplus,
462-:            totals.systemDebtAtStart - totals.debtToRedeem,
463-:            totals.price
464-:        );

Assessed type

Invalid Validation