Securing Protocols During Development- From a High Level Invariant to a Pool-Draining Vulnerability in SushiSwap’s Trident

Published in

Certora

7 min readNov 21, 2021

Trident is SushiSwap’s upcoming platform for launching and running liquidity pools and managing their interactions with users; it is expected to handle billions worth of assets. This document describes a pool-draining exploit that was uncovered during its development, and the subsequent fix by SushiSwap. Most importantly, we describe how we rooted out the vulnerability, using a method reproducible for any DeFi pool platform. This method consists of three steps:

1) Formulate a must-hold property or requirement (“invariant” or “rule” below) of the system

2) Use Certora’s automated verification tool to find a concrete scenario that violates the invariant — a specific assignment for the pool’s variables and an operation that breaks the property

3) Leverage the newly-discovered scenario to exploit the system.

Some Background on the Trident Protocol

The bug concerns the automated market maker contract for constant product pools (CPPs). In a CPP, Liquidity providers (LPs) deposit two types of underlying tokens (Token0 and Token1) in exchange for LP tokens. They can later burn LP tokens to reclaim a proportional amount of Token0 and Token1.

Trident users can swap one underlying token for the other by transferring some tokens of one type to the pool and receiving some number of the other token. To determine the exchange rate, the pool returns enough tokens to ensure that

(reserves0 ⋅ reserves1)ᵖʳᵉ =(reserves0 ⋅ reserves1)ᵖᵒˢᵗ

Step 1: Formulate the Invariant

The ability to burn LP tokens into underlying tokens suggests an important invariant: if there are any LP tokens (the totalSupply is greater than 0), then neither reserves₀ nor reserves₁ should ever become zero (otherwise the pool could not produce the underlying tokens). More formally:

totalSupply = 0 ↔ reserves0 = 0

and

totalSupply = 0 ↔ reserves1 = 0

The Certora Prover allows us to write this invariant in the specification for the contract:

Step 2: Find a Violation

Certora’s Prover examines every possible state of the system and every possible operation, and checks that this invariant will always hold. If it is possible to violate a condition, the prover will produce a concrete example showing what can go wrong. From that counter-example, one can find the flaw in their program.

To our surprise, the tool showed that the burn-single operation violated the invariant. The burn-single operation combines a burn and a swap: it first burns LP tokens to produce both kinds of underlying tokens, then swaps one type for the other (producing only a single kind of underlying token).

Even though the `swap` and `burn` operations maintain the invariant, the combined operation had a flaw that allowed a malicious user to drain the pool.

Understanding the burn-single function

To understand the bug in the burn-single function, we need to know a little about how the Trident pool works. The Trident CPP contract tracks the reserves of the pool as reserve0 and reserve1 (for Token0 and Token1 respectively). If underlying tokens are transferred without the intervention of the CPP contract, then the actual balances held by the pool can become larger than the stored reserve variables. Trident refers to the actual underlying balances of the pool as balance0 and balance1.

Suppose a user (Alice) decides to burn her LP tokens using burn-single, asking to receive her share in Token₁ only (TokenOut=Token₁ in full code, line 69 below). Let’s follow the code step by step:

[convert LP tokens to Token0 and Token1] The amounts of Token0 and Token₁ that Alice is due are computed. These are called amount₀ and amount₁, respectively:

The amount of a token that the user is due is the current pool’s balance of that token times her portion of LP liquidity of the total supply of LP tokens. Note that this exact computation appears in the burn function that passed the invariant test.

2. [convert produced Token0 to Token1] Trident computes how much Token1 Alice should receive in exchange for amount0 of Token0. The conversion from Token0 to Token1 is defined by the `_getAmountOut` function, shown below. Since step (1) removed amount₀ of Token0 and amount₁ of Token1 from the pool, the current reserves are reserve0-amount0 and reserve1-amount1. Trident calculates how much amount₀ of Token0 worth in Token1 for the new reserve values:

This value is added to amount₁ above (line 64) that was already granted to Alice, and the sum is transferred to her (line 71).

3. To end the operation, the pool reserves are updated:

The Unseen Problem

So what can go wrong? Remember that the reserves can be smaller than the balances. The Certora Prover crafted a scenario that shows an inconsistency in how these are used: while amount₀ and amount₁ are computed using the balances, they are subtracted from the reserves (this issue was also discovered independently by Cristoph Michel, as we were told by Sushi).

Suppose that before calling burnSingle, the balance is high enough that: amount0=(liquidity/totalSupply)⋅ balance0=reserve0

(The Prover’s concrete assignment had been: balance0=10,000, liquidity=100, totalSupply=1000, reserve0=1000 )

Alice goes on to burnSingle her LP. When asking to receive this amount in Token₁ at step 2 above, the calculation reads:

_getAmountOut(amount0, 0, _reserve1 — amount1)

The calculated amount out will be reserve1 — amount1. In total, the user will get the entirety of reserve1. Now reserve1=0 but totalSupply > 0, breaking the invariant.

Step 3: From a Broken Invariant to a Contract Exploitation

Now that we have a concrete operation that produces an invalid state, we can try to exploit this violation to describe a complete attack on the pool.

Assume an adversary, Mallory, has some liquidity in a CCP. First, she needs to reach the state amount0=(liquidity/totalSupply)⋅ balance0=reserve0. Normally, the balances of a pool equal its reserve: the reserves are updated to equal the balances after each operation of a user. Had there been a difference, any user could use it to gain the difference for herself. Mallory can achieve that state by taking a large flash loan in Token0, then adding all funds to the pool’s balance0. For example, let’s take a pool that holds 1M$ TVL, 0.5M$ of it in Token0, and the remainder 0.5M$ in Token1. If Alice has 1% of all TVL, she must provide the pool with an additional 44.5M$ in token0.

Mallory goes on to burnSingle her LP, asking to receive this amount in Token1. Mallory successfully draws all of Token1 as a result. But how can Mallory pay back the loan, taken in Token0?

In general, programmers are likely to count on fundamental properties of the system and presuppose them in different places for optimization (instead of checking them repeatedly). Here, the Swap function relied on our invariant when it checked that only one of the reserves is greater than 0 before a swap:

Trident assumed that either the pool is initialized and then both reserves aren’t 0, or the pool is uninitialized and then both reserves are 0. In Mallory’s attack, only reserve1 is 0, but the requirement in line 194 holds.

Therefore, to complete the attack, Mallory swaps a single Token1 in the zero-reserve1 pool. Using the same getAmountOut function above with reserve1=0, the reader can verify that Mallory now takes the entire reserve0 of the pool. Mallory can then pay back her loan.

To summarize, to perform the attack, Mallory needs to:

Take a flash loan in Token0
Add a large amount to Balance0
burnSingle with Token1 reserve as output
Swap a single Token1 for the Token0 reserve

SushiSwap’s Fix

SushiSwap responded with a quick fix: calculating the tokens amounts owed to the users in the burn-single function using the reserves instead of the balances.

Conclusion

Thinking about general properties that a system should satisfy is a useful approach for reasoning about the correctness of DeFi systems without reasoning about specific bugs. These properties are not system specific, and don’t require understanding implementation details or enumerating specific bugs. Formal verification can be used to check that an entire system satisfies those general properties, and identifies exploitable bugs.