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

bytes032 marked the issue as insufficient quality report

bytes032 marked the issue as remove high or low quality report

bytes032 marked the issue as sufficient quality report

bytes032 marked the issue as duplicate of #63

We are still looking into this finding which:

• Seems to have a non relevant impact (sorting being replaced)
• Seems to imply a mistake in the way fees are computed

The impact is incorrect

The way Stake changes incorrectly causes fee split is valid

We're investigating impact and consequences

Not a dup of 63 this seems to be a solo finding

jhsagd76 marked the issue as not a duplicate

I mark this as satisfactory but will wait for the final investigate result from sponsor.

jhsagd76 marked the issue as satisfactory

@GalloDaSballo

The conclusion is wrong

But the finding showed that the feeSplit math is incorrect, which is a severe finding

jhsagd76 marked the issue as selected for report

It is more like a precision issue using Solidity (sth like $\frac{(x -z) + (z - y)}{c} \neq \frac{x - z}{c} + \frac{z - y}{c}$) instead of a fundamental design problem.

The following statement is worth more thinking: we can intuitively understand that new CDPs will pay more fees than the old ones. Therefore, new cpds NICR (Nominal Individual Collateral Ratio = shares/debt) will decrease at a higher rate than old ones

Yes, higher stake leads to more fees, but it is NOT equal to "decrease at a higher rate", actually the relative ratio of NICR between two CDPs always keep the same "theoretically" by the stake mechanism:

• Suppose totalStakeSnapshot is $S_{n}$ which is not changed by split fee claim
• At time T0, totalCollateralSnapshot is $C_{n0}$
• At time T1, a $CDP_{1}$ is created with initial collateral share c and debt d thus its stake is $s_{1}=\frac{c * S_{n}}{C_{n0}}$
• At time T2, a split fee claim happens and totalCollateralSnapshot is changed to $C_{n1}$, note that $C_{n1} < C_{n0}$ and $C_{n0} - C_{n1} = S_{n} * \Delta{P_{1}}$ where $\Delta{P_{1}}$ is the delta change of fee per stake unit
• At time T3, another $CDP_{2}$ is created with the same collateral share c and debt d but now its stake is $s_{2}=\frac{C * S_n}{C_{n1}} > s_{1}$
• Now NICR of $CDP_{1}$ is $\frac{c - s_{1} * \Delta{P_{1}}}{d}$ and NICR of $CDP_{2}$ is $\frac{c}{d} > NICR_{1}$, their NICR ratio $r_{1}$ is $\frac{c - s_{1} * \Delta{P_{1}}}{c}$
• At time T4 (maybe after a long time), a split fee claim happens again and $\Delta{P_{2}}$ is the delta change of fee per stake unit for this time
• Now NICR of $CDP_{1}$ is $\frac{c - s_{1} * \Delta{P_{1}} - s_{1} * \Delta{P_{2}}}{d}$ and NICR of $CDP_{2}$ is $\frac{c - s_{2} * \Delta{P_{2}}}{d}$, so their NICR ratio $r_{2}$ is now $\frac{c - s_{1} * \Delta{P_{1}} - s_{1} * \Delta{P_{2}}}{c - s_{2} * \Delta{P_{2}}}$
• Let us prove that $r_{2}=r_{1}$ in theory

If $\frac{c - s_{1} * \Delta{P_{1}} - s_{1} * \Delta{P_{2}}}{c - s_{2} * \Delta{P_{2}}} = \frac{c - s_{1} * \Delta{P_{1}}}{c} \Rightarrow $

$(c - s_{1} * \Delta{P_{1}}) * (c - s_{2} * \Delta{P_{2}}) = c * (c - s_{1} * \Delta{P_{1}} - s_{1} * \Delta{P_{2}}) \Rightarrow $

$c^2 - c * s_{2} * \Delta{P_{2}} - c * s_{1} * \Delta{P_{1}} + s_{1} * s_{2} * \Delta{P_{1}} * \Delta{P_{2}} = c^2 - c * s_{1} * \Delta{P_{1}} - c * s_{1} * \Delta{P_{2}} \Rightarrow $

$s_{1} * s_{2} * \Delta{P_{1}} = c * (s_{2} - s_{1}) \Rightarrow \frac{s_{1}}{c} * \Delta{P_{1}} = 1 - \frac{s_{1}}{s_{2}} \Rightarrow$

$\frac{S_{n}}{C_{n0}} * \Delta{P_{1}} = 1 - \frac{C_{n1}}{C_{n0}} \Rightarrow S_{n} * \Delta{P_{1}} = C_{n0} - C_{n1} $

Proved

If we could manually syncAccounting for the first CDP along the poc test path (i.e., always sync its collateral for every index increase in the loop) or simply set the loop number to 1000 instead of 100, the list order will not break at the end of the poc test.

And the break require some delicate conditions like significant increase of the Lido stETH index, e.g., 40% increase means about 10 years at the current staking reward apr

I suggest to mark it as "acknowledged"

Tks for the careful and clear math prove from @rayeaster , it's very helpful to show the underlying mechanism of the issue based. It's amazing. And I want to add a comment for s2 in T3. There is no need to worry about the impact of c and s1 on Sn and Cn1 in T1, as they grow proportionally. The mathematical calculations in T3 are completely correct, and you can further prove this. I have actually done it myself, but I'm not very good at writing mathematical formulas using Markdown. So, I'm only providing this conclusion to prevent any doubts about this.

And I add one line at the end of logNICR function in the original poc:

console.log(cdpManager.getSyncedNominalICR(firstCdpId) * 1e18 / cdpManager.getSyncedNominalICR(lastCdpId));

The console log can clearly show why the sponsor say it's precision issue:

Logs:
before
  ---------------------------------- 1st cdp
  getCdpStake         :  9800399201596806387
  getCdpCollShares    :  9800399201596806387
  getSyncedNominalICR :  1791162047648499053200
  ---------------------------------- last cdp
  getCdpStake         :  10760678217311938700
  getCdpCollShares    :  9833333333333333333
  getSyncedNominalICR :  1791162047648499053418
  ---
  -218
  999999999999999999
  ----------------------------------
 after
  ---------------------------------- current cdp
  getCdpStake         :  7660143815713583482
  getCdpCollShares    :  6125000000000000000
  getSyncedNominalICR :  1225000000000000000000
  ----------------------------------
  ---------------------------------- 1st cdp
  getCdpStake         :  9800399201596806387
  getCdpCollShares    :  9800399201596806387
  getSyncedNominalICR :  1567266791692436672600
  ---------------------------------- last cdp
  getCdpStake         :  10760678217311938700
  getCdpCollShares    :  9833333333333333333
  getSyncedNominalICR :  1567266791692436672219
  ---
  381
  1000000000000000000
  ----------------------------------

In fact, this variation is not linear. It requires the growth of the index to occur at an extremely precise value in order to generate this error.

And I also want to provide a poc test for the amazing math prove from @rayeaster , tks him again.

      function test_H2prove() public {
        vm.pauseGasMetering();
      
        address cdp1_user;
        address cdp2_user;
        bytes32 cdp1_id;
        bytes32 cdp2_id;       

        // stake someting to init
        {
            address _nobody = prepareUser();
            vm.prank(_nobody);
            borrowerOperations.openCdp(1.337 ether, "hint", "hint", 31.415 ether);
            _applyIndexChange(1000000000000000); // +0.1% index
        }
        
        // T0
        {
            cdpManager.syncGlobalAccountingAndGracePeriod();
            uint Sn = cdpManager.totalStakesSnapshot();
            uint Cn0 = cdpManager.totalCollateralSnapshot();
            console.log(Sn, Cn0);    
        }
        
        // const
        uint c = 10 ether;
        uint d = 0.5 ether;

        // T1
        cdp1_user = prepareUser();
        vm.prank(cdp1_user);
        cdp1_id = borrowerOperations.openCdp(d, "hint", "hint", c);
        // uint s1 = cdpManager.getCdpCollShares(cdp1_id);
        // console.log(s1);

        // T2
        {
            int delta_p1 = 2000000000000000; // +0.2% index
            _applyIndexChange(delta_p1);
            cdpManager.syncGlobalAccountingAndGracePeriod();
            // vm.prank(cdp1_user);
            // cdpManager.syncAccounting(cdp1_id);
        }

        // T3
        cdp2_user = prepareUser();
        vm.prank(cdp2_user);
        // c = 17 ether;
        // d = 1.1 ether;
        cdp2_id = borrowerOperations.openCdp(d, "hint", "hint", c);
        // uint s2 = cdpManager.getCdpCollShares(cdp2_id);
        // console.log(s2);

        // after T3, we should calc NICR rate
        uint wad = 1e18;
        {
            uint cdp1_NICR_T3 = cdpManager.getSyncedNominalICR(cdp1_id);
            uint cdp2_NICR_T3 = cdpManager.getSyncedNominalICR(cdp2_id);
            uint rate_T3 = cdp1_NICR_T3 * wad / cdp2_NICR_T3;
            console.log(rate_T3);
        }

        // T4
        {
            int delta_p2 = 400000000000000000; // +40% index
            _applyIndexChange(delta_p2);
            cdpManager.syncGlobalAccountingAndGracePeriod();
            // dump rate after T4
            uint cdp1_NICR_T4 = cdpManager.getSyncedNominalICR(cdp1_id);
            uint cdp2_NICR_T4 = cdpManager.getSyncedNominalICR(cdp2_id);
            uint rate_T4 = cdp1_NICR_T4 * wad / cdp2_NICR_T4;
            console.log(rate_T4);
            // console.log(cdpManager.getCdpCollShares(cdp1_id), cdpManager.getCdpCollShares(cdp2_id));
        }
      }

So, finally, I will mark this as QA, but waiting a double check from sponsors @GalloDaSballo @rayeaster

@jhsagd76 Thanks for the great proof test!

It helps to spark an interesting idea. Do you think it would help to use sth like cdpManager.getSyncedNominalICR(firstCdpId) * 1e18 / cdpManager.getSyncedNominalICR(lastCdpId) to compare the NICR as an additional check?

I mean we could say $NICR_{1}$ is larger than $NICR_{2}$ only if the following two conditions are satisfied at the same time:

• $NICR_{1} > NICR_{2}$
• $\frac{NICR_{1} * 1e18}{NICR_{2}} > 1e18$

Aha,I think this check may be idealistic. The poc we are currently discussing only involve a single rounding situation, but the actual scenario may be much more complex. Each syncAccounting after a rebase introduces rounding, but I believe this will actually alleviate the impact of the issue.

If we add bad debt redistribution into the play, the ratio of NICR between CDPs would change but will NOT go to the extent that reverse the ordering, theoretically:

• Following above math derivation setup, suppose right after $CDP_{2}$ is created at time T3, there is a liquidation with some bad debt to be redistributed and introduce a $\Delta{d_{1}}$ increase for systemDebtRedistributionIndex
• Now the NICR of $CDP_{1}$ is $\frac{c - s_{1} * \Delta{P_{1}}}{d + s_{1} * \Delta{d_{1}}}$, and NICR of $CDP_{2}$ is $\frac{c}{d + s_{2} * \Delta{d_{1}}}$, let us prove that their NICR ratio still keep the ordering:

$ratio_{NICR} = \frac{c - s_{1} * \Delta{P_{1}}}{c} * \frac{d + s_{2} * \Delta{d_{1}}}{d + s_{1} * \Delta{d_{1}}} = \frac{s_{1}}{s_{2}} * \frac{d + s_{2} * \Delta{d_{1}}}{d + s_{1} * \Delta{d_{1}}} = \frac{s_{1} * s_{2} * \Delta{d_{1}} + s_{1} * d}{s_{1} * s_{2} * \Delta{d_{1}} + s_{2} * d} \lt 1$

Proved

So the whole story would be:

• Split fee distribution would keep the NICR ratio the same
• Bad debt redistribution would change the NICR ratio a bit but still remain the ordering

The impact based on bad debt redistribution is valid, but it can't break the cdp order. Considering the fixes already introduced in Liquity, I suggest considering the impact of this issue in long-running systems. Therefore, I mark this issue as med.

jhsagd76 changed the severity to 2 (Med Risk)

l couldn't hold myself to not make this given the comments here.

bytes032 marked the issue as insufficient quality report

GalloDaSballo (sponsor) disputed

Need actual math

Also redemption fees are 1% due to oracle drift (check cheatsheet)

Interesting, but I cannot classify these as med without sufficient evidence.

jhsagd76 marked the issue as unsatisfactory: Insufficient proof

Elevate this issue to an valid QA and recommend the sponsor to consider this suggestion. Although I don't consider it a vulnerability or a specific functional error, I believe it would be beneficial for the protocal stability.

jhsagd76 removed the grade

jhsagd76 changed the severity to QA (Quality Assurance)

jhsagd76 marked the issue as grade-a

Elevate this issue to an valid QA and recommend the sponsor to consider this suggestion. Although I don't consider it a vulnerability or a specific functional error, I believe it would be beneficial for the protocal stability.

Further explain this suggestion. Common over-collateralized peg assets typically incur fees for open position / borrow / mint, such as LUSD and YUSD, usually around 0.5%. However, eBTC does not have such fees because the protocol charges fees from the stETH rebase. However, I have noticed that while this mechanism enhances capital efficiency, it also introduces some issues difficult to mitigate. For example

1. #325 rebase fee can be skipped in one tx per day.
2. #308 inflating the total debt can be used to decrease redemption fee
3. #226 open position can be used to dos redemptions

If we consider this fee as a defense rather than a profit, we can set the fee at a low level to maintain capital efficiency. For example, according to the current stETH rate, 3.6% - 4%, div by 365, a fee about 0.01% sounds good, IMO.

kindly ping the sponors to ensure they won't miss this @GalloDaSballo @CodingNameKiki