Popsicle Finance Bug — Revisited. Could the hack be prevented?

We explain the coding error in Popsicle Finance that was exploited to steal $20mm of users’ funds and ask the question, “could the hack be prevented?”. We also provide a simplified example of the vulnerable contract and access to the Certora prover to try it yourself.

Introduction

Popsicle Finance is a yield optimization platform for liquidity providers. In simple terms, instead of providing liquidity directly to UniSwap (or any other platform) to gain interest, you can deposit your assets in the Popsicle Finance smart contract. They will optimize your yield from fees as well as the impermanent loss by using models to pick the correct low and high range of the LP in Uniswap V3.

When an investor deposits money to the Popsicle Finance smart contract, she gets newly minted Popsicle tokens proportional to the deposited amount, which she can withdraw at any time with the earned profits she deserves.

On August 4, 2021, the Popsicle Finance team was hacked and lost $20MM of users’ funds. In short, the Popsicle Finance team implemented a gas-efficient system to distribute the gained profits that involved maintaining information per user. When a user deposits, withdraws, or transfers Popsicle tokens, the system should update that user’s data before transferring the funds. The Popsicle Finance team didn’t update those values in the transfer method, which led to a severe vulnerability that could have drained all of the Popsicle Finance funds.

The Popsicle Finance bug

Popsicle implements its profit distribution system by maintaining a global counter that records the profits earned per LP token. When a user invests, the system records the value of the global counter at that time. When a user withdraws her investment, the system calculates her profit as the product of her LP balance and the difference between the current value of the global counter and its value at the time of the investment.

The bug occurs when one user transfers LP tokens to another user. The system correctly computes the new balances, but it does not change the value of the profits-per-token it maintains for every user. This allows an attacker to transfer N tokens which were minted when the global counter was X to a collaborator who invested when the global counter was Y < X. As a result, the collaborator is now credited with a profit of N*(X-Y), a profit which none of the parties deserve. See the chart below for a concrete example with N=10 and X-Y=α.

Initially, the attacker doesn’t own any LP token. The attacker friend has 1 token, and its profits-per-token value is k, which were earned fairly. The attacker deposits 10 LP tokens and transfers its newly minted tokens to its friend. The friend is credited with its unchanged profits-per-token value for the newly received tokens from the attacker. Therefore the friend can withdraw all the funds, with a profit of 10k more than deserved.

Once the bug is found, it is easy to fix — the transfer method should credit the receiver with its gains and reset the value of its profits-per-token to the value of the current counter at the time of the transfer. But losing $20MM to an attacker to find the bug is an expensive proposition; in the next section, we show how to find it much more cheaply using the Certora Verification Tool.

Preventing the Popsicle Hack: A Certora Verification Tool Case Study

At Certora, we write rules that describe desired properties of the system. If the rules can be violated, the Certora Verification Tool gives us a concrete counterexample that demonstrates the vulnerability. If the Prover determines that the rules cannot be violated, it provides proof that the contract satisfies the desired property.

The contract violated property is that transferring tokens should not increase the parties’ total assets (worth). Clearly, after transferring to a user with a greater profits-per-token, the parties’ total profit increases, increasing their worth. The Certora Prover finds the instance that allows that to happen.

rule increase_total_value_without_actually_adding_assets() {
    env e;
    address a;
    address b;
    uint amount;
    uint total_balance_before = assetsOf(e, a) + assetsOf(e, b);
    transferFrom(e, a, b, amount);
    uint total_balance_after = assetsOf(e, a) + assetsOf(e, b);
    assert (total_balance_after == total_balance_before);
}

Every contract that implements a transfer function should satisfy this property, and we recommend verifying it on every contract. For example, the same rule would also find the BOG finance vulnerability exploited on May 22, 2021.

Try it yourself

We implemented a small version of the Popsicle Finance contract with the same fees handling system. Take a look at the demo https://demo.certora.com/. The file `PopsicleBroken.sol` contains the vulnerable contract, which you can verify by selecting the `Popsicle.spec` and clicking “Start Verification”. We have corrected the `transferFrom` function as suggested above in the file `PopsicleFixed.sol`; verifying the Popsicle spec file against this version shows that the vulnerability has been fixed.

As discussed, the fix is to implement transfer, transferFrom methods instead of blindly inherit them from the ERC20 implementation as done in the broken version.