Problems in Solidity Fixed Point Libraries — Certora Bug Disclosure

Author: Netanel Rubin-Blaier.
Editors: Uri Kirstein, Yura Sherman.

Background

In computer science, fixed-point representation is a method of representing real numbers by storing a fixed number of digits of their fractional part (i.e. the digits to the right of a decimal point). It is clear that manipulating fixed-point numbers is essential for any DeFi application, e.g., to calculate interest rates, borrowing index, determining the AMM price curve, etc.

What is maybe less obvious is that even small rounding or implementation errors can accumulate and compound, potentially leading to an arbitrage opportunity or even a security vulnerability. Recent examples include:

• The Alpha Homora exploit (Feb 2021)
• The spl-token-lending bug in the Solana Program Library (Dec 2021)
• Yieldly HDL distribution pool exploit (Mar 2022)
• The Hundred Finance exploit (April 2023)
• The Midas Capital exploit (June, 2023)

See also the section on “Security Considerations” in ERC-4626 (Tokenized Vaults) which recommends the use of distinct, opposing rounding directions when computing vault shares.

Two excellent resources for implementing advanced math functions in Solidity are Mikhail Vladimirov’s Math in Solidity blog series, and Remco Bloeman’s website. The latter inspired one of the most popular, gas efficient, and sophisticated fixed-point libraries in Solidity — the PRBMath library, written by Paul Razvan Berg. Overall, the library is incredibly well-written and maintained, including multiple unit tests for its various functions. However, using the Equivalence Checker, we recently discovered a previously unknown design flaw in the PRBMath library which impacts the function:

function mulDivSigned(int256 x, int256 y, int256 denominator) pure 
returns (int256 result)
/// @notice Calculates floor(x*y÷denominator) with full precision.

The problem is simple, but when implemented in the DeFi context it could lead to a critical vulnerability and a loss-of-funds. It is present in every instance of the PRBMath library with version number from 1.1.0 and up to (and including) version 4.0.

As far as we are aware, this is the first time that an automatic tool has found a bug in a public, open-source, Solidity library.

Description of the bug

Roughly speaking, the algorithm PRBMath is using to compute signed multiplication-and-division can be divided into three steps —

1. Extract the signs and the absolute values of the inputs:

• (abs_x,abs_y,abs_d) := absolute values of (x,y,d)
• (sign_x,sign_y,sign_d) := signs of (x,y,d)

// Get hold of the absolute values of x, y and the denominator.    
uint256 xAbs;
uint256 yAbs;
uint256 dAbs;
unchecked {
  xAbs = x < 0 ? uint256(-x) : uint256(x);
  yAbs = y < 0 ? uint256(-y) : uint256(y);
  dAbs = denominator < 0 ? uint256(-denominator) : uint256(denominator);
}
// Get the signs of x, y and the denominator.
uint256 sx;
uint256 sy;
uint256 sd;
// "sgt" is the "signed greater than" assembly instruction and "sub(0,1)" is -1 in two's complement.
assembly ("memory-safe") {
  sx := sgt(x, sub(0, 1))
  sy := sgt(y, sub(0, 1))
  sd := sgt(denominator, sub(0, 1))
}

2. Compute the absolute value of the result by reducing to the unsigned case:

uint256 abs_result = mulDiv(abs_x, abs_y, abs_d);

where

function mulDiv(uint256 x, uint256 y, uint256 denominator) pure 
returns (uint256 result)
/// @notice Calculates floor(x*y÷denominator) with full precision.

3. Compute the overall sign and return the result:

uint256 overall_sign = sign_x ^ sign_y ^ sign_d;
result = (overall_sign == 0) ? -int256(abs_result) : int256(abs_result);

The problem is that step 2 is wrong. We actually have:

So whenever the result is negative, we are actually rounding towards zero and not minus infinity, leading to an off-by-one error.

Impact and Proper Disclosure Procedure

While working on a project, auditors often classify smart contract bugs according to both severity (how much damage could the bug cause: denial-of-service, loss of funds,…) and difficulty (how hard it is for a malicious actor to weaponize the vulnerability into an actual exploit).

We first encountered this bug while working with one of the leading DeFi protocols on unreleased AMM¹ code which used mulDivSigned as part of its computation of the trading function. Under certain circumstances, this arithmetic error would have enabled an attacker to force liquidity pools to accept unfavorable trade², systematically draining the LP-tokens of their worth.

Originally, we classified this vulnerability as critical severity but also high difficulty and notified the client who fixed the problem in their code. However, our initial classification became complicated when we noticed that this arithmetic error occurs in multiple instances of the PRBMath library and could therefore potentially influence many more systems, including live ones.

This presented a bit of a conundrum: even in the world of “classical” computer security, library bugs are notoriously dangerous and it is very hard to estimate severity and difficulty across projects. This difficulty is compounded in Ethereum which lacks native support for upgradable libraries or a mechanism for distributing hotfixes, and where (for gas reasons) people prefer to just copy specific functions from PRBMath and tweak them instead of importing the whole library.

After consulting with leading security researchers samczsun and Mudit Gupta, we conducted a thorough search through public repositories (both off- and on-chain) and notified potential vulnerable projects privately. We also contacted Paul Razvan Berg (the author of PRBMath) who immediately hopped on a call with us and confirmed the findings.

As a result of our investigations, we believe that at this point in time, very few smart contracts use the signed arithmetic portion of PRBMath in a problematic way. Thus, and given the immutable nature of smart contracts, it seems best to expose it to the public.

Mitigation

To address the problem quickly, Paul issued a temporary fix (version 4.1) which changes the definition of mulDivSigned to round toward zero:

function mulDiv(uint256 x, uint256 y, uint256 denominator) pure 
returns (uint256 result)
/// @notice Calculates x*y÷denominator with 512-bit precision.
/// Notes:
/// - The result is rounded toward zero.

In the longer term, this problem will be given a long-term solution as part of an ongoing plan to provide extensive support for multiple rounding modes in PRBMath, see the discussions here for more.

Conclusion

Mathematical Libraries are the basic building blocks of the DeFi ecosystem. However, they are surprisingly hard to get right (especially when one tries to aggressively optimize their gas consumption), and auditing them can be tiresome and difficult.

The above bug demonstrates that even with comprehensive unit testing, there is great methodological advantage in the process of writing formal specification for a system (if only just to ensure that nothing was ignored or overlooked). It also serves as a good example for the expressibility of the CVL Language — an elementary CVL spec (an “equivalence spec”)

was able to detect a 2-year old bug in the Solidity code of a mathematical library which involves extensive Yul segments, numerous bit-hacking tricks, and even a bit of number theory thrown into the mix — all without the need to even understand anything about the details of the implementation.

¹ See, e.g., the survey paper “SoK: Decentralized Exchanges (DEX) with Automated Market Maker (AMM) Protocols” for a quick review of DEX’s, AMM’s, and related DeFi terminology.

² also known as the AMM- or CFMM-invariant.