*To view the full version, including a more detailed analysis of the code, visit our Github **here**.*

## Background

On Sep 20, 2020, the liquidity mining project DeFi Soda.Finance was hacked by malicious actors, who subsequently liquidated over 400 ETH (around $160,000) from the Soda loan pool. In this blog, we will walk thru the hack incident, and show how we can apply formal verification could have prevented it.

Here are some screenshots of the hacking transactions:

To everyone’s surprise, the loophole exploited by the hackers was simply a mistakenly written variable in the WETHCalculator.sol smart contract. Let’s dive in and see how a seemingly tiny issue caused this huge loss.

## Where Is The Bug?!

The buggy variable was ** amount** in line 193 of WETHCalculator.sol. According to the Soda.Finance blog, this variable should be replaced by

**, which is exactly how the Soda team fixed this bug in line 300 of WETHCalculatorFixed.sol**

*lockedAmount*uint256 maximumLoan = loanInfo[_loanId].amount.mul(loanInfo[_loanId].maximumLTV).div(LTV_BASE);

*WETHCalculator.sol*

uint256 maximumLoan = loanInfoFixed[_loanId].lockedAmount.mul(loanInfoFixed[_loanId].maximumLTV).div(LTV_BASE);

*WETHCalculatorFixed.sol*

The consequence of this mistake was that for whatever input, the following requirement check in line 196 of WETHCalculator.sol would pass, enabling everyone, including hackers to call the ** collectDebt()** function to liquidate WETH stored in the pool.

require(loanTotal >= maximumLoan, "collectDebt: >=");

*requirement check*

## Formal Verification and Z3

This loophole is completely a code logic design issue, and no static scanner is available for detecting such bugs. However, the formal verification technique could be applied here for code logic detection. According to Wikipedia, formal verification is a technique to prove or disprove the correctness of intended algorithms with a set of specifications. In the case of this loophole, formal verification could prove that all valid inputs bypass the requirement in line 196 of WETHCalculator.sol.

The formal verification library Z3 developed by Microsoft Research is a powerful tool for solving this type of code logic, and the following proof will be conducted with Z3Py, a Python binding package of Z3. Here is a slide screenshot from Microsoft Research about the Z3 workflow:

## Formulating The DeFi Problem

In order to convert the code into a formal verification topic, the first step is to formulate the code into mathematical conditions.

- Variable
is an unsigned integer, so*amount*is integer-typed and non-negative.*amount* - Variable
is an unsigned integer, so*lockedAmount*is also integer-typed and non-negative.*lockedAmount* - Variable
is computed by function*loanToal*in line 106 of WETHCalculator.sol, and is actually a sum of*getLoanTotal()*and*amount*. Therefore,*interest*is*loanTotal*and*amount + interest*is also unsigned integer.*interest*

function getLoanTotal(uint256 _loanId) public view override returns (uint256) { return getLoanPrincipal(_loanId) + getLoanInterest(_loanId); }

*getLoanTotal()*

- Variable
is computed by code below,*maximumLoan*

uint256 maximumLoan = loanInfo[_loanId].amount.mul(loanInfo[_loanId].maximumLTV).div(LTV_BASE);

which is essentially ** amount** times the factor

**. The range of this factor is restricted in (0,1) because**

*mul(loanInfo[_loanId].maximumLTV).div(LTV_BASE)***value is 100 defined in line 17 of WETHCalculator.sol, and**

*LTV_BASE***is within 15 ~ 95 defined in line 54 ~ 56 of WETHCalculator.sol. Therefore, we can model variable**

*maximumLTV***as**

*maximumLoan***, where**

*amount * factor***is a real number in range (0,1)**

*factor*uint256 constant LTV_BASE = 100;

*LTV_BASE*

require(_minimumLTV + 5 <= _maximumLTV, "+ 5 <= _maximumLTV"); require(_minimumLTV >= 10, ">= 10"); require(_maximumLTV <= 95, "<= 95");

*maximumLTV*

- The requirement in line 196 of WETHCalculator.sol could be modeled as
.*loanTotal >= maximumLoan*

Z3 is an smt-solver and would tell the user whether there **exists** a solution to the problem or not. After proving that given specific contraints, no solution is available to meet the negation version of requirement: ** loanTotal < maximumLoan**, the requirement

**will always be satisfied.**

*loanTotal >= maximumLoan*To understand this logic reasoning, take genetically modified foods (GM foods) as the example: if anyone finds one type of GM foods that harms human body, then GM foods are dangerous; should all GM foods are good for health, then GM foods are safe. The logic is the same for the above reasoning: if we cannot find a solution that satisfies the negation version of the requirement, then ** loanTotal >= maximumLoan** is always true.

## Constructing The Proof in Z3 Python

To start Z3 programming on theorem proving, the parameters should be initialized as stated in the Formulation section above:

from z3 import *amount = Int('amount')

interest = Int('interest')

lockedAmount = Int('lockedAmount')

factor = Real('factor')

The next step is to verify that ** loanTotal >= maximumLoan** is always true by writing a solver function:

def checkBuggy(amount, interest, factor):

s = Solver()

s.add([amount >= 0, interest >= 0])

s.add([factor > 0, factor < 1])

loanTotal = amount + interest

maximumLoan = amount * factor

s.add(loanTotal < maximumLoan)

return s.check()print(checkBuggy(amount, interest, factor))

The variable ** s** is a Z3 solver object, and the next two lines are contraints, since

**and**

*amount***are unsigned integers and**

*interest***is within range (0,1).**

*factor*** loanTotal** and

**are initialized in the same way as the original code.**

*maximumLoan*The final step is to add the negation version of the requirement to check if there is a solution.

After running this script in the unix terminal, the result is ** unsat**, which is short for unsatisfactory meaning that no solution is available given these constraints. Therefore, it is proved that the requirement will always pass.

Moreover, it is also possible to check the fixed version requirement and see if it will fail given constraints:

def checkFixed(amount, interest, factor, lockedAmount):

s = Solver()

s.add([amount >= 0, interest >= 0, lockedAmount >= 0])

s.add([factor > 0, factor < 1])

loanTotal = amount + interest

maximumLoan = lockedAmount * factor

s.add(loanTotal < maximumLoan)

return s.check()print(checkFixed(amount, interest, factor, lockedAmount))

The only difference between the buggy code and the fixed code is that ** maximumLoan** is the result of

**, instead of using variable**

*lockedAmount * factor***. If this is fixed, then there are specific inputs that make**

*amount***smaller than**

*loanTotal***and fail the requirement check.**

*maximumLoan*After running this script in terminal, the result is ** sat**, which is short for satisfactory meaning that there are solutions making

**smaller than**

*loanTotal***. Therefore, the requirement check will fail under specific circumstances and the hackers now are not able to attack arbitrarily.**

*maximumLoan*The Python source code can be found here .

## Conclusion

Although formal verification is powerful and could mathematically prove a given piece of code’s correctness, this technique is limited due to several disadvantages.

- Efforts need to be made on modeling and translating the code. For complex smart contract business logics, this task might take days or weeks.
- Expertise in formal verification is necessary to construct the proof body. If the code is well-defined, developers would be able to build templates for a series of similar problems. However, current popular DeFi projects are not following common patterns so no template is available to address all DeFi security issues.
- Real world formal verification application is still maturing in the blockchain security industry, and tools are limited.

As of 2020, formal verification is not yet ready for prime time. The AnChain.AI team recommends DeFi, DApp and smart contract development teams to engage with blockchain security professionals that leverage static, dynamic, and statistical analysis to ensure known vulnerabilities are eliminated.

With millions of dollars of your community’s crypto assets locked in these DeFi smart contracts like Soda.Finance, security auditin has become even more essential than ever before.

## Reference

- Consensys Formal Verification Blog: https://media.consensys.net/how-formal-verification-can-ensure-flawless-smart-contracts-cbda8ad99bd1
- Microsoft Research Z3 Tutorial: https://rise4fun.com/z3/tutorial
- Microsoft Research Z3 Video Presentation: https://www.youtube.com/watch?v=wHSmAThRBHg&ab_channel=MicrosoftResearch
- Soda Hack Report: https://weibo.com/5307267565/JlyJgiAz9?type=
- comment