Numerical Analysis Tips for DeFi Audits
Security techniques for analyzing numerical overflow, underflow, and rounding errors in DeFi smart contracts.
This article summarizes Kurt Barry’s seminar delivered at Spearbit, covering critical numerical analysis techniques for auditing DeFi protocols. The full video seminar is available on YouTube.
Key Focus Areas
- Order of magnitude reasoning
- Overflow checking
- Worst-case testing
- Safety in the presence of rounding error
- SMT solver hacks
Examples derive from Spearbit’s audit of Cron Finance’s TWAMM implementation, where gas efficiency optimizations required careful numerical analysis.
Cron Finance Security Review
The TWAMM mechanism is similar to Uniswap V2 but supports long-term orders. Spearbit emphasized gas efficiency, which led to optimizations requiring detailed numerical analysis due to SafeMath usage and storage slot packing.
The full security review is available here.
Double Overflow of Scaled Proceeds
When making long-term orders in TWAMM, proceeds accumulate in a scaled variable divided by total tokens being sold, similar to yield protocols like Yearn.
To save gas, two scaled proceeds values are packed into a single storage slot using 128-bit integers, reducing storage operations. However, this creates a double overflow risk:
One overflow is normally acceptable from a risk perspective, but two overflows can cause fund loss through disproportionate and incorrect differences.
Order-of-Magnitude and Proportionality Analysis
Begin by estimating orders of magnitude for every relevant term:
C.B64 (Constant)
- 2⁶⁴, approximately 10¹⁹ (operates as the round-off protection scaling factor)
_salesRateU112
- Sales rate (tokens sold per block) multiplied by 10^(decimals of token being sold)
_tokenOutU112
- Tokens purchased depends on price relative to the sold token, plus order block interval factors:
- Per block in denominator
- Per order block interval in numerator
- N: factor for number of tokens
- 10^(decimals out): factor for decimal values
Checking the Worst-Case First
Always test the most extreme scenario to understand risk boundaries. Consider this extreme case:
Price Analysis
Both DAI and GUSD are equivalent to 1 USD, so nothing is noteworthy here.
Order Block Interval (OBI)
The OBI is 64. The interval ratio is approximately 10¹⁷, dangerously close to the scaling factor of 10¹⁹, so investigation is needed.
Overflow Analysis
Overflow occurs after roughly 29 order block intervals, equating to about six hours. This falls below the intended five-year safety window for orders.
Other Considerations
Price Differences
Price variations compound overflow risk. DAI-WBTC pairs demonstrate how stark value and decimal differences exacerbate the problem.
Partial Cancellation of Imbalances
Pairs with one asset having few decimals and another being far more valuable (like USDC-ETH) can partially cancel decimal imbalances. Development teams must review worst-case scenarios to avoid overlooking issues.
Scaling Factors
Should be dynamic rather than hardcoded, dependent on the decimals of the relevant denominator token to avoid excessive rounding errors.
Block Number Subtraction Underflow
In the logic for canceling long-term orders, an underflow exists. While not exploitable, it warrants examination:
Orders can be canceled even after fulfillment, potentially triggering underflow. The calculation determines leftover tokens unsold due to early cancellation, which are returned to the owner.
The key is whether the ‘refundU112’ parameter can be smaller than both total liquidity pool reserves and total tokens queued for sale. This requires determining achievability through order-of-magnitude analysis:
Two key variables:
- expiryBlock: block number at which an order expires
- lastVirtualOrderBlock: last block the AMM has processed
Configuring ‘salesRateU112’ with an upper limit of approximately one billion tokens (18 decimal places) transacted per block yields a value approaching maximum uint256, subsequently multiplied to trigger multiple overflows.
The primary concern is the remainder post-multiplication, modulated by 2²⁵⁶. This should align with extractable value. Worst-case analysis redefines the calculation:
The result shows 10⁷⁷ (2²⁵⁶) minus a significantly smaller number. The remaining result far exceeds tokens the contract will reasonably hold, making it unexploitable.
Refactoring for Gas and Safety
Checking Subtractions for Safety
Two checked subtractions have potential concerns if underflow occurs. SafeMath may not be truly safe because reversions could freeze funds; its removal is incentivized as a gas-saving goal.
Second Subtraction
This subtraction is safe by construction and SafeMath can be removed since it’s guaranteed less than or equal to zero, as shown in the ammEndToken1 calculation:
First Subtraction
The first subtraction does not have this property. A decreased denominator can yield a value larger than expected:
Refactoring
To ensure inconsistencies didn’t result from the core invariant calculation, the formula was rewritten to be safer:
By rewriting to explicitly avoid underflow, accuracy is ensured and underflow-caused freezing prevented. This formula is also cheaper gas-wise than the original, with SafeMath dropped.
Using SMT Solvers
Satisfiability Modulo Theories (SMT) checks if a problem expressed in logical and mathematical statements has a solution under certain conditions. SMT solvers allow:
- Automatically finding satisfying assignments
- Transforming Solidity formulas into SMT expressions using tools like Z3’s Python API
- Verifying our rewritten formula is safe and avoids underflow issues
Leveraging Solidity Code in SMT Solvers
Constraints
Precise constraints ensure token reserves match DeFi world orders of magnitude.
Underflow Possibility
Results demonstrated that achieving underflow is very difficult in practice: one sales rate must be extremely high (selling more tokens per block than pool reserves) while the other is extremely low.
This could occur in very low-liquidity pools or where only one token type is sold, but remains impractical.
Conclusion
Understanding math and proper numerical analysis techniques is crucial when reviewing DeFi protocols. By assessing risk via order-of-magnitude understanding, worst-case analysis, checking numerical overflows/underflows, addressing rounding issues, and leveraging deep protocol mathematical understanding with SMT checkers, valuable insights into potential subversions with drastic protocol impacts emerge.