alexzoid-eth / uniswap-v4-periphery-cantina-fv

Uniswap v4 x Certora Formal Verification Competition (#2 place)
https://cantina.xyz/competitions/e2cf6906-ec8b-4c78-a585-74ac90615659
GNU General Public License v2.0
0 stars 0 forks source link

Incorrect Payer When Settling Contract's Balance #1

Open alexzoid-eth opened 1 month ago

alexzoid-eth commented 1 month ago

Description

In the PositionManager contract, when settling with the CONTRACT_BALANCE flag, the action should always use the contract's entire balance of the specified currency. This flag is defined in ActionConstants as:

/// @notice used to signal that an action should use the contract's entire balance of a currency

However, the current implementation allows the payer to be set to the user even when the CONTRACT_BALANCE flag is used. This could lead to a situation where the user is charged for the entire contract balance instead of the contract itself.

Proof of Concept

A Certora rule is violated https://prover.certora.com/output/52567/95983b906f214449807a0fe6283ed52f/?anonymousKey=d411d086cecc1adb8efb0af12b27385b85c98ffa

import "./PositionManagerValidState.spec";

/// @notice used to signal that an action should use the contract's entire balance of a currency
/// This value is equivalent to 1<<255, i.e. a singular 1 in the most significant bit.
definition CONTRACT_BALANCE() returns uint256 = 0x8000000000000000000000000000000000000000000000000000000000000000;

// Verifies that when settling with the CONTRACT_BALANCE flag, the action uses the contract's entire balance
rule settleUsesFullContractBalance(env e, bytes params) {

    // Assume PositionManager is in a valid state before the action
    requireValidStatePositionManagerEnv(e);

    // Decode the input parameters for the settle action
    PoolManager.Currency currency;
    uint256 amount; 
    bool payerIsUser;
    currency, amount, payerIsUser = _HelperCVL.decodeSettleParams(params);

    // Record the locker's balance before the action
    mathint lockerBalanceBefore = balanceOfCVL(e, currency, ghostLocker);

    // Execute the settle action
    handleActionSettle(e, params);

    // Record the locker's balance after the action
    mathint lockerBalanceAfter = balanceOfCVL(e, currency, ghostLocker);

    // Check the contract's balance after the settle action
    mathint posBalanceAfter = balanceOfCVL(e, currency, _PositionManager);

    // If CONTRACT_BALANCE flag was set, the contract's entire balance must be used
    assert(amount == CONTRACT_BALANCE() => posBalanceAfter == 0);

    // If CONTRACT_BALANCE flag was set, the locker's balance should remain unchanged
    assert(amount == CONTRACT_BALANCE() => lockerBalanceBefore == lockerBalanceAfter);
}

Recommendation

diff --git a/src/PositionManager.sol b/src/PositionManager.sol
index 52c0192..70dfc02 100644
--- a/src/PositionManager.sol
+++ b/src/PositionManager.sol
@@ -26,6 +26,8 @@ import {Permit2Forwarder} from "./base/Permit2Forwarder.sol";
 import {SlippageCheck} from "./libraries/SlippageCheck.sol";
 import {PositionInfo, PositionInfoLibrary} from "./libraries/PositionInfoLibrary.sol";

+import {ActionConstants} from "./libraries/ActionConstants.sol";
+
 //                                           444444444
 //                                444444444444      444444
 //                              444              44     4444
@@ -210,6 +212,9 @@ contract PositionManager is
                 return;
             } else if (action == Actions.SETTLE) {
                 (Currency currency, uint256 amount, bool payerIsUser) = params.decodeCurrencyUint256AndBool();
+                if (amount == ActionConstants.CONTRACT_BALANCE) {
+                    require(payerIsUser == false, "Payer must not be a user when current contract's balance is used");
+                }
                 _settle(currency, _mapPayer(payerIsUser), _mapSettleAmount(amount, currency));
                 return;
             } else if (action == Actions.TAKE) {

A previous rule is not violated after this fix https://prover.certora.com/output/52567/120916fd9a7647c490b2d57caa0f284b/?anonymousKey=43c8b2e83d1175b135c5461fd44e975e025fb935

teryanarmen commented 1 month ago

Is there a corresponding Cantina bug submission?

alexzoid-eth commented 1 month ago

Is there a corresponding Cantina bug submission?

Yeah, #411

teryanarmen commented 1 month ago

Do you have a link?

alexzoid-eth commented 1 month ago

Do you have a link?

https://cantina.xyz/code/e2cf6906-ec8b-4c78-a585-74ac90615659/findings/411