Formal Verification helps finding insolvency bugs — Balancer V2 Bug Report

This blogpost details a solvency issue we found in Balancer V2 in February 2021, during our review of the system. It has since been fixed, and is not present in any live version.

Many smart contract systems hold the funds of users. A paramount requirement of those systems is that they stay solvent — a user depositing an asset should always be able to withdraw that asset later. Insolvency usually manifests itself as a denial of service — a user could withdraw their assets only after other users deposit enough assets into the system (somewhat like a Ponzi scheme). In severe cases, the asset loss could be permanent.

There is no catch-all definition for solvency for all smart contracts. Different systems have different entities, user privileges, and fund allocations. If solvency is breached, a user could lose some or all of their deposited assets. We call such a breach an insolvency attack.

Insolvency attacks are severe. They are usually hard to find by manual auditing, as the system has many, even an infinite number of possible states. Using an automated tool to prove solvency gives strong security guarantees about the system and greatly assists in detecting bugs usually missed by other techniques.

Recently, Certora’s automated tool has assisted us in finding an insolvency attack in Balancer V2.

Balancer’s solvency-breaking flash loan bug

Balancer V2 offers an efficient system for joining, exiting, and swapping with liquidity pools. All the interactions with the pools are done through a single contract: the Vault. The Vault keeps track of users’ balances internally in a structure called “internal balance”, which is useful to reduce gas costs for frequent trades. The Vault keeps all the funds of all the users in the system and all the pools.

The Vault offers a flash loan mechanism that allows users to increase their leverage significantly. A flash loan differs from a traditional loan in that it does not require any collateral from users. Instead, it requires the payment of at most one percent fee. Moreover, it must be repaid in full at the end of the underlying transaction.

The simplified code for the flash loan function is provided below:

Balancer V2 flash loan function — simplified code. This code contains an insolvency bug. Other forms of attack, such as reentrancy, equal length of input arrays, and more were actively prevented in the code. Those checks were removed from this text for readability.

This function gets a contract address flashLoanReceiver, and two arrays. The first array lists all the tokens to be borrowed, and the second lists the amounts to be borrowed from the corresponding tokens. For example, with an input of [WETH, DAI] and [200, 200], the flashLoanReceiver loans 200 DAI and 200 WETH (1). If the fee amount is 1%, the receiver will need to provide at least 202 WETH and 202 DAI, or else the loan will revert.

This code enables an insolvency attack. Can you spot it?

Fee evasion

A user can pay less tax by providing the same token twice and splitting the loan in half. For example, let’s assume the user wants to loan 200 USDC, and the flash loan fee percentage is 1%. Suppose they provide as input a token array of [USDC] and amount [200]. The user would have to pay back 202 USDC.
However, the user can instead input tokens as [USDC, USDC] and amounts as [100, 100]. preLoanBalances would be [200, 100]. feeAmounts would be [1, 1]. At line 29, we check that the balance of USDC is now at least 201. This means the user can pay back only 1 USDC in fees, half the tax.
The user can split the loan amount into four: a user borrows [USDC, USDC, USDC, USDC], with amounts [50, 50, 50, 50]. This way, they can pay only 0.5 USDC, 25% of the due tax. This scheme can be generalized to splitting the loan to N equal amounts to pay 1/N of the due fee (2).

We can pay even less fees. Given a total loan amount T, number of divisions n, and fee percentage f, the optimal input array (3) amounts as

where

is:

and the fees we pay are

We can decrease the fees paid exponentially by the number of divisions! For a maximal fee of 1%, and n=10, we can pay only ~ 9*10⁻²¹ as a fee percentage.

Solvency breach

As we saw, a user can avoid paying flash loan fees. However, the vault thinks it collected new fees at every loop iteration. This leads to a potential violation of the vault’s solvency.
The solvency of Balancer V2 for a given token is defined as (4):

balanceOf(vault) >= sum_of_all_internal_blances + sum_of_all_pool_balances + collected_fees

Consider a system with only two users, Alice and Bob. Alice holds 100 USDC tokens in the vault, and Bob also has 100 USDC tokens in the vault. The total USDC holdings of the vault are 200 USDC. The flash loan fee is 1%. Bob borrows a flash loan of tokens [USDC, USDC] with amounts [100, 100], paying only 201 USDC back. The vault’s internal records claim 2 USDC collected tax revenue. Bob withdraws his 100 USDC. Now the vault’s owner draws the 2 USDC collected as tax revenue. The vault currently only holds 99 USDC, and when Alice would now try to withdraw her 100 USDC, her request would revert.

Note that Bob does not have to be malicious for this insolvency attack; Bob is following economic incentives to pay fewer fees.

Solution

Balancer’s team solved the bug by requiring the token address array to be sorted in a strictly ascending order. This prevents giving the same token address as input more than once.

Fixed version of the flash loan code, simplified

Certora formally verified the solution to the bug. This is how the formal verification rule looks like in our specification language:

The Certora specification to catch the bug, simplified

We defined an input additivity property. Suppose we look at two different runs of the contract from the same initial state. The first run executes a flash loan twice with a single token and amount. The second run executes flash loan once but with input arrays tokens and amounts that are the concatenated input arrays of the previous run. Note that we did not constrain the values of the inputs. In particular, token_a and token_b can be the same.

We require that either flash loan reverts or that the concatenated run couldn’t return fewer fees than the separate runs.

The old code violated the rule, but the fixed code satisfied it, as expected.

(1) For simplicity, throughout this document, instead of listing the addresses of the token contracts we write the names of the tokens.
(2) Gas costs also increase linearly by the number of divisions. The attack therefore has a hard limit, where we increase the number of divisions as long as the fees evaded are worth more than the additional gas costs.
(3) The proof of optimality will appear in a future blog post.
(4) We assume the tokens are “well-behaved”. It is trivial to write tokens with back doors that break the solvency property. We only care about naive, practically usable tokens such as DAI and USDC.