Overview

This article is a written breakdown of Kurt Barry’s seminar delivered at Spearbit.

Spearbit is a decentralized and industry-leading blockchain security services firm pairing protocols with top security researchers with deep subject matter expertise to identify vulnerabilities in an ever-evolving landscape.

Kurt Barry is a Spearbit Lead Security Engineer (LSR) and his seminar in video form is available on Youtube.

This article is not meant to be a complete replacement of Kurt’s seminar and instead as supplementary material to support deeper understanding. We highly recommend watching the video seminar as well.

In this seminar, Kurt shares his insights on numerical analysis techniques for DeFi audits. The key areas of focus include:

• Order of magnitude reasoning
• Overflow checking
• Worst-case testing
• Safety in the presence of rounding error
• SMT solver hacks.

Examples and analysis stem from Spearbit’s audit on Cron Finance’s implementation of TWAMM. A recurring theme throughout this security review was emphasizing gas efficiency, which led to optimizations that required careful numerical analysis due to safe math being used or storage slot packing being implemented.

Cron Finance Security Review

The TWAMM mechanism is similar to Uniswap V2, however, the key difference is that it also supports long-term orders.

Spearbit performed a security review on Cron Finance’s implementation of TWAMM. Strong emphasis was made on gas efficiency, which led to optimizations that required careful numerical analysis due to SafeMath being used or storage slot packing being implemented.

The security review itself is available here.

Double Overflow of Scaled Proceeds

When making a long-term order in TWAMM, proceeds (tokens purchased) are accumulated in a standard accumulator-style variable which gets scaled in the denominator divided out by the total amount of tokens being sold.

• This is similar to other yield protocols such as Yearn where earnings are accumulated and distributed proportionately.
• In the case below, we are calculating total purchases over all long-term orders which gets scaled in the denominator divided out by the total amount of tokens being sold.
• To save gas costs further in TWAMM implementation, two scaled proceeds values are packed into a single storage slot using 128-bit integers as you’re essentially performing half as many s-store operations.
• However, this leads to a double overflow as shown below:

One overflow in this scenario is assumed and accounted for from a risk perspective, however, two overflows can result in loss of funds as the differences will be disproportionate and incorrect.

Order-of-Magnitude and Proportionality Analysis

In order to perform this type of analysis, we begin by by estimating orders of magnitude for every relevant term as shown below:

C.B64 (Constant)

• 2⁶⁴, which is roughly 10¹⁹ (operates as the round-off protections scaling factor)

_salesRateU112

• The sales rate (Number of tokens being sold per block) multiplied by 10^(Decimals of token being sold) for tokens coming in.

_tokenOutU112

• Tokens being purchased will depend on price of that token relative to the one being sold. There is also the factor of the order block interval:
• per block in the denominator
• per order block interval in the numerator
• N — Factor for the number of tokens
• 10^(decimals out) — Factor for decimal values of token out

Checking the Worst-Case First

Always check the most-extreme example in order to test the problem at it’s most extended boundaries in order to understand the end of the spectrum for risk starting from the tail-end.

Let’s take a look at an extreme case:

Price Analysis

Simple and straightforward as both are equivalent to 1 USD so nothing noteworthy here.

Order Block Interval (OBI)

The OBI within the code itself states that it is 64. The interval ratio comes out to about 10¹⁷ which is a bit too close to the scaling factor of 10¹⁹. Thus, we should investigate:

Overflow Analysis

An overflow time calculation shows that we need about 29 order block intervals to overflow. This equates to about six hours, which is below the intended safe length of time for an order (five years).

Other Considerations

Price Differences

Differences in price can prove to be problematic. Above there is an example of a pair (DAI-WBTC) which compounds the risk of overflow due to the stark difference value of price as well as decimals.

Partial Cancellation of Imbalances A ****pair where one asset has very few decimals and the other is far more valuable such as in the below slide (USDC-ETH), can contribute to a partial cancellation of decimal imbalances. It’s important for development teams to review worst case scenarios to prevent overlooking potential issues.

Scaling Factors

Should be dynamic instead of hardcoded and dependent based on the decimals of the relevant token being provided in the denominator.

By doing so, we can avoid excessive rounding errors.

Block Number Subtraction Underflow

Let’s take a look at another example. In the logic for canceling long-term orders, there is an underflow present. Let’s dive into how this underflow occurs. While the underflow was present, it was not exploitable, but the presence is still worth mentioning.

An order is able to be cancelled even after it has been completely fulfilled. This condition, however, can lead to an underflow. The calculation, as depicted above, aims to determine the quantity of tokens initially earmarked for sale but ultimately not sold due to an early cancellation of the order. These leftover tokens would then be returned to the owner.

The key lies in the ‘refundU112’ parameter. If it represents a quantity of tokens smaller than both the total reserves in the liquidity pool and the total number of tokens lined up for sale, then it opens up an opportunity to extract value. This, however, hinges on the ability to get this value within a manageable range.

The challenge is now to figure out whether this is achievable. To do this, let’s conduct our basic order-of-magnitude analysis:

We consider two key variables:

• expiryBlock - represents the block number at which an order expires
• lastVirtualOrderBlock - denotes the last block that the Automated Market Maker (AMM) has processed.

Next, we configure ‘salesRateU112’ with an upper limit approximation of a billion tokens (with 18 decimal places) transacted per block.

Upon performing these operations, we find ourselves dealing with a value that comes dangerously close to the maximum uint256 value, which will subsequently be multiplied by another number to trigger multiple overflows.

Our primary concern at this juncture is the remainder value obtained post-multiplication, modulated by 2²⁵⁶. Ideally, this remainder should fall within a range that aligns with the value extractable from the contract. To simplify our evaluation and address this concern, we will undertake a worst-case analysis by redefining the calculation:

What we end up with is a result where 10⁷⁷ (2²⁵⁶) is subtracted by a number significantly smaller than itself. As a result, the remaining result is far larger than the amount of tokens that the contract will ever reasonably hold, and is therefore not exploitable.

Refactoring for Gas and Safety

Checking Subtractions for Safety

Here we have two checked subtractions that have potential concerns if an underflow occurs. SafeMath may not necessarily be very safe because reverting could make funds get stuck and the removal of it is still incentivized as a key goal of this security review as gas savings.

Second Subtraction

The second subtraction is completely safe and we can remove SafeMath because it's less than or equal to zero by construction as shown in the **ammEndToken1** calculation above. Safemath here could be safely removed.

First Subtraction

However, for the first subtraction, this does not apply as the the decreased denominator can result in a potentially larger than the expected value:

Refactoring

In order to ensure that inconsistencies did not result from the core invariant calculation, the formula was rewritten to be safer as shown below:

By rewriting the formula in a way that explicitly avoids underflow, we can ensure that our results are accurate and avoid getting stuck due to an underflow. This new formula is also cheaper gas-wise than the original one as SafeMath has been dropped.

Using SMT Solvers

Satisfiability Modulo Theories (SMT) is a method used to check if a problem or question (expressed in terms of logical and mathematical statements) has a solution or not, under certain conditions. Using an SMT solver we can:

• Automatically find satisfying assignments for these types of expressions.
• Transform our Solidity formula into an SMT expression using tools like Z3’s Python API.
• Using an SMT solver allows us to check if our rewritten formula is safe and avoid potential issues with underflow.

Leveraging our Solidity Code to Enter into a SMT Solver

Constraints

• Precise constraints were added to make the token reserves be orders of magnitude that one would expect in a DeFi world.

Underflow Possibility

In the analysis the results demonstrated that achieving underflow may be very hard in practice as one sales rate has to be extremely high (selling more tokens per block than there are reserves of that token in the pool) and the other token’s has to be extremely low.

This could happen in pools with very low liquidity or where only one type of token is being sold, however, as mentioned before, this seems like this would be very hard to achieve in practice.

Conclusion

Understanding math and proper numerical analysis techniques is crucial when reviewing DeFi protocols. Through assessing risks via understanding orders of magnitude, worst case analysis, proper checking of numerical overflows/underflows, rounding issues, and leveraging a deep understanding of the protocol’s mathematical functionality to use an SMT checker we can gain valuable insights into possible subversions of anticipated functionality that can have drastic impacts across the protocol.

Looking for a Security Review?

Please contact us via our submission form.

You may also reach out to us via our Twitter: SpearbitDAO

For a brief overview of what Spearbit is and what we have to offer please see this tweet