This document describes the specification and verification of ConstantProductPool by SushiSwap using the Certora Prover. The work was undertaken while the contract was in development and concluded on Nov 4th, 2021.
The scope of our verification was ConstantProductPool contract, a liquidity pool that uses a constant product market maker and consists of two tokens. The LP tokens are called Trident tokens.
The Certora Prover proved the implementation of ConstantProductPool is correct with respect to the formal rules written by the Certora and SushiSwap team.
The next section formally defines high level specifications of ConstantProductPool. The results of running the Certora Prover are available at:
Severity: Critical
Issue: | Loss of all assets |
---|---|
Rules Broken: | integrityOfTotalSupply |
Description: | A burnSingle opertaion can empty a token's reserve. This can be leveraged to an exploit draining both pool's reserves, using a burnSingle followed by a swap. |
Mitigation/Fix: | Updated the burnSingle method to compute burn amount of out reserve and not balance. |
Severity: High
Issue: | Wrong amount out for burnSingle |
---|---|
Rules Broken: | burnTokenAdditivity |
Description: | After burning the Trident tokens, the burnSingle method would always swapping token0 for token1 irrespective of the tokenOut. |
Mitigation/Fix: | Updated the burnSingle method to swap the correct tokens based on the tokenOut. |
Severity: High
Issue: | Non-parametric burnSingle |
---|---|
Rules Broken: | pathSanityForToken0 |
Description: | Users could only burn token1 using the burnSingle method because of a faulty require statement. |
Mitigation/Fix: | Updated the burnSingle method to be able to burn both tokens based on the tokenOut. |
Severity: Medium
Issue: | Denial of Service |
---|---|
Rules Broken: | integrityOfTotalSupply (on older version of the code) |
Description: | If either of the reserves become non-zero when Trident's total supply is zero, then the users would not be able to mint anymore. Furthermore, the _update method was not checking for division by zero when reserve0 is zero, which could cause reverts and halt the system. |
Mitigation/Fix: | All operations are possible only on a non-empty pool. _update method fixed to check for division by zero. |
Severity: Medium
Issue: | Loss of assets |
---|---|
Rules Broken: | afterOpBalanceEqualsReserve |
Description: | The unit for pool's balances and reserves is BentoBox shares, but at some places, they were confused as amounts and converted to shares before transferring. |
Mitigation/Fix: | Removed the unnecessary conversions from amounts to shares in ConstantProductPool. |
Severity: low
Issue: | Validity of pool's tokens |
---|---|
Rules Broken: | validityOfTokens & tokensNotTrident |
Description: | Pool's tokens could be the zero address or the ConstantProductPool contract itself. |
Mitigation/Fix: | Updated the constructor to check the validity of token addresses. |
Severity: low
Issue: | Invalid pool |
---|---|
Rules Broken: | integrityOfTotalSupply (on older version of the code |
Description: | When there is a migrator, there is no check that the balance now is greater than zero. |
Mitigation/Fix: | This feature has been removed |
The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification.
We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Certora or any of its employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here.
✔️ indicates the rule is formally verified on the latest reviewed commit. We write ✔️* when the rule was verified under some simplifying assumption and/or when the verification run timeouts for some functionality of the code (and specify the functions below).
ConstantProductPool is one of the contracts from the Trident system by SushiSwap. The contract works with SushiSwap's BentoBox and TridentRouter, which is another contract of the Trident system. It is a liquidity pool that uses a constant product market maker and consists of two tokens, token0 and token1. Users can deposit liquidity in terms of token0 and token1 to mint Trident tokens. The contract also provides the functionality of swapping tokens and burning Trident tokens to get back liquidity in terms of token0 and token1 or either one of them.
The pool keeps track of the BentoBox balances for both tokens in the form of reserves. Whenever these balances change and an operation is performed, the reserves are updated accordingly. The pool is in a balanced state when the BentoBox balances for both tokens equal the internal state variables keeping track of the reserves.
msg.sender
is not the ConstantProductPool.totalSupply
is zero if and only if both the reserves are zerokLast=0
, meaning that the Bar Fee was ignored.getAmountOut
✔️amountIn
is zero, amountOut
should always be zero.amountIn
token's reserve is zero, amountOut should always be zero.amountOut
cannot be greater than the output token's reserve.totalSupply
should decrease.