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

Lines of code

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

Vulnerability details

Impact

Most actions that modify the (ICR) of a Collateralized Debt Position (CDP) must adhere to specific regulations to maintain the system's stability. For instance, closing a CDP or decreasing its collateral is not permitted if it would trigger the system's recovery mode, or if the system is already in that mode.

However, the rules for redemptions are less stringent. The only conditions are that both the system and the CDPs undergoing redemption must have an TCR and ICR above the MCR. So, it is possible to redeem a cdp that is actually helping the system to stay healthy.

Proof of Concept

Follow the next steps to run the coded proof of concept:

• Copy and paste the following test under test/CdpManagerTest.js:

it.only("redeemCollateral(): Is inconsistent with other cdp behaviors", async () => {
    await contracts.collateral.deposit({from: A, value: dec(1000, 'ether')});
    await contracts.collateral.approve(borrowerOperations.address, mv._1Be18BN, {from: A});
    await contracts.collateral.deposit({from: B, value: dec(1000, 'ether')});
    await contracts.collateral.approve(borrowerOperations.address, mv._1Be18BN, {from: B});
    await contracts.collateral.deposit({from: C, value: dec(1000, 'ether')});
    await contracts.collateral.approve(borrowerOperations.address, mv._1Be18BN, {from: C});

    // @audit-info Current BTC / ETH price is 1.
    const newPrice = dec(1, 18);
    await priceFeed.setPrice(newPrice)

    // @audit-info Open some CDPs.
    await borrowerOperations.openCdp(dec(400, 18), A, A, dec(1000, 'ether'), { from: A })
    await borrowerOperations.openCdp(dec(75, 18), B, B, dec(100, 'ether'), { from: B })
    await borrowerOperations.openCdp(dec(75, 18), C, C, dec(100, 'ether'), { from: C })

    let _aCdpId = await sortedCdps.cdpOfOwnerByIndex(A, 0);
    let _bCdpId = await sortedCdps.cdpOfOwnerByIndex(B, 0);
    let _cCdpId = await sortedCdps.cdpOfOwnerByIndex(C, 0);

    const price = await priceFeed.getPrice()
    
    const currentTCR = await cdpManager.getSyncedTCR(price);
    console.log("TCR of the system before price reduction: " + currentTCR.toString())

    // @audit-info Some price reduction.
    const newPrice2 = dec(6, 17);
    await priceFeed.setPrice(newPrice2)

    const price2 = await priceFeed.getPrice()

    const currentTCR2 = await cdpManager.getSyncedTCR(price2);
    console.log("TCR of the system after price reduction" + currentTCR2.toString())

    // @audit-info All cdps are in the linked list.
    assert.isTrue(await sortedCdps.contains(_aCdpId))
    assert.isTrue(await sortedCdps.contains(_bCdpId))
    assert.isTrue(await sortedCdps.contains(_cCdpId))

    await cdpManager.setBaseRate(0) 

    // @audit-info Redemption of 400 eBTC.
    const EBTCRedemption = dec(400, 18)
    await th.redeemCollateralAndGetTxObject(A, contracts, EBTCRedemption, GAS_PRICE, th._100pct)

    // @audit-info Redemption will happen to A's position because B and C ICRs are below MCR.
    assert.isFalse(await sortedCdps.contains(_aCdpId))
    assert.isTrue(await sortedCdps.contains(_bCdpId))
    assert.isTrue(await sortedCdps.contains(_cCdpId))
    
    // @audit-issue UNDERCOLLATERALIZED
    const currentTCR3 = await cdpManager.getSyncedTCR(price2);
    console.log("TCR after redemption: " + currentTCR3.toString())
  })

This proof of concept highlights a significant risk: a situation where the entire system becomes undercollateralized. Although the likelihood of this occurring is low, there are other, more probable scenarios to consider. One such scenario involves executing one or multiple redemptions that push the system into recovery mode.

Currently, there's a redemption fee in place that escalates the cost of withdrawing large amounts of collateral, serving as a financial deterrent to potential manipulation. However, this is primarily an economic obstacle. Given that eBTC aims to be a fundamental component for Bitcoin in the Ethereum DeFi ecosystem, it's crucial to ensure that redemptions do not jeopardize the system's stability.

It should also be noted that the RiskDao's analysis regarding redemptions does not extend to situations where redemptions are strategically used to affect the system's collateralization.

Tools Used

Manual Review

Recommended Mitigation Steps

Redemptions should have the same rules for other cdp changes. For example:

• Redeeming should not let the system in RM
• Redeeming should not be possible if the system is in RM unless it makes the system to get out of RM

Assessed type

Other

Lines of code

https://github.com/code-423n4/2023-10-badger/blob/f2f2e2cf9965a1020661d179af46cb49e993cb7e/packages/contracts/contracts/LeverageMacroBase.sol#L173

Vulnerability details

Impact

The doOperation function in the LeverageMacroBase allows to make post conditions checks depending on the operations that was carried out. One of these checks can be done after opening a cdp, lets check how this is carried out.

// ...

uint256 initialCdpIndex;
if (postCheckType == PostOperationCheck.openCdp) {
   initialCdpIndex = sortedCdps.cdpCountOf(address(this));
}

// ...

if (postCheckType == PostOperationCheck.openCdp) {
   bytes32 cdpId = sortedCdps.cdpOfOwnerByIndex(address(this), initialCdpIndex);

   // Check for param details
   ICdpManagerData.Cdp memory cdpInfo = cdpManager.Cdps(cdpId);
   _doCheckValueType(checkParams.expectedDebt, cdpInfo.debt);
   _doCheckValueType(checkParams.expectedCollateral, cdpInfo.coll);
   require(
       cdpInfo.status == checkParams.expectedStatus,
       "!LeverageMacroReference: openCDP status check"
   );
}

First of all is using the functions sortedCdps.cdpCountOf and sortedCdps.cdpOfOwnerByIndex that are functions meant to be used off-chain, since they are O(n).

The main issue is not that,but a logic flaw. First, we see initialCdpIndex = sortedCdps.cdpCountOf(address(this));. Hence, initialCdpIndex is the amount of cdps the owner has. Later on the post check we see:

bytes32 cdpId = sortedCdps.cdpOfOwnerByIndex(address(this), initialCdpIndex);

Where initialCdpIndex is used to get the cdpId. Hence, the code assumes that the returned cdpId is the one that was opened previously. This assumption is incorrect, cdpOfOwnerByIndex starts at the tail of the linked list and checks if the current cdp is of the owner, if it is and the index match initialCdpIndex then it returns it, if not, increments index and keep searching.

Given the above, we know that bytes32 cdpId = sortedCdps.cdpOfOwnerByIndex(address(this), initialCdpIndex); will return the last cdpId of the owner in the linked list, which is not necessarily the cdp that was recently opened. Hence the following checks will be meaning less:

// Check for param details
ICdpManagerData.Cdp memory cdpInfo = cdpManager.Cdps(cdpId);
_doCheckValueType(checkParams.expectedDebt, cdpInfo.debt);
_doCheckValueType(checkParams.expectedCollateral, cdpInfo.coll);
require(
   cdpInfo.status == checkParams.expectedStatus,
   "!LeverageMacroReference: openCDP status check"
);

Proof of Concept

The following test can be added to test/CdpManagerTest.js:

it.only("sortedCdps.cdpOfOwnerByIndex(): Post Check is Incorrect", async () => {
    await contracts.collateral.deposit({from: A, value: dec(1000, 'ether')});
    await contracts.collateral.approve(borrowerOperations.address, mv._1Be18BN, {from: A});

    // @audit-info Current BTC / ETH price is 1.
    const newPrice = dec(1, 18);
    await priceFeed.setPrice(newPrice)

    // @audit-info Open a cdp
    await borrowerOperations.openCdp(dec(50, 18), A, A, dec(100, 'ether'), { from: A })

    let initialCdpIndex = await sortedCdps.cdpCountOf(A);

    // @audit-info Open a cdp with a smaller ICR than the first one.
    let secondCdpId = await borrowerOperations.openCdp(dec(70, 18), A, A, dec(100, 'ether'), { from: A })

    let assumedToBe_secondCdpId = await sortedCdps.cdpOfOwnerByIndex(A, toBN(initialCdpIndex.toString()));

    // @audit-info They are not equal
    expect(secondCdpId).to.not.be.equal(assumedToBe_secondCdpId);
  })

Tools Used

Manual review

Recommended Mitigation Steps

openCdp returns the cdpId. This value should be used for the post-check.

Assessed type

Other