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

Lines of code

https://github.com/code-423n4/2023-10-badger/blob/f2f2e2cf9965a1020661d179af46cb49e993cb7e/packages/contracts/contracts/SortedCdps.sol#L382-L385

Vulnerability details

Summary

It is possible for reInsert to revert for data.size == 2 and data.tail == data.head in SortedCdps.

Description

For a new list insert will assign data.head and data.tail to the same _id value:

SortedCdps.sol#L382-L385

        if (prevId == dummyId && nextId == dummyId) {
            // Insert as head and tail
            data.head = _id;
            data.tail = _id;

Calling remove right after initializing the list by calling insert will not result in the _id being removed, since only one of the two ids present in the list has been removed contains(_id) will still return true.

Additionally, it will be impossible to call reInsert for data.size == 2:

SortedCdps.sol#L498-L514

    function reInsert(
        bytes32 _id,
        uint256 _newNICR,
        bytes32 _prevId,
        bytes32 _nextId
    ) external override {
        _requireCallerIsBOorCdpM();
        // List must contain the node
        require(contains(_id), "SortedCdps: List does not contain the id");
        // NICR must be non-zero
        require(_newNICR > 0, "SortedCdps: NICR must be positive");


        // Remove node from the list
        _remove(_id);


        _insert(_id, _newNICR, _prevId, _nextId);
    }

This is because of the same reason, _remove will only remove one of the two ids and _insert will revert at !contains(id) check.

Proof of Concept

I wrote two certora rules to showcase this finding.

The first one shows that removing an _id does not mean !contains(_id) will be true. This rule should pass but doesn't in the current code. Here is the link for the certora traces.

/**
 * @title Deleting a node does not guarantee that it has been deleted because it can be added twice when initializing the list
 */
rule list_does_not_contain_id_after_remove(bytes32 _id) {
    env e;

    require getSize(e) == 2;

    // Execute the remove function
    remove(e, _id);

    // Assert that the node is no longer in the data.nodes mapping after removal
    assert !contains(e, _id);
}

The second rule is supposed to show that there is at least one non-reverting path in the reInsert function. It works with data.size == 1 but find a violation with data.size == 2, which suggests that data.size == 2 has a reverting path. In the certora traces for this rule, you will see that there is indeed a reverting path for data.tail == data.head.

rule reInsert_does_not_always_revert(bytes32 _id, uint256 _newNICR, bytes32 _prevId, bytes32 _nextId) {
    env e;

    // Assume the caller is BO or CdpM
    require e.msg.sender == borrowerOperationsAddress(e) || e.msg.sender == cdpManager(e);

    // Ensure the list contains the node with _id
    require contains(e, _id);

    // to prevent reverts
    require _newNICR > 0;
    require !isFull(e);
    require _id != dummyId(e);
    require _newNICR > 0;
    require getSize(e) < maxSize(e);
    require _id != getNext(e, _id);

    // data.size == 2
    require getSize(e) == 2;

    reInsert@withrevert(e, _id, _newNICR, _prevId, _nextId);

    assert !lastReverted;
}

Impact

It will force users to call remove twice in order to call reInsert and it may lead to users incorrectly thinking that their id has been removed when it's actually still present in the list. It might also lead to side effects if some parts of the codebase are assuming that calling remove imply !contains(_id) == true afterward.

Tool used

Manual Review

Recommended Mitigation Steps

Unfortunately, I don't have enough time left to come up with a good recommendation. But I would recommend adding additional logic to take into account the edge case of data.size == 2 with data.tail == data.head. Make sure to take great care when modifying the code as it could add vulnerabilities in other parts of the code.

Assessed type

Other