Soda Finance Hack: Could Formal Verification Have Prevented It? (Code Included)

Background

Where Is The Bug?!

uint256 maximumLoan = loanInfo[_loanId].amount.mul(loanInfo[_loanId].maximumLTV).div(LTV_BASE);
uint256 maximumLoan = loanInfoFixed[_loanId].lockedAmount.mul(loanInfoFixed[_loanId].maximumLTV).div(LTV_BASE);
require(loanTotal >= maximumLoan, "collectDebt: >=");

Formal Verification and Z3

Formulating The DeFi Problem

  • Variable amount is an unsigned integer, so amount is integer-typed and non-negative.
  • Variable lockedAmount is an unsigned integer, so lockedAmount is also integer-typed and non-negative.
  • Variable loanToal is computed by function getLoanTotal() in line 106 of WETHCalculator.sol, and is actually a sum of amount and interest. Therefore, loanTotal is amount + interest and interest is also unsigned integer.
function getLoanTotal(uint256 _loanId) public view override returns (uint256) { return getLoanPrincipal(_loanId) + getLoanInterest(_loanId); }
  • Variable maximumLoan is computed by code below,
uint256 maximumLoan = loanInfo[_loanId].amount.mul(loanInfo[_loanId].maximumLTV).div(LTV_BASE);
uint256 constant LTV_BASE = 100;
require(_minimumLTV + 5 <= _maximumLTV, "+ 5 <= _maximumLTV"); require(_minimumLTV >= 10, ">= 10"); require(_maximumLTV <= 95, "<= 95");
  • The requirement in line 196 of WETHCalculator.sol could be modeled as loanTotal >= maximumLoan.

Constructing The Proof in Z3 Python

from z3 import *amount = Int('amount')
interest = Int('interest')
lockedAmount = Int('lockedAmount')
factor = Real('factor')
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))
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))

Conclusion

  1. Efforts need to be made on modeling and translating the code. For complex smart contract business logics, this task might take days or weeks.
  2. 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.
  3. Real world formal verification application is still maturing in the blockchain security industry, and tools are limited.

Reference

--

--

--

Blockchain data analytics firm providing security, risk, and compliance solutions.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

Tips an Tricks Python

Implement Domain-Driven Design (DDD) in Golang

Neo4j Driver Best Practices

Docker: Networking & Bind Mounts

Yodel takes over your Customer Support

Introduction to Data Structures And Algorithms — Linked list (singly)

Get more done with value-added services from buzinessware

Freeing up Space in Windows PC [Beginner Guide]

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
AnChain.AI

AnChain.AI

Blockchain data analytics firm providing security, risk, and compliance solutions.

More from Medium

Silo: Secure & Scalable Lending Markets

What Is Decentralized Finance (DeFi) and How Is It Different from Traditional Finance?

What is Decentralized Finance

The centralization in Defi (EVM Blockchain)