Veridise
Published in

Veridise

Detecting Smart Contract Vulnerabilities with Static Analysis

In the previous blog posts, we looked at how static analysis works at a high level. In this blog post, we look into three examples of common smart contract vulnerabilities and explain how static analysis can help detect them.

Reentrancy

One of the oldest DeFi attacks (responsible for the DAO Hack of 2016) is caused by “reentrancy”, which occurs when a contract invokes a function of another contract before it finishes updating any necessary contract state (such as a contract variable tracking refunds). Since the target contract can invoke functions in the source contract (hence the name “reentrancy”), this will cause the vulnerable contract to use stale values. This, in turn, can allow an attacker to access resources that they don’t have any claim to. Commonly, such an attack is used to withdraw more funds from a contract than they actually have, as illustrated below:

How to detect them: Such reentrancy vulnerabilities can be detected by statically checking that no storage variables are updated after an external function is called. In particular, the static analyzer needs to compute which function calls can be made at every program point and which variables are updated. Then, if there exist two program points L1 and L2 such that (1) L1 can execute before L2, (2) L1 can invoke an external function, and (3) L2 can write to a storage variable, then there is a possible vulnerability in the code. It is worth noting that reentrancy vulnerabilities cannot be checked in a sound way using syntactic pattern matching — e.g., storage variables may be updated in subtle ways due to pointer aliasing and external functions may be called in non-obvious ways (e.g., through other function calls).

Flash loan

Flash loan attacks are a relatively new type of DeFi exploit in which an attacker manipulates the price of some asset. For instance, in 2021, multiple flash loan attacks on CREAM finance allowed attackers to steal close to 130M dollars over an undisclosed period of time.

“Flash loan attacks” are named this way because exploiting the vulnerability first requires the attacker to obtain a very large amount of funds, usually through a flash loan. A flash loan attack typically works in the following way:

  • First, the attacker obtains funds through a flash loan. A flash loan is a short-term loan that typically requires little to no collateral. These loans let individuals borrow massive amounts of funds, but the loan must be repaid by the end of the transaction. If the loan is not repaid, the transaction reverts to ensure that the funds are not stolen.
  • Next, the attacker uses these funds to manipulate the price of some asset, allowing the purchase to be below the fair market price. Such price manipulation is possible by exploiting the logic that controls the price of an asset.
  • Finally, the attacker sells the asset to another party at the fair market value. This allows the attacker to not only pay off the flash loan but also to make a lot of money.

This process is illustrated below:

As is evident from this discussion, flash loan attacks are enabled by a vulnerability that allows the attacker to manipulate the price of some asset. Such price manipulation is possible if the logic of the contract computes the value of an asset based on the token balance of some entity. For instance consider the following code:

function _computeOraclePrice() private view returns (uint256) {
return address(uniswapPair).balance * (10 ** 18) /
token.balanceOf(uniswapPair);
}

This code is vulnerable to a flash loan attack because the price of the asset depends on the token balance of uniswapPair. Thus, an attacker can reduce the price by flooding uniswapPair with a large number of tokens.

How to detect them: These types of flash loan vulnerabilities can be detected through a static analysis technique called “taint analysis”. The goal of such an analysis is to determine whether some value tainted via a “source” can flow to a “sink”. Many types of static analysis problems can be formulated in this taint framework, and a flash loan vulnerability is no exception. In particular, the source in this context corresponds to the token balance of an entity, and the sink is the return value of a function that computes the price of some asset. Hence, by performing taint analysis in this way, we can determine whether a given contract is vulnerable to a flash loan attack.

Arithmetic Over- and Under-flow

Integers used in smart contracts are not unbounded integers in a mathematical sense. For instance, consider the commonly used type of uint256 which represents unsigned integers of 256 bits. Thus, values of type uint256 hold integers in the range $[0, 2^{256}-1]$. Now, consider an expression such as $x-y$ where $x$ (of type uint256) has value 1 and $y$ (also of type uint256) has value 2. Since uint256 only represents integers in the range $[0, 2^{256}-1]$, the subtraction will result in an arithmetic underflow and wrap around to $2^{256}-1.$ Hence, unsafe arithmetic operations (such as our $x-y$ example) can be exploited by attackers to steal funds, as have happened with many contracts such as the BEC token.

To see how arithmetic over- or underflows can be exploited, consider the following function for withdrawing funds from a contract:

function withdraw(uint256 _amount) {
uint256 balance = userBalances[msg.sender];
require(balance — _amount >= 0, “Insufficient balance”);
userBalances[msg.sender] -= _amount;
(bool success, ) = msg.sender.call{value: _amount}(“”);
require(success, “Failed to send”);
}

This code attempts to check that the caller has sufficient funds in their account through the first require statement. However, if _amount is larger than balance, the subtraction will underflow, and balance — _amount will be a large positive integer. Hence, the transaction will not revert, and it will proceed to send the caller more funds than they have in their account.

How to detect them: We can statically detect such arithmetic safety problems using the type of analyses we talked about in the previous blog post. For example, we can use abstract interpretation to infer lower and upper bounds on integers and check whether they are in a range consistent with their type. Going back to the code example above, since _amount can be any number in the range $[0, 2^{256}-1]$, the static analyzer would not be able to prove that balance — _amount is also in the range $[0, 2^{256}-1]$ and would report that the subtraction operation is potentially unsafe.

Summary

In this blog post, we looked at three common types of smart contract vulnerabilities and discussed how static analysis can be used to detect them. Our static analyzers at Veridise can check for all of these common vulnerabilities as well as many others not described in this blog post. However, the absence of a common vulnerability does not guarantee the correctness of a DeFi application, as attackers continuously come up with new zero-day exploits. Hence, it is important to check not only that a contract is devoid of common vulnerabilities but also that “it behaves as intended”. In the next blog post, we will talk about how we can go beyond common vulnerabilities and prevent zero-day exploits by using formal verification technology.

About Veridise

Veridise offers thorough and comprehensive security audits for blockchain applications. Leveraging our expertise in automated program analysis, Veridise provides state-of-the-art solutions for ensuring security of decentralized finance applications. If you’re interested in learning more information, please consider following us on social media or visiting our website:

Website | Twitter | Facebook | LinkedIn | Github

--

--

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