Process
Numerical Review
Last updated:
October 12, 2021

This security review step focuses on the correctness of mathematical computations on integers or fixed point numbers. Numerical code can result in several classes of errors such as mismatched accounting, numerical drift, rounding errors, overflow & underflow errors, etc. Some errors are tricky to find and can only be observed over several transactions or under precise and difficult to find input values.

Identify invariants and assumptions

The first step for each area of numerical computation is to identify what invariant needs to hold true. For example for Uniswap trades, the constant product formula can be used as an invariant for the reserve amounts.

Consider proving correctness directly

One way to build confidence about a particular series of operations is to translate it into equations. Use SSA form to convert a Solidity math function into a series of equations.

Consider modeling in a different programming language

For more complex mathematical routines Solidity testing is comparatively slow. It's possible to rewrite certain mathematical routines in another programming language:

  • Python supports fixed point decimal numbers out of the box and Q-numbers with the support of fxpmath module. hypothesis could then be used to test the invariants
  • Haskell is another popular alternative and QuickCheck is perfect for finding rare numerical errors associated with certain numerical types
  • Finally Rust also has several property testing frameworks.

Use a debugger for a complex series of steps

Use a Solidity Debugger to review a more complex series of numerical steps (such as algorithms for approximating exponentials).

Leverage fuzzing and/or formal verification

Even in Solidity, fuzzing and formal verification are available to try and break invariants. Fuzzing can be useful to find deeper sequences of transactions that result in errors while formal verification can be used for more comprehensive assertions that a given mathematical formula works.

Fuzzing can work well with mathematical operations since the state is usually simpler. Formal verification on the other hand can work less well. Even the simplest math can translate into complex diophantine equations with no closed form solution and require significant iteration.

See Also: