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

1. Use braces around operators with uncertain precedence In RolesAuthority::canCall we see the following code

File: package/contracts/contracts/Dependencies/RolesAuthority.sol
function canCall(
        address user,
        address target,
        bytes4 functionSig
    ) public view virtual override returns (bool) {
return bytes32(0) != getUserRoles[user] & getRolesWithCapability[target][functionSig];

In Solidity the & operator will be executed before != but this might not always be clear and might be different in other languages. I suggest adding braces around getUserRoles[user] & getRolesWithCapability[target][functionSig] to clarify operator precedence.

2. More check for save storage In the RolesAuthority::setRoleCapability method, a require condition should be added at the beginning to ensure that the functionSig is not invoked for the CapabilityFlag.Burned and CapabilityFlag.Public cases:

File: package/contracts/contracts/Dependencies/RolesAuthority.sol
function setRoleCapability(
        uint8 role,
        address target,
        bytes4 functionSig,
        bool enabled
    ) public virtual requiresAuth {
require(capabilityFlag[target][functionSig] == CapabilityFlag.None,"xxx");

This condition serves to protect the owner from setting roles as burned or public, thus preventing unnecessary storage wastage.

3. transferOwnership should be two step process

File: package/contracts/contracts/Dependencies/Auth.sol
function transferOwnership(address newOwner) public virtual requiresAuth {
        owner = newOwner;

        emit OwnershipTransferred(msg.sender, newOwner);
    }

The function transferOwnership() transfer ownership to a new address. In case a wrong address is supplied ownership is inaccessible. Consider implementing a two step ownership transfer.

4. Strengthening Checks in the _initializeAuthority Method for Enhanced Reliability

File: package/contracts/contracts/Dependencies/AuthNoOwner.sol
function _initializeAuthority(address newAuthority) internal {
        require(address(_authority) == address(0), "Auth: authority is non-zero");
        require(!_authorityInitialized, "Auth: authority already initialized");

        _authority = Authority(newAuthority);
        _authorityInitialized = true;

        emit AuthorityUpdated(address(this), Authority(newAuthority));
    }

In order to ensure system integrity, it is imperative to diligently verify that newAuthority is a contract and has the canCall method properly implemented. The omission of this critical check may culminate in a revert scenario upon calling setAuthority, consequently triggering a system-wide failure.

5. Strengthening Checks in the setAuthority Method for Enhanced Reliability

File: package/contracts/contracts/Dependencies/AuthNoOwner.sol
function setAuthority(address newAuthority) public virtual {
        // We check if the caller is the owner first because we want to ensure they can
        // always swap out the authority even if it's reverting or using up a lot of gas.
        require(_authority.canCall(msg.sender, address(this), msg.sig));

        _authority = Authority(newAuthority);

        // Once authority is set once via any means, ensure it is initialized
        if (!_authorityInitialized) {
            _authorityInitialized = true;
        }
        //change to
        require(_authorityInitialized,"xx");
        emit AuthorityUpdated(msg.sender, Authority(newAuthority));
    }

When using require(_authorityInitialized, "xx") instead, it ensures that the setAuthority method can only be called after invoking _initializeAuthority, adding a necessary condition for proper sequence and functionality.

6. Enhancing Reliability: Making LIQUIDATOR_REWARD Mutable

File: package/contracts/contracts/Dependencies/EbtcBase.sol
uint256 public constant LIQUIDATOR_REWARD = 2e17;
change to
uint256 internal LIQUIDATOR_REWARD = 2e17;

With the fluctuation in the price of ETH, adjusting the reward value might be necessary to effectively incentivize liquidators for liquidation.

7. Addressing Potential Block Number Overflow Issues in the Future

File: package/contracts/contracts/SortedCdps.sol
function toCdpId(
        address owner,
        uint256 blockHeight,
        uint256 nonce
    ) public pure returns (bytes32) {
        bytes32 serialized;

        serialized |= bytes32(nonce);
        serialized |= bytes32(blockHeight) << BLOCK_SHIFT; // to accommendate more than 4.2 billion blocks
        serialized |= bytes32(uint256(uint160(owner))) << ADDRESS_SHIFT;

        return serialized;
    }

In the future, if Ethereum were to change the block generation time, there is a potential risk of overflow beyond the maximum value of uint32 for blockHeight. This could lead to inaccuracies in tracking the owner's address. To address this potential flaw, it is advisable to implement additional checks to ensure proper handling of blockHeight overflow scenarios.

8. Potential Out-of-Gas Issues of cdpOfOwnerByIndex Function File: package/contracts/contracts/SortedCdps.sol function cdpOfOwnerByIndex( address owner, uint256 index ) external view override returns (bytes32) { (bytes32 _cdpId, ) = _cdpOfOwnerByIndex(owner, index, dummyId, 0); return _cdpId; }

This function, which iterates over all nodes, poses a risk of gas exhaustion, particularly when dealing with a substantial node count, such as 5000. The possibility of a revert due to out-of-gas conditions needs careful consideration and potential mitigation strategies.
The cdpCountOf and getCdpsOf functions share a similar concern. A meticulous review of all dependencies on these functions is imperative to ensure seamless functionality, particularly when dealing with a substantial number of nodes.

9. Enhancing Safety: Adding Additional Checks to batchRemove Function
File: package/contracts/contracts/SortedCdps.sol
function batchRemove(bytes32[] memory _ids) 

batchRemove makes a strong trust assumption that the specified nodes are sorted in the same order as in the input array. It is potentially risky, as inadvertent actions could lead to the deletion of nodes that shouldn't be removed. To mitigate this risk, please consider adding a check in the code to ensure that the input array is sorted.