Formal Verification of Smart Contracts: Equivalence Checking of Uniswap Library
In this blog article, we show how to apply formal verification to ensure correctness of a smart contract. For demonstration, we analyse and
prove that MulDiv
function from Uniswap library
FullMath is correctly implemented, i.e.,
it does not overflow or underflow. We do that by performing equivalence checking — a formal verification technique, to show that the
Solidity based implementation of MulDiv
is equivalent to a reference implementation. At the backend, we use Z3 Theorem Prover
for analysis.Brief Introduction to Formal Verification
Formal verification is a mathematical method for proving the correctness of smart contracts, algorithms, or systems. It involves creating a mathematical model of the system being verified and using mathematical logic to prove that the model meets certain specifications. Formal verification can be used to ensure correctness, security, and reliability of smart contracts. Since the proof is mathematical, it provides 100% correctness guarantee.
Formal verification can be performed by means of several techniques. Here, we shall focus on equivalence checking. Equivalence checking ensures that two designs or implementations of a system are equivalent, and they will behave identically under all possible inputs and conditions. In the context of formal verification of smart contracts, equivalence checking can be used to ensure that different versions of a smart contract, or a smart contract and its specification, are equivalent. This can be particularly useful in situations where a smart contract has been modified or updated, as it can help to ensure that the modified contract is still correct and behaves as intended.
Equivalence Checking of Uniswap MulDiv Function
The MulDiv function calculates floor (a × b ÷ denominator) with full precision. The function throws if result overflows a uint256 or denominator is equal to 0. MulDiv function is available in the Uniswap libraries and it is used at many places in Uniswap. Furthermore, all the dApps using Uniswap’s APIs are also indirectly using the MulDiv function. Hence, it is very important that MulDiv function is formally verified.
Our Approach
In this blog article we use equivalence checking to prove the correctness of MulDiv with respect to a reference model (see Figure below). In principle, one can use their own abstracted reference model as well, but for this article we will use the aforementioned model which is publicly available. Both the models are implemented in Solidity and they achieve the same goal. However, both the models are implemented in a slightly different way. Our goal is to prove that both models are indeed implementing the same functionality.
Installations
For equivalence checking, we are using Z3 theorem prover. First, we need to transform the Solidity implementation of MulDiv to a representation Z3 solver understands. Either we can write the MulDiv function code into SMT-Lib format directly or we can use Z3’s Python API. For this blog article, we will use Python 3 here. The first step is to install z3-solver in your system. You can execute the following command
pip install z3-solver
Afterwards, create a new Python file and import z3. At this point, we have to build a syntax tree of a mathematical formula which is solved by Z3. This can be done in multiple ways. In this blog, we utilize the following approach:
Declarations & Implementation
We start by declaring the function mulDiv which takes 3 parameters as input, a, b, and denominator.
We then declare all locally used variables as symbolic variables of type Bit Vector. Here, it is worth mentioning that we will use Static Single Assignment (SSA). SSA is a form of intermediate representation (IR) in which each variable is assigned exactly once, and every variable is defined before it is used. This has several benefits for analysis of programs. Some of the declarations with 256-bits bitwidth are shown below:
from z3 import *
def mulDiv (a, b, denominator):
prod0= BitVec("prod0",256)
prod00= BitVec("prod00",256)
prod000= BitVec("prod000",256)
prod1 = BitVec ("prod1",256)
mm= BitVec("mm",256)
result0 = BitVec ("result0",256)
result1 = BitVec ("result1",256)
Here, prod0 represents the variable defined the first time, prod00 represents “prod0” defined the second time, and so on. As a next step, we analyze the mulDiv Solidity code shown below
let mm := mulmod(a, b, not(0)) prod0 := mul(a, b) prod1 := sub(sub(mm, prod0), lt(mm, prod0))
In the code excerpt, there is a solidity variable mm which is assigned the result of multiplication and modulo operation. It is followed by a variable prod0 which is assigned the result of multiplication of a and b. The last statement performs multiple operations like subtraction (sub) and a less-than comparison (lt) and assigns the result to prod1. We transform this code into assertions using solver.add() function of Z3 as follows:
s.add (mm == (a * b) % int(negate(0))) s.add (prod0 == a * b)
One important thing to note is that there are no assignments in Z3. Equality symbol (==) is always used. If the code is written in a different way using standard Python syntax, then Python transforms the code into equality symbol by itself.
For prod1, we need to transform the operations in a clever way so that Z3 understands the intended functionality. For this the first step is to write the “if-statement” from Solidity into Z3 expression. Here, if we use Python if-statement, we will get the error that the comparison cannot be done on symbolic variables. Hence, we need to use “if-statement” from Z3. The syntax is as follows:
If (condition, then, else)
The if-statement in Z3 uses capital “I”, and it accepts three parameters, 1) condition to check, 2) operations when condition is True, and 3) operations when condition is False. Another thing to note is that mulDiv function in Solidity uses uint256, i.e., unsigned integers of 256 bit width. Hence, all the comparisons and computations should be unsigned. We write the Z3 expression as follows
s.add (If(ULT(mm, prod0), prod1 == mm - prod0 - BitVecVal(0x1, 256), prod1 == mm - prod0 - BitVecVal(0x0, 256)))
we start with the unsigned comparison of mm and prod0 using Z3 function ULT (Unsigned Less Than). If the comparison results in True, “1” is subtracted from the expression, otherwise “0”. One important thing to note here is that if we write “1” or “0” without wrapping it in any sort(), we will get the error. Hence, we create a BitVecVal with value 1 and it is 256-bits wide. The remaining Solidity code is transformed in a similar way. At the end, it is checked whether prod1 is equal to 0 or not. In Solidity code, the result is return under 2 cases, either when prod1 is equal to 0 or when it is not equal to 0. Again, one has to be creative about formulating it for Z3 solver. Below you can see an excerpt from the Solidity code.
….
….
if (prod1 == 0) {
require(denominator > 0);
assembly {
result := div(prod0, denominator)
}
return result;
}
…
…
result = prod0 * inv;
return result;
To represent the 2 aforementioned cases, we add the following statement:
s.add (If (prod1 == 0, result == result0, result == result1))
We create a variable result which is assigned either result0 or result1 depending on the value of prod1.
Similarly, the mulDiv code from Mikhail is also converted in to Z3 expressions. Once both the functions are implemented, we check if they are equivalent or not. For this, we define an invariant using Z3Py
s.add(Not(ForAll (X, ForAll (Y, ForAll (denom, mulDiv (X,Y,denom) ==mulDiv_medium(X,Y,denom))))))
ans = s.check()
if ans == sat:
print (ans)
print (s.model())
elif ans == unsat:
print ("unsat")
else:
print ("unknown")
It means, we want to check, for all the values of X and Y and denom that the equation holds True. We can check this for equality or we can ask the solver to check for the case(s) when both the functions are not giving same output. In our case, we use the latter and ask the solver to check (s.check ()) for the input combination when the output of both mulDiv programs is different.
At this point, we have Uniswap mulDiv function and Mikhail mulDiv function implemented using Z3 expressions. Additionally, we have the invariant which should always hold true if there are no bugs. The final step is to run the Python code with the following command:
Python Filename.py
Result & Conclusion
The code output is UNSAT, which means for all X, Y, and denom, there does not exist any input value which results in different outputs. Hence, it is proof that the implemented functionality is indeed correct.
We also defined more invariants (properties which should always stay True) but we shall talk about those in our upcoming articles.
The complete code can be downloaded from our GitHub.
About Truscova:
Truscova comes with 30+ years of academic research and hundreds of academic publications which pioneered the area of Formal Verification. The team combines academic leadership, industrial strength and Blockchain expertise. Truscova currently analyzes Solidity code combining Formal Verification techniques: abstract interpretation, constraint solving, theorem proving, and equivalence checking.