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

Leaving for sponsor/judge review

Might be OOS: https://gist.github.com/GalloDaSballo/a0f9766bf7bac391f49d2d167e947de0#incorrect-sorting-due-to-pending-debt-and-yield

bytes032 marked the issue as sufficient quality report

bytes032 marked the issue as primary issue

GalloDaSballo (sponsor) disputed

The finding is known and part of the known broken invariants + cantina report

We would be more lenient if any impact was demonstrated but afaict there's only an edge case for Redemptions not working when liquidations are more profitable which would lead me to dispute even in that case

We are interested in more impacts if those were found

We would want to ask the Warden for the POC as we have a concern for the issue being valid, but it seems like the finding is impossible in practice

here is a working POC to verify the finding https://gist.github.com/CodingNameKiki/4925e433ee47be70e6a4ef3eebe75b81?permalink_comment_id=4770452#gistcomment-4770452

OOS

The finding is known and part of the known broken invariants + cantina report

jhsagd76 marked the issue as unsatisfactory: Out of scope

I have noticed that a pull request https://github.com/ebtc-protocol/ebtc/pull/725 has been submitted to the main repo for this issue. Is this really OOS? @GalloDaSballo

The breaking of sorting is known but the mechanism through which this was achieved was not, so we believe the finding to be in scope

The impact of this finding is unclear

jhsagd76 removed the grade

jhsagd76 changed the severity to 2 (Med Risk)

jhsagd76 marked the issue as satisfactory

jhsagd76 marked the issue as selected for report

The attack scenario provided by the warden is very clear, but I don't see any actual profit or loss from it. Warden might argue that the CDP's position is incorrect after partial redemption, leading to damage upon the next redemption. However, in reality, it could have been fully redeemed initially, and the attacker wouldn't have gained any additional profits from it. But this clearly violates a critical invariant, especially when carefully crafted inputs are used as attack vectors. Therefore, I believe this falls into a med category.

Hey @jhsagd76, currently working alongside the badger team on some mitigations.

The breaking of sorting is known but the mechanism through which this was achieved was not, so we believe the finding to be in scope

With further research this report doesn't demonstrate any attack.

Issue 173

I believe this is not related to the empty nodes kept in the system while partially reInserting, it doesn't matter if you partially reInsert when there are empty nodes or not as the system is working correctly. The concern here is regarding the mathematical aspect of the ebtc system, it was proven in the broken invariants that there could be slightly difference in the NICR when redeeming happens and as a result a particular node could have a bigger NICR than his previous node in the sorted list.

There is no attack scenario here, whether if you remove the empty nodes or keep them or only partially redeeming the problem is still there and it's just how the system operates, there could be mathematical value difference between the NICR of the two nodes next to each other, but it is slim to nothing and doesn't lead to anything.

You can see that the problem still exist when there is no full redemption on redeeming and the partial redeemed node still has a bigger NICR than prev one in the sorted list.

// SPDX-License-Identifier: UNLICENSED
pragma solidity 0.8.17;

import "forge-std/Test.sol";
import {eBTCBaseInvariants} from "./BaseInvariants.sol";

contract checkSorting is eBTCBaseInvariants {

    address wallet = address(0xbad455);

    function setUp() public override {
        super.setUp();

        connectCoreContracts();
        connectLQTYContractsToCore();

    }

    function testSorting() public {

        uint256 grossColl = 11e18 + cdpManager.LIQUIDATOR_REWARD();

        uint256 price = priceFeedMock.fetchPrice();

        uint256 debtColl = _utils.calculateBorrowAmount(
            11e18,
            price,
            COLLATERAL_RATIO
        );

        // Cdp with the biggest NICR and the head of the sorted list
        bytes32 first = _openTestCDP(wallet, grossColl, debtColl - 10000);
        // Cdp with second best NICR in the sorted list
        bytes32 second = _openTestCDP(wallet, grossColl, debtColl - 7500);
        // Cdp with second lowest NICR in the sorted list
        bytes32 third = _openTestCDP(wallet, grossColl, debtColl);

        vm.startPrank(wallet);

        (bytes32 hint, uint256 partialNICR, , ) = hintHelpers.getRedemptionHints(debtColl / 2, priceFeedMock.fetchPrice(), 0);

        // Approve cdp manager to use ebtc tokens
        eBTCToken.approve(address(cdpManager), eBTCToken.balanceOf(wallet));
      
        cdpManager.redeemCollateral(debtColl / 2 , hint, bytes32(0), bytes32(0), partialNICR, 0, 1e18);

        uint256 _secondNICR = cdpManager.getCachedNominalICR(second);
        uint256 _thirdNICR = cdpManager.getCachedNominalICR(third);

        assert(_thirdNICR > _secondNICR);

        vm.stopPrank();

    }

}

Alright, according to the prove from sponsor:

There is no attack scenario here, whether if you remove the empty nodes or keep them or only partially redeeming the problem is still there and it's just how the system operates, there could be mathematical value difference between the NICR of the two nodes next to each other, but it is slim to nothing and doesn't lead to anything.

The warden only show the known broken invariant, but doesn't provide a valid and new attack vector. So this is OOS.

jhsagd76 marked the issue as unsatisfactory: Out of scope

First of all l apologise for the second ping, but l think l made a mistake here. If we add additional logs to the POC we can see that even tho the NICR of the partial redeem node changes and goes above the prev node in the sorted list, the system still finds its correct place when reInserting happens. So on second look l believe the issue in this report is valid and occurs only when fully redeeming node and partial redeeming from another. @jhsagd76

https://gist.github.com/CodingNameKiki/11103cc1921f18a3c600123f87ace4ab

Additional note and impact regarding this issue:

• First we know that there could be mathematical value difference between the NICR of the two nodes next to each other when a node is partial redeemed and reInserted back to the sorted list. If we look at the logs from the POC we can see what the difference between the two Cdp NICRs could look like. So if we apply the issue here - number 3 would be above number 2 even tho it has smaller NICR.

  2: 2154011847065201038074
  3: 2154011847065190493148

• This issue only applies for the first two nodes in the sorted list with ICR >= MCR, as the redeem functionality is designed to start with the first node with ICR >= MCR you can't actually redeem whatever node id you want and mess up whatever part of the sorted list you want. The fun fact here is that the next users which redeem can actually fix the incorrect sorting of the first two nodes, by fully redeeming the first redeemable node.

Given the small NICR mathematical difference between the two nodes and that this issue only applies for the first two nodes in the sorted list which have ICR >= MCR. l don't think its possible to have any rational impact here rather than the first two nodes having a small NICR difference between them.

Alright, I'll go back here, but waiting a final check:

The attack scenario provided by the warden is very clear, but I don't see any actual profit or loss from it. Warden might argue that the CDP's position is incorrect after partial redemption, leading to damage upon the next redemption. However, in reality, it could have been fully redeemed initially, and the attacker wouldn't have gained any additional profits from it. But this clearly violates a critical invariant, especially when carefully crafted inputs are used as attack vectors. Therefore, I believe this falls into a med category.

Alright, I'll go back here, but waiting a final check:

Will make a POC today to confirm the statement and let you know.

Hello again :) @jhsagd76

So on short explanation l understood that this issue:

• Have no impact that l am aware of.
• Messes up only the first redeemable node after the attack.
• The node ordering is back to normal when someone else redeems after the attack.

The attack scenario provided by the warden is very clear, but I don't see any actual profit or loss from it.

Agree with you on this one, at the same time an interesting question is why would anyone want to do this if there is no profit from it, no impact and the sorted order is back to normal on the next redeem.

https://gist.github.com/CodingNameKiki/b3f36aacc704c082df2b974b2db89c78

Thanks for the poc and verification from @CodingNameKiki . And the sponsor finally convinced me. The invariant was only temporarily broken, and whatever the attacker does during this intermediate stage will get back to the previous state. This impact is so minimal that it can be downgraded to a QA

jhsagd76 changed the severity to QA (Quality Assurance)

jhsagd76 marked the issue as grade-a

Hello @jhsagd76, @rayeaster, thank you for reviewing the issue.

I would like to respectfully question the severity of the problem for the following reasons:

• Initially, there doesn't seem to be an attacker involved in this issue, as a regular user seeking partial redemption could potentially disrupt the sorted cdps. The provided Proof of Concept (POC) demonstrates that the hints used by the sender are derived from the hintHelpers contract rather than being predetermined by an attacker.

• Additionally, the POC presented by @CodingNameKiki might be applicable only when the redemption occurs immediately after. What if other transactions take place before the fixed redemption? For instance, consider a scenario where the NICR of sortedCdps post-redemption disrupts the order, such as [8, 12, 5]. If a user intends to open a new CDP with NICR = 9, the provided hints could be before NICR = 8, resulting in the new sorted cdps as [9, 8, 12, 5]. In this case, there are now two incorrect positions in the sorted list instead of one. The more openCdp() transactions are initiated, the more incorrect positions could emerge, and the cost to rectify the order becomes higher.

Considering these factors, I believe the severity of this issue should be classified as medium.

Initially, there doesn't seem to be an attacker involved in this issue, as a regular user seeking partial redemption could potentially disrupt the sorted cdps. The provided Proof of Concept (POC) demonstrates that the hints used by the sender are derived from the hintHelpers contract rather than being predetermined by an attacker.

Do you mean providing wrong _firstRedemptionHint or wrong _partialRedemptionHintNICR, if that's the case the system will manually find the correct redeemable hint which is the first node with ICR >= MCR, on the other hand if you provide a wrong partial hint NICR the partial redeeming will be cancelled.

        if (_isValidFirstRedemptionHint(_firstRedemptionHint, totals.price)) {
            currentBorrower = sortedCdps.getOwnerAddress(_firstRedemptionHint);
        } else {
            _cId = sortedCdps.getLast();
            currentBorrower = sortedCdps.getOwnerAddress(_cId);
            // Find the first cdp with ICR >= MCR
            while (currentBorrower != address(0) && getSyncedICR(_cId, totals.price) < MCR) {
                _cId = sortedCdps.getPrev(_cId);
                currentBorrower = sortedCdps.getOwnerAddress(_cId);
            }
        }

            if (
                newNICR != _redeemColFromCdp.partialRedemptionHintNICR ||
                collateral.getPooledEthByShares(newColl) < MIN_NET_STETH_BALANCE
            ) {
                singleRedemption.cancelledPartial = true;
                return singleRedemption;
            }

In case you are talking about the upper and lower hints used in the POC, l tried every other possible hints and the system is working correctly. So this scenario is only possible if someone provided the exact hints and only when the system fully redeems a node and partially redeems from another.

We would be more lenient if any impact was demonstrated but afaict there's only an edge case for Redemptions not working when liquidations are more profitable which would lead me to dispute even in that case We are interested in more impacts if those were found

As mentioned we are already aware and it's known that wrong sorting can happen from the broken invariants, the question should be what impact does this issue lead to? Would suggest for a further research on the impact here and coded POC.

@jhsagd76 @rayeaster @GalloDaSballo I would like to explain the reasons why I believe this issue should be considered at least a medium severity. I also believe that these explanations can address the concerns raised from @codingnamekiki and others to downgrade this issue.

1. I believe the provided attack vector is very clear, indicating that an attacker can disrupt the sorting order of CDPs through partial redemption. The attacker just needs to call the function redeemCollateral with malicious values for _upperPartialRedemptionHint and _lowerPartialRedemptionHint to place the partially redeemed CDP in the wrong position. The scenario was described very clearly in the report, and there is another proof of concept (POC) mentioned in the comment by @rayeaster. Additionally, I believe it's not a known issue because the known scenario that also breaks the order is from redistribution of debt and yield, which is different. This scenario allows an external attacker to interact with and manipulate the broken invariants. It has a significant impact, which will be described below.

2. An attacker can increase the NICR of a partially redeemed CDP to a very large value and place it in the wrong position. To achieve this, the attacker can calculate the redemption amount to leave the remaining debt of the partially redeemed CDP at 1. For example, if a CDP has $15e18 in collateral and $10e18 in debt, the attacker can calculate a partial redemption with a debt of $10e18 - 1, resulting in a remaining debt of 1 and remaining collateral of 5e18 (assuming remaining collateral can bypass MIN_NET_STETH_BALANCE). This manipulation causes the new NICR to become very large.
 Consider the scenario in the report. After redemption, the sortedCdps list will be: $x_1, \;..., \; x_{i-3}, \; x_{i-2}, \; x_{i-1}, \; ..., \; x_i', \; x_j, \; ..., \; x_{n}$ $x_{i}'$ may have a very large NICR (up to infinity), and it is the first node with ICR >= MCR because the ICR of $x_{j}$ is below MCR. Therefore, any new CDP that is opened with _upperHint as dummy or invalid will be placed after the CDP $x_{i}'$. This is because the _findInsertPosition function will find the position in ascending order if the _prevId parameter is dummy or invalid.
You can read this code snippet to understand this flow. For example, when the NICR of $x_{i}'$ is very large (considered infinity), the NICR list of sortedCdps is like: 300%, 250%, ..., 160%, 150%, inf, 125%, 124%, ... When opening a CDP with a 200% NICR and _upperHint as dummy or invalid, the list will become: 300%, 250%, ..., 160%, 150%, inf, 200%, 125%, 124%, ... Therefore, the new CDP (200% NICR) will be inserted to a wrong position and become the first node (most right) with ICR > MCR and will be redeemed with priority, even though the NICR of that CDP is still good. Here is a POC of this scenario: https://gist.github.com/huuducsc/c6885a06058d56cd4f6669f3b11c8f7d

3. Due to the above scenario, I disagree with the statement made by @jhsagd76: "The invariant was only temporarily broken, and whatever the attacker does during this intermediate stage will get back to the previous state." The attacker can open numerous new Cdps into incorrect positions using dummy upperHint and invalid lowerHint (details are described in the scenario and PoC of section 2), disrupting the order of protocols. Moreover, the attacker can front-run any opening CDP transaction by users to break the order, make it becomes the first position to be redeemed. Here are the details of the impacts that cause significant damage to protocol:

• The attacker can break the order of sortedCdps and disrupt it by opening many new CDPs with _upperHint is dummy, placing them in incorrect positions (as described above). Therefore, sortedCdps will have many incorrect positions that are not easy to resolve. This disruption can mess up the protocol's data and may result in incorrect returns from the HintHelpers contract.
• After the mentioned manipulation, any new CDP will be at risk of being redeemed with priority, even though its NICR is still good. This can happen if the _upperHint passed to the openCdp function of users is dummy or invalid, which can occur normally due to changes in on-chain data like front-running or incorrect returns from the HintHelper contract. It creates an unfair situation for protocol users, as they may be compelled to redeem their assets (acquiring debt assets and losing collateral assets) even when they have a CDP with a high NICR.

In conclusion, this issue has a significant impact that can disrupt the ordered state of the protocol and put users at risk of having their assets forcibly redeemed. However, the severity may increase if attackers identify other attack vectors (which I haven't found until now) to manipulate the state and exploit vulnerabilities since attackers are able to break order invariants externally.

^ Thanks for the reply, will further make a POC to double confirm everything.

Check the below POC which confirms the above statements.

https://gist.github.com/CodingNameKiki/0f4bc68802cfcbfe255759554b735b38

Thank warden for providing additional information on the impact. This has made the report ultimately comprehensive and clear.

I have discussed the final rating based on the following facts, rules, and input from two senior judges. We ultimately elevate this issue to MED. Record I.:

As the original submission doesn't contain a PoC of the final impact, I think Medium is more appropriate.

Record II.:

1. for the impact I.

This disruption can mess up the protocol's data and may result in incorrect returns from the HintHelpers contract.

it meets the criteria of MED. Although it is not dos, it affected the availability of the protocol for normal users.

but the function of the protocol or its availability could be impacted

2. For impact II.

It creates an unfair situation for protocol users, as they may be compelled to redeem their assets (acquiring debt assets and losing collateral assets) even when they have a CDP with a high NICR.

Its based on impact I, but I think it can be a HIGH according to the criteria:

Assets can be stolen/lost/ compromised directly or indirectly if there is a valid attack path that does not have hand-wavy hypotheticals

Because attackers are able to break order invariants externally, we can believe the attack path is explicit (include front run). And the redemption from high NICR cdp won't result in a direct loss of assets, but it is clearly a form of compromise.

This previously downgraded issue has been upgraded by jhsagd76

jhsagd76 marked the issue as satisfactory

jhsagd76 marked the issue as selected for report

@jhsagd76 Thank you very much for your review. I would like to say that this issue deserves a high severity because users' assets can be compromised when order of Cdps is broken. It aligns with the criteria of a high-severity issue outlined in Code4rena's docs.

Assets can be stolen/lost/ compromised directly or indirectly if there is a valid attack path that does not have hand-wavy hypotheticals

The reason I didn't provide detailed descriptions of the impact in the initial report was my assumption that anyone could create several high impacts by exploiting the scenario of an attacker breaking the order externally. However, there were arguments against this view, necessitating a detailed explanation of the impact. And it is a fact that I provided a detailed explanations of this issue along with a PoC. Therefore, I believe this issue should be considered a valid high-severity issue.

Furthermore, I believe it doesn't make sense to downgrade this issue based on the rationale that "the original submission doesn't contain a PoC of the final impact." While the impact in the report may lack details and be unclear to some, I subsequently provided detailed explanations and a PoC to substantiate its high severity. The information I supplied doesn't alter the severity of this issue; rather, it serves to validate the impact and address concerns/suspects raised by others. Therefore, I believe that the lack of details in the report shouldn't be used as a basis for downgrading the issue, based on this statement from C4's docs:

At the judge's discretion, a highly-standard issue can be accepted with less detail provided.

In fact, the Record II. is my assessment, while the Record I. consists of recommendations from the senior judges. I find their suggestions reasonable, and they also provided me with precedents. However, I believe that discussing these precedents here may not be appropriate. And the rules you mentioned is for the case "Duplicate Report PoC Thoroughness".

still consider the recommendation from the senior judges. And I will submit a proposal to the org after the contest to formalize the rule.

Thank you for your understanding and perfect work.

@jhsagd76 Thank you for the reply. I understand your situation, but I believe this issue shouldn't be downgraded since it was initially raised with high severity, and the PoC merely clarified its impact. Additionally, I don't see any reasonable grounds in the other judge's suggestions to downgrade this issue. I believe there were many valid issues on C4 that lacked a detailed PoC or explanation but were still accepted as high/medium severity issues because the judges could easily understand them. In this case, this issue faced arguments and misunderstandings, necessitating a detailed explanation of the impact. This is why the Post-judging period is necessary, as it assists the warden in proving and clarifying statements from the report. My additional PoC didn't increase the impact of my initial report; rather, it further clarified it and should not lead to a downgrade in the severity of the issue. Here are some examples from C4's judging for several issues that lacked a detailed PoC:

• https://github.com/code-423n4/2023-10-wildcat-findings/issues/431 While this issue lacked detailed description and didn't provide a PoC for verification, it was still accepted as High severity because the judge already understood its potential impact, which would compromise two core functionalities of the protocol after deployment
• https://github.com/code-423n4/2023-08-dopex-findings/issues/2228 https://github.com/code-423n4/2023-11-betafinance-findings/issues/37 https://github.com/code-423n4/2023-03-polynomial-findings/issues/263 These are QA issues that lacked everything, including detailed descriptions, PoC, and impact. However, they were upgraded to high and medium severity, and 2 of them became solo findings. Therefore, I believe it doesn't make sense to downgrade a high issue just because it lacks details of impact.
• https://github.com/code-423n4/2023-03-polynomial-findings/issues/75 
https://github.com/code-423n4/2022-10-holograph-findings/issues/445 
These are the issues that were accepted after the post-judging period because the warden provided more explanations and details of the PoC. They still maintained their severity.

bytes032 marked the issue as sufficient quality report

L5

jhsagd76 marked the issue as grade-a