UNSAFE CASTING CAN LEAD TO ERRORNEOUS `utility` VALUE CALCULATION

[code423n4]

Lines of code

https://github.com/code-423n4/2023-08-shell/blob/main/src/proteus/EvolvingProteus.sol#L831-L834 https://github.com/code-423n4/2023-08-shell/blob/main/src/proteus/EvolvingProteus.sol#L716

Vulnerability details

Impact

The EvolvingProteus._getUtility function is used to calculate the utility value of the pool at the time of the function call. The utilitiy is calculated using a quadratic formula which is shown below:

k(ab - 1)u**2 + (ay + bx)u + xy/k = 0

Above quadratic equation when solved gives us two solutions which differ based on the sign of the discriminant. The discriminant is calculated in the function as shown below:

int256 disc = int256(Math.sqrt(uint256((bQuad**2 - (aQuad.muli(cQuad)*4)))));

This issue here is with the uint256((bQuad**2 - (aQuad.muli(cQuad)*4))) phrase. Since we are taking the square root of the result of the above phrase we are casting its result into uint256.

Now consider the following scenario:

1. The (bQuad**2 - (aQuad.muli(cQuad)*4)) phrase results in a negative value.
2. This is possible when aQuad.muli(cQuad)*4) > bQuad**2.
3. When we cast this negative value to uint256 it will result in a large positive value (since negative int256 is represented in two's complement format).
4. But when aQuad.muli(cQuad)*4) > bQuad**2 this condition occurred the transaction should have reverted.
5. But instead we are getting a large positive value as the answer which will be used to calculate the utility value thus providing a wrong utility value.

Proof of Concept

        // FIXED_FEE * 2 because we will possibly deduct the FIXED_FEE from
        // this amount, and we don't want the final amount to be less than
        // the FIXED_FEE.
        if (absoluteValue < FIXED_FEE * 2) revert AmountError();

https://github.com/code-423n4/2023-08-shell/blob/main/src/proteus/EvolvingProteus.sol#L831-L834

        int256 disc = int256(Math.sqrt(uint256((bQuad**2 - (aQuad.muli(cQuad)*4)))));

https://github.com/code-423n4/2023-08-shell/blob/main/src/proteus/EvolvingProteus.sol#L716

Tools Used

VSCode and Manual Review

Recommended Mitigation Steps

Hence it is recommended to revert the transaction when aQuad.muli(cQuad)*4) > bQuad**2 occurs. This can be done by implementing a require statement (before int256 disc value is calculated) as shown below:

require(aQuad.muli(cQuad)*4) <= bQuad**2, "Wrong Discriminant");

Assessed type

Under/Overflow

[c4-pre-sort]

0xRobocop marked the issue as duplicate of #143

[c4-pre-sort]

0xRobocop marked the issue as low quality report

[c4-pre-sort]

0xRobocop marked the issue as not a duplicate

[c4-pre-sort]

0xRobocop marked the issue as primary issue

[0xRobocop]

Invalid.

Running the following in Z3 using python, says that discriminant cannot be negative if reserves have positive values.

from z3 import *

a = Real('a')
b = Real('b')
x = Real('x')
y = Real('y')

s = Solver()

s.add(y > 0, x > 0, (a*y + b*x)**2 < 4*(a*b - 1)*(x*y))
for c in s.assertions() :
    print(c)

print(s.check())
print(s.model())

[c4-judge]

JustDravee marked the issue as unsatisfactory: Insufficient proof