Numerical Analysis for DeFi Audits: A TWAMM Case Study by Kurt Barry

Numerical Analysis Tips and Tricks for DeFi Audits

In this talk, Kurt discusses numerical analysis tips and tricks for DeFi audits with a focus on the TiWam audit conducted by Spear Bit. The tools discussed include order of magnitude reasoning, overflow checking, worst-case testing, safety in the presence of rounding error, and SMT solver hacks.

Introduction

• Kurt introduces himself and the topic of his talk.

• He mentions that he will be discussing numerical analysis tips and tricks for DeFi audits with a focus on the TiWam audit conducted by Spear Bit.

Analyzing DeFi Math

• Kurt discusses some tools for analyzing DeFi math including order of magnitude reasoning, overflow checking, worst-case testing, safety in the presence of rounding error, and SMT solver hacks.

TiWam Audit

• Kurt explains that the TiWam mechanism is similar to Uniswap V2 but also supports long-term orders.

• He mentions that Spear Bit audited the Crown Finance implementation of TiWam.

• A recurring theme throughout this audit was gas efficiency which led to optimizations that required careful numerical analysis due to safe math being used or storage slot packing being implemented.

Double Overflow of Scaled Proceeds

• When making a long-term order in TiWam, proceeds are accumulated in an accumulator-style variable which gets scaled in the denominator divided out by the total amount of tokens being sold.

• To save gas costs further in TiWam's implementation, two scaled proceeds values are packed into a single storage slot using 128-bit integers.

• However, this can lead to double overflow which can cause the loss of money.

Conclusion

• Kurt's talk is not about showing off cool findings but rather about the process and reasoning tools used in numerical analysis for DeFi audits.

Understanding Token Sale Rate

In this section, the speaker discusses how to calculate the token sale rate and what factors affect it.

Factors Affecting Token Sale Rate

• The constant is 2^64 or about 10^19.

• The sale rate is the number of tokens sold per block, which can be bounded later.

• The number of decimals for the token being sold affects the sale rate.

• The price of the token being purchased relative to the one being sold affects the sale rate.

• The order block interval is a factor in calculating the sale rate.

Ratio Calculation and Safety

• The ratio depends on price, order block interval, and unit value for each token.

• The ratio needs to be small compared to 10^19 for safety.

• If things are fine for an extreme but reasonable example, then we can stop worrying about it.

Analyzing Decimal Imbalances

In this section, the speaker discusses decimal imbalances and their potential impact on token pools.

Decimal Imbalances Analysis

• Decimal imbalances can cause issues with token pools.

• DAI has 18 decimals while GUSD has two decimals. Both stable coins could be in a pool together.

• Price differences between tokens can also cause issues with token pools.

Overflow Time Calculation

• 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 between tokens can partially cancel out decimal imbalances in some cases.

• It's important to write tests to confirm math and reasoning.

Order of Magnitude Analysis

The speaker discusses the importance of checking worst-case scenarios and highlights an example where a hard-coded value was replaced with a scaling factor based on token decimals and denominators.

Importance of Worst-Case Scenarios

• Dev teams should check worst-case scenarios to quickly identify potential problems.

• Time to overflow doesn't depend on token sales rate, but rather on bounded prices.

Scaling Factor Based on Token Decimals and Denominators

• Hard-coded values can be replaced with scaling factors based on token decimals and denominators.

• Extreme prices could be an issue, but for reasonable tokens that currently exist, it's not a big deal.

Underflow Issue

The speaker discusses an underflow issue in the logic for canceling long-term orders. They explain how this calculation works and how it can lead to extracting value from the contract.

Canceling Long-Term Orders

• Cancelling an order after it's been completely filled leads to underflow.

• Calculation determines how many unsold tokens are returned when cancelling an order early.

Extracting Value from the Contract

• If the right-hand side value is less than total reserves of the pool and total tokens queued to be sold, you can extract value.

• Basic order of magnitude analysis helps determine if refund u112 value is in a feasible range.

Evaluating Mod Easily

• Multiplication overflows many times; what matters is the remainder mod 256.

• Rewrite expression in a way that allows for easy evaluation of mod.

Mathematical Multiplications and Modulus

In this section, the speaker explains how to rewrite mathematical multiplications using modulus.

Rewriting Multiplication Using Modulus

• The speaker makes the modulus explicit.

• Rearrange the terms to get a value that is very small compared to 2 to the 256.

• The first term is a nice multiple of two to the 256.

Evaluating Order of Magnitude Directly

In this section, the speaker explains how to evaluate order of magnitude directly.

Evaluating Order of Magnitude Directly

• Drop all things that are multiplied by 2 to the 256 except for one leading factor of 2 to the 256.

• Get something where there is no modulus involved anymore and look at its order of magnitude directly.

• The result is still basically 10^77 which is way more tokens than will ever be in the contract.

Refactoring for Gas and Safety

In this section, the speaker explains how gas optimization can make code safer.

Checking Subtractions for Safety

• Two checked subtractions have potential concerns if an underflow occurs.

• Removing safe math may not necessarily be very safe because reverting could make funds get stuck.

• The second line is completely safe and we can remove safe math because it's less than or equal to zero by construction.

• For the first line, there's a division that goes in the wrong way so we cannot remove safe math.

English Rewriting a Formula for Safety

In this section, the speaker discusses how to rewrite a formula for safety and the benefits of doing so. They also introduce Satisfiability Modulo Theories (SMT) and demonstrate how it can be used to check if a formula is safe.

Rewriting the Formula

• The original formula had potential issues with underflow, which could lead to incorrect results.

• 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.

Symmetry in Formulas

• A good way to spot bugs in formulas is by checking if they have manifest symmetry when interchanging indices.

• The original constant product formula had this symmetry but it was hidden. The rewritten formula has obvious symmetry.

Using SMT Solvers

• Satisfiability Modulo Theories (SMT) refers to a class of mathematical problems that involve finding satisfying assignments for Boolean predicates involving mathematical objects like integers, rationals, reals, and bit vectors.

• An SMT solver can automatically find satisfying assignments for these expressions.

• We can transform our Solidity formula into an SMT expression using tools like C3's Python API.

• Using an SMT solver allows us to check if our rewritten formula is safe and avoid potential issues with underflow.

Verifying Underflow

In this section, the speaker discusses how to verify if an underflow is possible in a given scenario using an SMT checker.

Using Conditions to Find Underflow

• To find an underflow, add a condition that sum zero is less than the token zero reserves at the end.

• Call check on the model and it returns a three-letter sat which means satisfiable or satisfied.

Getting Concrete Solutions

• Use s dot model to get the concrete solution out of that. It gives you the set of initial input variables that you declared for the token reserves and the token inputs.

Adding Constraints for Realistic Assignments

• Add more constraints to get more realistic assignments. The speaker added some constraints to make the token reserves be orders of magnitude that we would maybe expect in a D5 world and also tried to constrain the token zero input to try to get something that would be a realistic exploit or something that maybe a hacker can achieve.

• This isn't a terribly interesting concrete solution because the numbers are so tiny right, but it's possible to add more constraints for more realistic assignments.

Difficulty Achieving Underflow in Practice

• Achieving underflow may be very hard in practice because one sales rate has to be extremely high and the other one has to be extremely low. By extremely high, it means selling like more tokens per block than there are reserves of that token in the pool.

• This could happen in pools with very low liquidity or where only one type of token is being sold.

• It seems like this would be very hard to achieve in practice.

Refactoring Verification

In this section, the speaker discusses how to refactor verification using an SMT checker.

Checking Refactoring

• Check the refactoring if Z3 is not needed because the reasoning was very simple.

• When we put it in and do the check, it comes back unsat which means unsatisfiable.

• It confirms that we can't get an underflow here.

Understanding Math for SMT Solver

In this section, the speaker discusses what level of math understanding is required to use an SMT solver.

Basic Understanding of Math Required

• You need a basic understanding of math to use an SMT solver. If you're able to understand the math that the code is doing, you can just type it into the SMT Checker and it'll spit numbers out.

• You probably need to be pretty good at math too write an SMT solver.

• Any math that you're able to understand just from looking at it can be put in there.

Accessibility of Formal Verification

• Maker has done some work on trying to make formal verification more accessible. There are some tutorials created for basic stuff that introduce things like Z3's Python API.

• These tutorials can help people who are interested in learning more about formal verification.

Difficulty of Auditing

In this section, the speaker discusses how difficult auditing can be depending on what is being audited.

Difficulty Depends on What Is Being Audited

• The difficulty of auditing depends a lot on what is being audited. If you're doing anything in DeFi, you won't be able to avoid doing a certain amount of math-heavy work.

Defi Tools and Audit Experience

In this section, the speaker talks about the tools required for auditing DeFi projects and shares their experience of auditing a project.

Required Tools for Auditing DeFi Projects

• Basic static analysis tools like Slither are useful.

• Being able to use an SMT solver can be helpful in some cases.

• A testing framework is essential. Foundry has good fuzzing capabilities built-in, while Echidna is also a good option.

• A unit test framework, fuzzer, static analysis tool, and formal verification tool like an SMT checker are necessary.

Audit Experience

• The audit was active with many findings and discussions.

• The team meshed well together and split up tasks effectively.

• The KRON Finance team was active in following issues and giving guidance on problem areas.

• It was a chaotic process due to the amount of information flying around. Keeping everything organized with GitHub issues could have been done better by writing things up into condensed issues sooner.

• Overall it was a great audit experience that provided valuable learning opportunities.

Specialization Areas for Auditors

• Numerical analysis and simulation could be an area of specialization as protocols become more complex.

• Economic reasoning could also be an area of specialization as there is often a game-theoretic level to these protocols beyond just implementing algorithms correctly.

The Role of Auditors in Specialization

In this section, the speaker discusses the role of auditors in specialization and emphasizes the importance of basic knowledge.

Auditors Need Basic Knowledge

• Auditors will always need to know the basic stuff.

• Specialization creates opportunities for auditors to specialize in certain areas.

• However, it is important for auditors to have a strong foundation in basic knowledge.

Conclusion

• The speaker thanks everyone for attending.