Bug inside ABDKMathQuad library

[code423n4]

Handle

a_delamo

Vulnerability details

Impact

FairSideFormula library is using ABDKMathQuad library underneath. According to the ABDKMathQuad README, the range of values is the following:

The minimum strictly positive (subnormal) value is 2^−16494 ≈ 10^−4965 and has a precision of only one bit. The minimum positive normal value is 2^−16382 ≈ 3.3621 × 10^−4932 and has a precision of 113 bits, i.e. ±2^−16494 as well. The maximum representable value is 2^16384 − 2^16271 ≈ 1.1897 × 10^4932.

Using Echidna, a fuzzing tool for smart contracts, I found some edge cases when some of the operations do not work as expected. This is the test code I run using echidna-test contracts/TestABDKMathQuad --contract TestABDKMathQuad

// SPDX-License-Identifier: Unlicense
pragma solidity >=0.6.0 <0.8.0;

import "./dependencies/ABDKMathQuad.sol";
import "@openzeppelin/contracts/math/SafeMath.sol";

contract TestABDKMathQuad {
    uint256 internal x;
    uint256 internal x1;

    int256 internal y;

    function setX(uint256 _x) public {
        x = _x;
    }

    function setX1(uint256 _x1) public {
        x1 = _x1;
    }

    function setY(int256 _y) public {
        y = _y;
    }

    function echidna_Uint_convertion() public returns (bool) {
        bytes16 z = ABDKMathQuad.fromUInt(x);
        return ABDKMathQuad.toUInt(z) == x;
    }

    function echidna_int_convertion() public returns (bool) {
        bytes16 z = ABDKMathQuad.fromInt(y);
        return ABDKMathQuad.toInt(z) == y;
    }

    function echidna_mulUint() public returns (bool) {
        uint256 mul = SafeMath.mul(x, x1);

        bytes16 z = ABDKMathQuad.fromUInt(x);
        bytes16 z1 = ABDKMathQuad.fromUInt(x1);
        bytes16 t = ABDKMathQuad.mul(z, z1);
        return ABDKMathQuad.toUInt(t) == mul;
    }

    function echidna_divUint() public returns (bool) {
        if (x1 == 0 || x == 0 || x < x1) return true;
        uint256 div = SafeMath.div(x, x1);

        bytes16 z = ABDKMathQuad.fromUInt(x);
        bytes16 z1 = ABDKMathQuad.fromUInt(x1);
        bytes16 t = ABDKMathQuad.div(z, z1);
        return ABDKMathQuad.toUInt(t) == div;
    }

    function echidna_neg() public returns (bool) {
        bytes16 z = ABDKMathQuad.fromInt(y);
        bytes16 z_positive = ABDKMathQuad.neg(z);
        int256 result = ABDKMathQuad.toInt(z_positive);

        return result == (-y);
    }

    function echidna_ln() public returns (bool) {
        if (x == 0) return true;

        bytes16 z = ABDKMathQuad.fromUInt(x);
        bytes16 result = ABDKMathQuad.ln(z);
        if (result == ABDKMathQuad.NaN) return false;
        uint256 result_uint = ABDKMathQuad.toUInt(result);
        return result_uint < x;
    }
}

And the results are:

echidna_mulUint: failed!💥
  Call sequence:
    setX(1)
    setX1(10389074519043615041642520862277205)

echidna_Uint_convertion: failed!💥
  Call sequence:
    setX(10385528305364854446597578558364193)

echidna_neg: failed!💥
  Call sequence:
    setY(-10394149475425461937254292332080605)

echidna_int_convertion: failed!💥
  Call sequence:
    setY(-10418479581230103876421151985443129)

echidna_divUint: failed!💥
  Call sequence:
    setX1(1)
    setX(10518626300707317802075092650125337)

If we check in Remix, we can see there is a small difference when converting from UInt to Bytes16 or the opposite way. This is probably the same issue with all the other operations.

ABDKMathQuad.fromUInt(10385528305364854446597578558364193);
// 0x40700005e5e8a8c4dcb4999a17cead10
ABDKMathQuad.toUInt(0x40700005e5e8a8c4dcb4999a17cead10)
//10385528305364854446597578558364192

Tools Used

Echidna https://github.com/crytic/echidna

Recommended Mitigation Steps

Use some fuzzing tool like Echidna to verify there is no edge cases

[fairside-core]

I am slightly mixed about this finding. We did employ fuzz tests during the audit we had gone through and they were unable to pinpoint any issues in the value range we expect the curve to be utilized in. This is definitely a good suggestion and one we will assimilate, however, I am not sure how one would judge the severity of this.