Inaccurate Display of Protocol Fee Share in `protocolFeeShare()`

[alexzoid-eth]

Low, https://cantina.xyz/code/41306bb9-2bb8-4da6-95c3-66b85e11639f/findings/452

Description

The GovernanceModule.protocolFeeShare() function incorrectly displays the protocol fee share as it does not consider the 50% limitation set by MAX_PROTOCOL_FEE_SHARE.

Proof of Concept

This Certora property is violated https://prover.certora.com/output/52567/6cd2626b55f9424b9b3da67b67628477/?anonymousKey=7245484ad3d408c53ad05615320c2c728e92bd78

// L1 | `protocolFeeShare()` displays incorrect value as it doesn't consider 50% limitation
rule protocolFeeShareLimited(env e) {
    assert(to_mathint(protocolFeeShare(e)) <= MAX_PROTOCOL_FEE_SHARE());
}

After the recommended fix, it is not violated https://prover.certora.com/output/52567/18817af4566947c688de0fd825257595/?anonymousKey=a9b4887daff68d3e16139921a5644f1e1a4e911c

Recommendation

diff --git a/src/EVault/modules/Governance.sol b/src/EVault/modules/Governance.sol
index 0b5ade0..720f501 100644
--- a/src/EVault/modules/Governance.sol
+++ b/src/EVault/modules/Governance.sol
@@ -118,7 +118,7 @@ abstract contract GovernanceModule is IGovernance, BalanceUtils, BorrowUtils, LT
     /// @inheritdoc IGovernance
     function protocolFeeShare() public view virtual reentrantOK returns (uint256) {
         (, uint256 protocolShare) = protocolConfig.protocolFeeConfig(address(this));
-        return protocolShare;
+        return protocolShare > MAX_PROTOCOL_FEE_SHARE ? MAX_PROTOCOL_FEE_SHARE : protocolShare;
     }

     /// @inheritdoc IGovernance

[teryanarmen]

nice one. valid.

[teryanarmen]

Did you try it with an invariant?

[alexzoid-eth]

Did you try it with an invariant?

No, but I found how the parametric rule could prove this issue.

[alexzoid-eth]

@teryanarmen

This Certora property is violated https://prover.certora.com/output/52567/0040a19d8f914ce383e11e56084a109a/?anonymousKey=454e6bc21111c55d3c71e78ba95845a67f310335

// L1-EX | Ensure that protocol fee receiver gets an amount of shares equal to what `protocolFeeShare()` getter returns
rule protocolFeeShareLimitedEx(env e, method f, calldataarg args) {

    // Retrieve the addresses for the governor and protocol fee receivers
    address governor = feeReceiver();
    address protocol = ghostProtocolFeeReceiver[currentContract];

    // Safe assumption: ensure that the governor fee receiver is set and is not the same as the protocol fee receiver
    require(governor != 0);
    require(governor != protocol);

    // Get the expected protocol fee shares based on the `protocolFeeShare()` getter
    mathint getterFeeShare = to_mathint(protocolFeeShare(e));
    mathint governorExpectShares = (ghostAccumulatedFees * (CONFIG_SCALE() - getterFeeShare)) / CONFIG_SCALE();
    mathint protocolExpectShares = ghostAccumulatedFees - governorExpectShares;

    // Capture the protocol fee receiver's balance before the function call
    mathint protocolBalanceBefore = ghostUsersDataBalance[protocol];

    // Execute any external function
    f(e, args);

    // Capture the protocol fee receiver's balance after the function call
    mathint protocolBalanceAfter = ghostUsersDataBalance[protocol];

    // Ensure that any change in the protocol fee receiver's balance is as expected
    // The increase in protocol fee receiver shares MUST equal the expectations based on the `protocolFeeShare()` getter
    assert(protocolBalanceAfter != protocolBalanceBefore 
        => protocolBalanceAfter - protocolBalanceBefore == protocolExpectShares
    );
}

After the recommended fix, it is not violated https://prover.certora.com/output/52567/667801eac9954702b8ec0de8e6913178/?anonymousKey=6ef372876c4208f300cb8baaced63beea93628aa

[alexzoid-eth]

@teryanarmen I have refined the previous comment to enhance the soundness of the rule. The updated rule is now also duplicated in the Cantina site.

[teryanarmen]

Can you please add hoytech and erik1o6 from euler as collaborators?

[teryanarmen]

If there's a limit on how many collaborators you can add, you can make this public, since the contest is over.

[alexzoid-eth]

If there's a limit on how many collaborators you can add, you can make this public, since the contest is over.

Sure, done.