From 96e1766a159cf5140bbcf32ae3e338d142aa311c Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Wed, 26 Mar 2025 19:39:25 +0200 Subject: [PATCH 1/6] cpp mini example for demo --- DEFI/CPP_mini/README.md | 43 ++++ DEFI/CPP_mini/certora/conf/runBroken.conf | 16 ++ DEFI/CPP_mini/certora/conf/runFixed.conf | 16 ++ DEFI/CPP_mini/certora/helpers/DummyERC20A.sol | 14 ++ DEFI/CPP_mini/certora/helpers/DummyERC20B.sol | 13 ++ DEFI/CPP_mini/certora/spec/CPPMini.spec | 109 ++++++++++ DEFI/CPP_mini/foundry.toml | 8 + DEFI/CPP_mini/src/ConstantProductPoolMini.sol | 196 +++++++++++++++++ .../src/ConstantProductPoolMiniFixed.sol | 197 ++++++++++++++++++ DEFI/CPP_mini/src/ERC20.sol | 151 ++++++++++++++ DEFI/CPP_mini/src/Math.sol | 72 +++++++ DEFI/CPP_mini/test/CPPMini.t.sol | 87 ++++++++ DEFI/CPP_mini/test/CPPSetup.sol | 31 +++ 13 files changed, 953 insertions(+) create mode 100644 DEFI/CPP_mini/README.md create mode 100644 DEFI/CPP_mini/certora/conf/runBroken.conf create mode 100644 DEFI/CPP_mini/certora/conf/runFixed.conf create mode 100644 DEFI/CPP_mini/certora/helpers/DummyERC20A.sol create mode 100644 DEFI/CPP_mini/certora/helpers/DummyERC20B.sol create mode 100644 DEFI/CPP_mini/certora/spec/CPPMini.spec create mode 100644 DEFI/CPP_mini/foundry.toml create mode 100644 DEFI/CPP_mini/src/ConstantProductPoolMini.sol create mode 100644 DEFI/CPP_mini/src/ConstantProductPoolMiniFixed.sol create mode 100644 DEFI/CPP_mini/src/ERC20.sol create mode 100644 DEFI/CPP_mini/src/Math.sol create mode 100644 DEFI/CPP_mini/test/CPPMini.t.sol create mode 100644 DEFI/CPP_mini/test/CPPSetup.sol diff --git a/DEFI/CPP_mini/README.md b/DEFI/CPP_mini/README.md new file mode 100644 index 00000000..6d4fbdae --- /dev/null +++ b/DEFI/CPP_mini/README.md @@ -0,0 +1,43 @@ +## Mini Constant Product Pool + +The following system is based on a simplified version of the Trident bug that was found by the Certora Prover. +You can find a brief explanation about the original system and bug here: +https://medium.com/certora/exploiting-an-invariant-break-how-we-found-a-pool-draining-bug-in-sushiswaps-trident-585bd98a4d4f + + +In constant-product pools, 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)ᵖᵒˢᵗ +where reserves0 and reserves1 are the amount of token0 and token1 the system holds. + +On first liquidity deposit, the system transfers 1000 LP tokens to address 0 to ensure the pool cannot be emptied. + +An important property is that if there are liquidity providers (totalSupply >0) than there must be assets in both tokens. +This property is written in CVL and in foundry as invariant. +### Fuzz test + +To run the fuzz test from the CPP_mini folder: +``` +forge coverage --report lcov --report-file fuzz --match-contract CPPMini +genhtml fuzz -o fuzzcov +open fuzzcov/index.html +``` +Coverage is very good - 96.3% however bug is missed. + +The bug is demonstrated in a manual crafted test `test_manual()` and shows how it can cause a complete drain of the protocol. + + +### Formal verification +To run the verification: +```certoraRun certora/conf/runBroken.conf``` + +As seen in the report: https://prover.certora.com/output/40726/4ba34bd0d7d54c279c7cb261d1616fef/?anonymousKey=626461dda2213599b57007646d3198b21c249908 + +The property is violated + +Once the bug is fixed the property is verified: +```certoraRun certora/conf/runFixed.conf``` + +https://prover.certora.com/output/40726/a90ecf39cd7a44d59b30ff8a6172e8ff/?anonymousKey=cac7192076ce98c8465b939d2ac2001385a484ff diff --git a/DEFI/CPP_mini/certora/conf/runBroken.conf b/DEFI/CPP_mini/certora/conf/runBroken.conf new file mode 100644 index 00000000..698f64ad --- /dev/null +++ b/DEFI/CPP_mini/certora/conf/runBroken.conf @@ -0,0 +1,16 @@ +{ + // files that are part of the scene (everything the Certora Prover can reason about) + "files": [ + "src/ConstantProductPoolMini.sol:ConstantProductPool", + "certora/helpers/DummyERC20A.sol", + "certora/helpers/DummyERC20B.sol" + ], + // the main contract under test and the spec file + "verify": "ConstantProductPool:certora/spec/CPPMini.spec", + // After unrolling loops, assume the loop halt conditions hold: https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops + "optimistic_loop": true, + // msg to recognize this run (presented in your list of jobs under prover.certora.com) + "msg": "ConstantProductPool with bugs", + // Check the rule is non-vacuous + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/DEFI/CPP_mini/certora/conf/runFixed.conf b/DEFI/CPP_mini/certora/conf/runFixed.conf new file mode 100644 index 00000000..0c2f30a5 --- /dev/null +++ b/DEFI/CPP_mini/certora/conf/runFixed.conf @@ -0,0 +1,16 @@ +{ + // files that are part of the scene (everything the Certora Prover can reason about) + "files": [ + "src/ConstantProductPoolMiniFixed.sol:ConstantProductPool", + "certora/helpers/DummyERC20A.sol", + "certora/helpers/DummyERC20B.sol" + ], + // the main contract under test and the spec file + "verify": "ConstantProductPool:certora/spec/CPPMini.spec", + // After unrolling loops, assume the loop halt conditions hold: https://docs.certora.com/en/latest/docs/prover/cli/options.html#options-regarding-source-code-loops + "optimistic_loop": true, + // msg to recognize this run (presented in your list of jobs under prover.certora.com) + "msg": "ConstantProductPool Fixed", + // Check the rule is non-vacuous + "rule_sanity": "basic" +} \ No newline at end of file diff --git a/DEFI/CPP_mini/certora/helpers/DummyERC20A.sol b/DEFI/CPP_mini/certora/helpers/DummyERC20A.sol new file mode 100644 index 00000000..79b5e608 --- /dev/null +++ b/DEFI/CPP_mini/certora/helpers/DummyERC20A.sol @@ -0,0 +1,14 @@ +// Represents a symbolic/dummy ERC20 token + +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +import "../../src/ERC20.sol"; + +contract DummyERC20A is ERC20 { + + string public name = "ERC20A"; + function mint(address account, uint256 amount) external { + _mint(account,amount); + } +} \ No newline at end of file diff --git a/DEFI/CPP_mini/certora/helpers/DummyERC20B.sol b/DEFI/CPP_mini/certora/helpers/DummyERC20B.sol new file mode 100644 index 00000000..f4b1a4e2 --- /dev/null +++ b/DEFI/CPP_mini/certora/helpers/DummyERC20B.sol @@ -0,0 +1,13 @@ +// Represents a symbolic/dummy ERC20 token + +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +import "../../src/ERC20.sol"; + +contract DummyERC20B is ERC20 { + string public name = "ERC20B"; + function mint(address account, uint256 amount) external { + _mint(account,amount); + } +} \ No newline at end of file diff --git a/DEFI/CPP_mini/certora/spec/CPPMini.spec b/DEFI/CPP_mini/certora/spec/CPPMini.spec new file mode 100644 index 00000000..ca74afe4 --- /dev/null +++ b/DEFI/CPP_mini/certora/spec/CPPMini.spec @@ -0,0 +1,109 @@ +/*** +This example demonstrate a critical bug found with the Certora Prover +***/ + +// reference from the spec to additional contracts used in the verification +using DummyERC20A as _token0; +using DummyERC20B as _token1; +using ConstantProductPool as _pool; + + +/* + Declaration of methods that are used in the rules. `envfree` indicates that + the method is not dependent on the environment (`msg.value`, `msg.sender`). + Methods that are not declared here are assumed to be dependent on the + environment. +*/ + +methods{ + function token0() external returns (address) envfree; + function token1() external returns (address) envfree; + function allowance(address,address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; + + function DummyERC20A.balanceOf(address) external returns (uint256) envfree; + function DummyERC20B.balanceOf(address) external returns (uint256) envfree; + function DummyERC20A.allowance(address,address) external returns (uint256) envfree; + function DummyERC20B.allowance(address,address) external returns (uint256) envfree; + //external calls to be resolved by dispatcher - taking into account all available implementations + function _.transfer(address recipient, uint256 amount) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + // mathematical summary + function Math.sqrt(uint256 y) internal returns (uint256) => floorSqrt(y); + +} + + +// A precise summarization of sqrt +ghost floorSqrt(uint256) returns uint256 { + // sqrt(x)^2 <= x + axiom forall uint256 x. floorSqrt(x)*floorSqrt(x) <= to_mathint(x) && + // sqrt(x+1)^2 > x + (floorSqrt(x) + 1)*(floorSqrt(x) + 1) > to_mathint(x); +} + +// a cvl function for precondition assumptions +function setup(env e){ + address zero_address = 0; + uint256 MINIMUM_LIQUIDITY = 1000; + require totalSupply() == 0 || currentContract._balances[zero_address] == MINIMUM_LIQUIDITY; + require currentContract._balances[zero_address] + currentContract._balances[e.msg.sender] <= totalSupply(); + require _token0 == token0(); + require _token1 == token1(); + require e.msg.sender != currentContract; +} + +invariant allowanceOfPoolAlwaysZero(address a) + _token0.allowance(_pool, a) == 0 && _token1.allowance(_pool, a) == 0 + { + preserved with (env e){ + setup(e); + } + } + + +/* +Property: For both token0 and token1 the balance of the system is at least as much as the reserves. + +This property is implemented as an invariant. +Invariants are defined as a specification of a condition that should always be true once an operation is concluded. +In addition, the invariant also checks that it holds immediately after the constructor of the code runs. + +*/ + +invariant balanceGreaterThanReserve() + (currentContract.reserve0 <= _token0.balanceOf(currentContract))&& + (currentContract.reserve1 <= _token1.balanceOf(currentContract)) + { + preserved with (env e){ + setup(e); + requireInvariant allowanceOfPoolAlwaysZero(e.msg.sender); + } + + + } + + +/* +Property: Integrity of totalSupply with respect to the amount of reserves. + +This is a high level property of the system - the ability to pay back liquidity providers. +If there are any LP tokens (the totalSupply is greater than 0), then neither reserves0 nor reserves1 should ever be zero (otherwise the pool could not produce the underlying tokens). + +This invariant catches the original bug in Trident where the amount to receive is computed as a function of the balances and not the reserves. + +Formula: + (totalSupply() == 0 <=> getReserve0() == 0) && + (totalSupply() == 0 <=> getReserve1() == 0) +*/ + +invariant integrityOfTotalSupply() + + (totalSupply() == 0 <=> currentContract.reserve0 == 0) && + (totalSupply() == 0 <=> currentContract.reserve1 == 0) + { + preserved with (env e){ + requireInvariant balanceGreaterThanReserve(); + setup(e); + } + } diff --git a/DEFI/CPP_mini/foundry.toml b/DEFI/CPP_mini/foundry.toml new file mode 100644 index 00000000..be0a80db --- /dev/null +++ b/DEFI/CPP_mini/foundry.toml @@ -0,0 +1,8 @@ +[profile.default] +src = "src" +out = "out" +libs = ["lib"] +[fuzz] +runs = 10000 + +# See more config options https://github.com/foundry-rs/foundry/blob/master/crates/config/README.md#all-options diff --git a/DEFI/CPP_mini/src/ConstantProductPoolMini.sol b/DEFI/CPP_mini/src/ConstantProductPoolMini.sol new file mode 100644 index 00000000..a025fea0 --- /dev/null +++ b/DEFI/CPP_mini/src/ConstantProductPoolMini.sol @@ -0,0 +1,196 @@ +/* +The following system is based on a simplified version of the Trident bug that was found by the Certora Prover. +You can find a brief explanation about the original system and bug here: +https://medium.com/certora/exploiting-an-invariant-break-how-we-found-a-pool-draining-bug-in-sushiswaps-trident-585bd98a4d4f + +*/ + + +pragma solidity ^0.8.0; +import "./ERC20.sol"; + +import {Math} from "./Math.sol"; + +/* +In constant-product pools, 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)ᵖᵒˢᵗ +where reserves0 and reserves1 are the amount of token0 and token1 the system holds. + +On first liquidity deposit, the system transfers 1000 LP tokens to address 0 to ensure the pool cannot be emptied. +*/ + +contract ConstantProductPool is ERC20 { + uint256 internal constant MINIMUM_LIQUIDITY = 1000; + address public token0; + address public token1; + uint256 internal reserve0; + uint256 internal reserve1; + uint256 public kLast; + + uint256 locked; + + modifier lock() { + require(locked == 1, "LOCKED"); + locked = 2; + _; + locked = 1; + } + + constructor(address _token0, address _token1) { + token0 = _token0; + token1 = _token1; + locked = 1; + } + + // Mints LP tokens + function mint() public lock returns (uint256 liquidity) { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 _balance0, uint256 _balance1) = _getBalances(); + + uint256 computed = Math.sqrt(_balance0 * _balance1); + uint256 amount0 = _balance0 - _reserve0; + uint256 amount1 = _balance1 - _reserve1; + + uint256 _totalSupply = totalSupply(); + uint256 k = kLast; + if (_totalSupply == 0) { + require (amount0 != 0 && amount1 != 0, "InvalidAmounts"); + liquidity = computed - MINIMUM_LIQUIDITY; + _mint(address(0), MINIMUM_LIQUIDITY); + } else { + uint256 kIncrease; + unchecked { + kIncrease = computed - k; + } + liquidity = (kIncrease * _totalSupply) / k; + } + require (liquidity != 0, "InsufficientLiquidityMinted"); + _mint(msg.sender, liquidity); + _update(_balance0, _balance1); + kLast = computed; + + } + + // Burns LP tokens and swaps one of the output tokens for another + // The user receives amountOut in tokenOut + function burnSingle(bool token1Out, uint256 liquidity) + public + lock + returns (uint256 amountOut) + { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 balance0, uint256 balance1) = _getBalances(); + uint256 _totalSupply = totalSupply(); + + uint256 amount0 = (liquidity * balance0 ) / _totalSupply; + uint256 amount1 = (liquidity * balance1 ) / _totalSupply; + + _burn( msg.sender, liquidity); + if (token1Out) { + amount1 += _getAmountOut( + amount0, + _reserve0 - amount0, + _reserve1 - amount1 + ); + + transfer(msg.sender, token1, amount1); + balance1 -= amount1; + amountOut = amount1; + amount0 = 0; + } else { + amount0 += _getAmountOut( + amount1, + _reserve1 - amount1, + _reserve0 - amount0 + ); + transfer(msg.sender, token0, amount0); + balance0 -= amount0; + amountOut = amount0; + amount1 = 0; + } + _update(balance0, balance1); + } + + // Swaps one token for another + function swap(bool token0Out) + public + lock + returns (uint256 amountOut) + { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 balance0, uint256 balance1) = _getBalances(); + require(_reserve0 > 0); + uint256 amountIn; + address tokenOut; + if (token0Out) { + tokenOut = token1; + amountIn = balance0 - _reserve0; + amountOut = _getAmountOut(amountIn, _reserve0, _reserve1); + balance1 -= amountOut; + } else { + tokenOut = token0; + amountIn = balance1 - _reserve1; + amountOut = _getAmountOut(amountIn, _reserve1, _reserve0); + balance0 -= amountOut; + } + transfer(msg.sender, tokenOut, amountOut); + _update(balance0, balance1); + } + + function transfer( + address to, + address token, + uint256 amount + ) internal { + bool success = ERC20(token).transfer(to, amount); + require(success, "TRANSFER FAILED"); + } + + function _update( + uint256 balance0, + uint256 balance1 + ) internal { + reserve0 = balance0; + reserve1 = balance1; + } + + function getReserve0() public view returns (uint256) { + return reserve0; + } + + function getReserve1() public view returns (uint256) { + return reserve1; + } + + function _getAmountOut( + uint256 amountIn, + uint256 reserveAmountIn, + uint256 reserveAmountOut + ) public pure returns (uint256 amountOut) { + amountOut = + (amountIn * reserveAmountOut) / + (reserveAmountIn + amountIn); + } + + function _getReserves() + internal + view + returns (uint256 _reserve0, uint256 _reserve1) + { + _reserve0 = reserve0; + _reserve1 = reserve1; + } + + function _getBalances() + internal + view + returns (uint256 _balance0, uint256 _balance1) + { + _balance0 = ERC20(token0).balanceOf(address(this)); + _balance1 = ERC20(token1).balanceOf(address(this)); + } +} + diff --git a/DEFI/CPP_mini/src/ConstantProductPoolMiniFixed.sol b/DEFI/CPP_mini/src/ConstantProductPoolMiniFixed.sol new file mode 100644 index 00000000..b9a44523 --- /dev/null +++ b/DEFI/CPP_mini/src/ConstantProductPoolMiniFixed.sol @@ -0,0 +1,197 @@ +/* +The following system is based on a simplified version of the Trident bug that was found by the Certora Prover. +You can find a brief explanation about the original system and bug here: +https://medium.com/certora/exploiting-an-invariant-break-how-we-found-a-pool-draining-bug-in-sushiswaps-trident-585bd98a4d4f + +*/ + + +pragma solidity ^0.8.0; +import "./ERC20.sol"; + +import {Math} from "./Math.sol"; + +/* +In constant-product pools, 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)ᵖᵒˢᵗ +where reserves0 and reserves1 are the amount of token0 and token1 the system holds. + +On first liquidity deposit, the system transfers 1000 LP tokens to address 0 to ensure the pool cannot be emptied. +*/ + +contract ConstantProductPool is ERC20 { + uint256 internal constant MINIMUM_LIQUIDITY = 10; + address public token0; + address public token1; + uint256 internal reserve0; + uint256 internal reserve1; + uint256 public kLast; + + uint256 locked; + + modifier lock() { + require(locked == 1, "LOCKED"); + locked = 2; + _; + locked = 1; + } + + constructor(address _token0, address _token1) { + token0 = _token0; + token1 = _token1; + locked = 1; + } + + // Mints LP tokens + function mint() public lock returns (uint256 liquidity) { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 _balance0, uint256 _balance1) = _getBalances(); + + uint256 computed = Math.sqrt(_balance0 * _balance1); + uint256 amount0 = _balance0 - _reserve0; + uint256 amount1 = _balance1 - _reserve1; + + uint256 _totalSupply = totalSupply(); + uint256 k = kLast; + if (_totalSupply == 0) { + require (amount0 != 0 && amount1 != 0, "InvalidAmounts"); + liquidity = computed - MINIMUM_LIQUIDITY; + _mint(address(0), MINIMUM_LIQUIDITY); + } else { + uint256 kIncrease; + unchecked { + kIncrease = computed - k; + } + liquidity = (kIncrease * _totalSupply) / k; + } + require (liquidity != 0, "InsufficientLiquidityMinted"); + _mint(msg.sender, liquidity); + _update(_balance0, _balance1); + kLast = computed; + + } + + // Burns LP tokens and swaps one of the output tokens for another + // The user receives amountOut in tokenOut + function burnSingle(bool token1Out, uint256 liquidity) + public + lock + returns (uint256 amountOut) + { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 balance0, uint256 balance1) = _getBalances(); + uint256 _totalSupply = totalSupply(); + + /* Fix bug - computation as part of reverse and not the external balance */ + uint256 amount0 = (liquidity * _reserve0 ) / _totalSupply; + uint256 amount1 = (liquidity * _reserve1 ) / _totalSupply; + + _burn( msg.sender, liquidity); + if (token1Out) { + amount1 += _getAmountOut( + amount0, + _reserve0 - amount0, + _reserve1 - amount1 + ); + + transfer(msg.sender, token1, amount1); + balance1 -= amount1; + amountOut = amount1; + amount0 = 0; + } else { + amount0 += _getAmountOut( + amount1, + _reserve1 - amount1, + _reserve0 - amount0 + ); + transfer(msg.sender, token0, amount0); + balance0 -= amount0; + amountOut = amount0; + amount1 = 0; + } + _update(balance0, balance1); + } + + // Swaps one token for another + function swap(bool token0Out) + public + lock + returns (uint256 amountOut) + { + (uint256 _reserve0, uint256 _reserve1) = _getReserves(); + (uint256 balance0, uint256 balance1) = _getBalances(); + require(_reserve0 > 0); + uint256 amountIn; + address tokenOut; + if (token0Out) { + tokenOut = token1; + amountIn = balance0 - _reserve0; + amountOut = _getAmountOut(amountIn, _reserve0, _reserve1); + balance1 -= amountOut; + } else { + tokenOut = token0; + amountIn = balance1 - _reserve1; + amountOut = _getAmountOut(amountIn, _reserve1, _reserve0); + balance0 -= amountOut; + } + transfer(msg.sender, tokenOut, amountOut); + _update(balance0, balance1); + } + + function transfer( + address to, + address token, + uint256 amount + ) internal { + bool success = ERC20(token).transfer(to, amount); + require(success, "TRANSFER FAILED"); + } + + function _update( + uint256 balance0, + uint256 balance1 + ) internal { + reserve0 = balance0; + reserve1 = balance1; + } + + function getReserve0() public view returns (uint256) { + return reserve0; + } + + function getReserve1() public view returns (uint256) { + return reserve1; + } + + function _getAmountOut( + uint256 amountIn, + uint256 reserveAmountIn, + uint256 reserveAmountOut + ) public pure returns (uint256 amountOut) { + amountOut = + (amountIn * reserveAmountOut) / + (reserveAmountIn + amountIn); + } + + function _getReserves() + internal + view + returns (uint256 _reserve0, uint256 _reserve1) + { + _reserve0 = reserve0; + _reserve1 = reserve1; + } + + function _getBalances() + internal + view + returns (uint256 _balance0, uint256 _balance1) + { + _balance0 = ERC20(token0).balanceOf(address(this)); + _balance1 = ERC20(token1).balanceOf(address(this)); + } +} + diff --git a/DEFI/CPP_mini/src/ERC20.sol b/DEFI/CPP_mini/src/ERC20.sol new file mode 100644 index 00000000..516395cc --- /dev/null +++ b/DEFI/CPP_mini/src/ERC20.sol @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: MIT +// OpenZeppelin Contracts v4.4.1 (token/ERC20/ERC20.sol) + +pragma solidity ^0.8.0; + +abstract contract Context { + function _msgSender() internal view virtual returns (address) { + return msg.sender; + } + + function _msgData() internal view virtual returns (bytes calldata) { + return msg.data; + } +} + +/** + * @dev Implementation of the {IERC20} interface. + * + * This implementation is agnostic to the way tokens are created. This means + * that a supply mechanism has to be added in a derived contract using {_mint}. + * For a generic mechanism see {ERC20PresetMinterPauser}. + * + * TIP: For a detailed writeup see our guide + * https://forum.zeppelin.solutions/t/how-to-implement-erc20-supply-mechanisms/226[How + * to implement supply mechanisms]. + * + * We have followed general OpenZeppelin Contracts guidelines: functions revert + * instead returning `false` on failure. This behavior is nonetheless + * conventional and does not conflict with the expectations of ERC20 + * applications. + * + * Additionally, an {Approval} event is emitted on calls to {transferFrom}. + * This allows applications to reconstruct the allowance for all accounts just + * by listening to said events. Other implementations of the EIP may not emit + * these events, as it isn't required by the specification. + * + * Finally, the non-standard {decreaseAllowance} and {increaseAllowance} + * functions have been added to mitigate the well-known issues around setting + * allowances. See {IERC20-approve}. + */ +contract ERC20 is Context { + mapping(address => uint256) internal _balances; + + mapping(address => mapping(address => uint256)) internal _allowances; + + uint256 internal _totalSupply; + + + function decimals() public view virtual returns (uint8) { + return 18; + } + + function totalSupply() public view virtual returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view virtual returns (uint256) { + return _balances[account]; + } + + + function transfer(address recipient, uint256 amount) public virtual returns (bool) { + _transfer(_msgSender(), recipient, amount); + return true; + } + + function allowance(address owner, address spender) public view virtual returns (uint256) { + return _allowances[owner][spender]; + } + + + function approve(address spender, uint256 amount) public virtual returns (bool) { + _approve(_msgSender(), spender, amount); + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) public virtual returns (bool) { + uint256 currentAllowance = _allowances[sender][_msgSender()]; + if (currentAllowance != type(uint256).max) { + require(currentAllowance >= amount, "ERC20: transfer amount exceeds allowance"); + _approve(sender, _msgSender(), currentAllowance - amount); + } + + _transfer(sender, recipient, amount); + + return true; + } + + function increaseAllowance(address spender, uint256 addedValue) public virtual returns (bool) { + _approve(_msgSender(), spender, _allowances[_msgSender()][spender] + addedValue); + return true; + } + + function decreaseAllowance(address spender, uint256 subtractedValue) public virtual returns (bool) { + uint256 currentAllowance = _allowances[_msgSender()][spender]; + require(currentAllowance >= subtractedValue, "ERC20: decreased allowance below zero"); + _approve(_msgSender(), spender, currentAllowance - subtractedValue); + + + return true; + } + + function _transfer( + address sender, + address recipient, + uint256 amount + ) internal virtual { + require(sender != address(0), "ERC20: transfer from the zero address"); + require(recipient != address(0), "ERC20: transfer to the zero address"); + + uint256 senderBalance = _balances[sender]; + require(senderBalance >= amount, "ERC20: transfer amount exceeds balance"); + _balances[sender] = senderBalance - amount; + _balances[recipient] += amount; + + } + + + function _mint(address account, uint256 amount) internal virtual { + _totalSupply += amount; + _balances[account] += amount; + + } + + + function _burn(address account, uint256 amount) internal virtual { + require(account != address(0), "ERC20: burn from the zero address"); + + uint256 accountBalance = _balances[account]; + require(accountBalance >= amount, "ERC20: burn amount exceeds balance"); + _balances[account] = accountBalance - amount; + _totalSupply -= amount; + + } + + function _approve( + address owner, + address spender, + uint256 amount + ) internal virtual { + require(owner != address(0), "ERC20: approve from the zero address"); + require(spender != address(0), "ERC20: approve to the zero address"); + + _allowances[owner][spender] = amount; + } + +} \ No newline at end of file diff --git a/DEFI/CPP_mini/src/Math.sol b/DEFI/CPP_mini/src/Math.sol new file mode 100644 index 00000000..69be2a0b --- /dev/null +++ b/DEFI/CPP_mini/src/Math.sol @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: GPL-3.0-or-later + +pragma solidity >=0.8.0; + +/// @notice Trident sqrt helper library. +library Math { + /// @dev Modified from Solmate (https://github.com/Rari-Capital/solmate/blob/main/src/utils/FixedPointMathLib.sol) + function sqrt(uint256 x) internal pure returns (uint256 z) { + assembly { + // This segment is to get a reasonable initial estimate for the Babylonian method. + // If the initial estimate is bad, the number of correct bits increases ~linearly + // each iteration instead of ~quadratically. + // The idea is to get z*z*y within a small factor of x. + // More iterations here gets y in a tighter range. Currently, we will have + // y in [256, 256*2^16). We ensure y>= 256 so that the relative difference + // between y and y+1 is small. If x < 256 this is not possible, but those cases + // are easy enough to verify exhaustively. + z := 181 // The 'correct' value is 1, but this saves a multiply later + let y := x + // Note that we check y>= 2^(k + 8) but shift right by k bits each branch, + // this is to ensure that if x >= 256, then y >= 256. + if iszero(lt(y, 0x10000000000000000000000000000000000)) { + y := shr(128, y) + z := shl(64, z) + } + if iszero(lt(y, 0x1000000000000000000)) { + y := shr(64, y) + z := shl(32, z) + } + if iszero(lt(y, 0x10000000000)) { + y := shr(32, y) + z := shl(16, z) + } + if iszero(lt(y, 0x1000000)) { + y := shr(16, y) + z := shl(8, z) + } + // Now, z*z*y <= x < z*z*(y+1), and y <= 2^(16+8), + // and either y >= 256, or x < 256. + // Correctness can be checked exhaustively for x < 256, so we assume y >= 256. + // Then z*sqrt(y) is within sqrt(257)/sqrt(256) of sqrt(x), or about 20bps. + + // For s in the range [1/256, 256], the estimate f(s) = (181/1024) * (s+1) + // is in the range (1/2.84 * sqrt(s), 2.84 * sqrt(s)), with largest error when s=1 + // and when s = 256 or 1/256. Since y is in [256, 256*2^16), let a = y/65536, so + // that a is in [1/256, 256). Then we can estimate sqrt(y) as + // sqrt(65536) * 181/1024 * (a + 1) = 181/4 * (y + 65536)/65536 = 181 * (y + 65536)/2^18 + // There is no overflow risk here since y < 2^136 after the first branch above. + z := shr(18, mul(z, add(y, 65536))) // A multiply is saved from the initial z := 181 + + // Given the worst case multiplicative error of 2.84 above, 7 iterations should be enough. + // Possibly with a quadratic/cubic polynomial above we could get 4-6. + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + z := shr(1, add(z, div(x, z))) + + // See https://en.wikipedia.org/wiki/Integer_square_root#Using_only_integer_division. + // If x+1 is a perfect square, the Babylonian method cycles between + // floor(sqrt(x)) and ceil(sqrt(x)). This check ensures we return floor. + // Since this case is rare, we choose to save gas on the assignment and + // repeat division in the rare case. + // If you don't care whether floor or ceil is returned, you can skip this. + if lt(div(x, z), z) { + z := div(x, z) + } + } + } +} \ No newline at end of file diff --git a/DEFI/CPP_mini/test/CPPMini.t.sol b/DEFI/CPP_mini/test/CPPMini.t.sol new file mode 100644 index 00000000..63fe7dfe --- /dev/null +++ b/DEFI/CPP_mini/test/CPPMini.t.sol @@ -0,0 +1,87 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity ^0.8.13; + +import {Test, console} from "forge-std/Test.sol"; +import {ERC20} from "../src/ERC20.sol"; +import {DummyERC20A} from "../certora/helpers/DummyERC20A.sol"; +import {DummyERC20B} from "../certora/helpers/DummyERC20B.sol"; +import {CPPSetup} from "./CPPSetup.sol"; + +contract CPPMiniTest is Test { + CPPSetup public cpp; + DummyERC20A public token0; + DummyERC20B public token1; + + uint256 private constant START_TOKENS = 1000e18; + + address[] users; + address private Alice = address(0x2); + address private Bob = address(0x1); + function setUp() public { + token0 = new DummyERC20A(); + token1 = new DummyERC20B(); + cpp = new CPPSetup(address(token0), address(token1)); + + + users.push(Alice); + users.push(Bob); + + for(uint256 i; i Date: Wed, 26 Mar 2025 23:28:19 +0200 Subject: [PATCH 2/6] submodule, fix invariant --- .gitmodules | 3 +++ DEFI/CPP_mini/lib/forge-std | 1 + DEFI/CPP_mini/test/CPPMini.t.sol | 4 +++- 3 files changed, 7 insertions(+), 1 deletion(-) create mode 160000 DEFI/CPP_mini/lib/forge-std diff --git a/.gitmodules b/.gitmodules index e69de29b..6165d77a 100644 --- a/.gitmodules +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "DEFI/CPP_mini/lib/forge-std"] + path = DEFI/CPP_mini/lib/forge-std + url = git@github.com:foundry-rs/forge-std.git diff --git a/DEFI/CPP_mini/lib/forge-std b/DEFI/CPP_mini/lib/forge-std new file mode 160000 index 00000000..6853b9ec --- /dev/null +++ b/DEFI/CPP_mini/lib/forge-std @@ -0,0 +1 @@ +Subproject commit 6853b9ec7df5dc0c213b05ae67785ad4f4baa0ea diff --git a/DEFI/CPP_mini/test/CPPMini.t.sol b/DEFI/CPP_mini/test/CPPMini.t.sol index 63fe7dfe..7e12a086 100644 --- a/DEFI/CPP_mini/test/CPPMini.t.sol +++ b/DEFI/CPP_mini/test/CPPMini.t.sol @@ -82,6 +82,8 @@ contract CPPMiniTest is Test { function invariant_reserve() public view { uint256 reserve0 = cpp.getReserve0(); uint256 reserve1 = cpp.getReserve1(); - assertEq(reserve0 == 0 , reserve1 == 0); + uint256 totalSupply = cpp.totalSupply(); + assertEq(reserve0 == 0 , totalSupply == 0); + assertEq(reserve1 == 0 , totalSupply == 0); } } From 26a69e747955850664884a2942d6bdcff617a64b Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Sun, 30 Mar 2025 09:45:20 +0300 Subject: [PATCH 3/6] Update DEFI/CPP_mini/README.md Co-authored-by: shellygr --- DEFI/CPP_mini/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DEFI/CPP_mini/README.md b/DEFI/CPP_mini/README.md index 6d4fbdae..d24f4c1f 100644 --- a/DEFI/CPP_mini/README.md +++ b/DEFI/CPP_mini/README.md @@ -24,7 +24,7 @@ forge coverage --report lcov --report-file fuzz --match-contract CPPMini genhtml fuzz -o fuzzcov open fuzzcov/index.html ``` -Coverage is very good - 96.3% however bug is missed. +Coverage is very good - 96.3%, however the bug is missed. The bug is demonstrated in a manual crafted test `test_manual()` and shows how it can cause a complete drain of the protocol. From b3044f28d740bc8d459138468276ee703302c460 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Sun, 30 Mar 2025 09:45:49 +0300 Subject: [PATCH 4/6] Update DEFI/CPP_mini/README.md Co-authored-by: shellygr --- DEFI/CPP_mini/README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/DEFI/CPP_mini/README.md b/DEFI/CPP_mini/README.md index d24f4c1f..dc79339a 100644 --- a/DEFI/CPP_mini/README.md +++ b/DEFI/CPP_mini/README.md @@ -35,7 +35,6 @@ To run the verification: As seen in the report: https://prover.certora.com/output/40726/4ba34bd0d7d54c279c7cb261d1616fef/?anonymousKey=626461dda2213599b57007646d3198b21c249908 -The property is violated Once the bug is fixed the property is verified: ```certoraRun certora/conf/runFixed.conf``` From 80f2346063563bbde608051790aac6f24f8d68c9 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Sun, 30 Mar 2025 09:45:58 +0300 Subject: [PATCH 5/6] Update DEFI/CPP_mini/README.md Co-authored-by: shellygr --- DEFI/CPP_mini/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DEFI/CPP_mini/README.md b/DEFI/CPP_mini/README.md index dc79339a..93da1af6 100644 --- a/DEFI/CPP_mini/README.md +++ b/DEFI/CPP_mini/README.md @@ -33,7 +33,7 @@ The bug is demonstrated in a manual crafted test `test_manual()` and shows how i To run the verification: ```certoraRun certora/conf/runBroken.conf``` -As seen in the report: https://prover.certora.com/output/40726/4ba34bd0d7d54c279c7cb261d1616fef/?anonymousKey=626461dda2213599b57007646d3198b21c249908 +As seen in the report, the property is violated: https://prover.certora.com/output/40726/4ba34bd0d7d54c279c7cb261d1616fef/?anonymousKey=626461dda2213599b57007646d3198b21c249908 Once the bug is fixed the property is verified: From a0fa39a45e4b4bd5653dae101734620cc3000040 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Sun, 30 Mar 2025 17:16:06 +0300 Subject: [PATCH 6/6] clean foundry test --- DEFI/CPP_mini/certora/spec/CPPMini.spec | 3 +- DEFI/CPP_mini/test/CPPMini.t.sol | 74 ++++++++++++++++++------- 2 files changed, 56 insertions(+), 21 deletions(-) diff --git a/DEFI/CPP_mini/certora/spec/CPPMini.spec b/DEFI/CPP_mini/certora/spec/CPPMini.spec index ca74afe4..58861513 100644 --- a/DEFI/CPP_mini/certora/spec/CPPMini.spec +++ b/DEFI/CPP_mini/certora/spec/CPPMini.spec @@ -93,8 +93,7 @@ If there are any LP tokens (the totalSupply is greater than 0), then neither res This invariant catches the original bug in Trident where the amount to receive is computed as a function of the balances and not the reserves. Formula: - (totalSupply() == 0 <=> getReserve0() == 0) && - (totalSupply() == 0 <=> getReserve1() == 0) + (totalSupply() == 0 <=> getReserve0() == 0 <=> getReserve1() == 0) */ invariant integrityOfTotalSupply() diff --git a/DEFI/CPP_mini/test/CPPMini.t.sol b/DEFI/CPP_mini/test/CPPMini.t.sol index 7e12a086..fb20b5ee 100644 --- a/DEFI/CPP_mini/test/CPPMini.t.sol +++ b/DEFI/CPP_mini/test/CPPMini.t.sol @@ -47,23 +47,49 @@ contract CPPMiniTest is Test { targetSender(Bob); } - function test_manual() public { +/*** @title fuzz test the invariant + Check for the invariant that reserve0 is 0 iff reserve1 is 0 and iff totalSupply is 0. + + This did not find the bug even after 100k runs. + */ + function invariant_integrityOfTotalSupply() public view { + uint256 reserve0 = cpp.getReserve0(); + uint256 reserve1 = cpp.getReserve1(); + uint256 totalSupply = cpp.totalSupply(); + assertEq(reserve0 == 0 , totalSupply == 0); + assertEq(reserve1 == 0 , totalSupply == 0); + } + + +/*** @title Manual show the violation + Only a specific computed value can cause the violation + + run command: forge test --match-test test_manual_bug -vvv + */ + + function test_manual_bug() public { vm.startPrank(Alice); cpp.transferAndMint(20,200); uint256 liquidity = cpp.balanceOf(Alice); uint256 _reserve0 = cpp.getReserve0(); uint256 _totalSupply = cpp.totalSupply(); - uint256 _actualB0 = token0.balanceOf(address(cpp)); - uint256 _actualB1 = token1.balanceOf(address(cpp)); + /* - we need _reserve0 == amount0 + we need _reserve0 == amount0 at the call to: + + amount1 += _getAmountOut( + amount0, + _reserve0 - amount0, + _reserve1 - amount1 + ); + + amount0 === (liquidity * balance0 ) / _totalSupply _reserve0 === (liquidity * balance0 ) / _totalSupply - - simple math we can compute it backwards + simple math we can compute the required balance0: + */ - uint256 balanceForBug = _reserve0 * _totalSupply /liquidity + 1; uint256 amountToTransfer = balanceForBug - _reserve0 ; @@ -71,19 +97,29 @@ contract CPPMiniTest is Test { cpp.burnSingle(true, liquidity); // now that we have one reserve 0 the invariant fails - // invariant_reserve(); // comment this out to see how critical is this bug - // but we can just continue to drain the protocol - cpp.transferAndSwap(false, 1); - _actualB0 = token0.balanceOf(address(cpp)); - _actualB1 = token0.balanceOf(address(cpp)); - console.log(_actualB0, _actualB1); + invariant_integrityOfTotalSupply(); } - function invariant_reserve() public view { - uint256 reserve0 = cpp.getReserve0(); - uint256 reserve1 = cpp.getReserve1(); - uint256 totalSupply = cpp.totalSupply(); - assertEq(reserve0 == 0 , totalSupply == 0); - assertEq(reserve1 == 0 , totalSupply == 0); +/*** + @title Critical bug demonstration + Once the invariant is broken, one can swap the entire reserve for just one token + run command: forge test --match-test test_manual_continue_to_drain -vvv + */ + function test_manual_continue_to_drain() public { + vm.startPrank(Alice); + cpp.transferAndMint(20,200); + uint256 liquidity = cpp.balanceOf(Alice); + uint256 _reserve0 = cpp.getReserve0(); + uint256 _totalSupply = cpp.totalSupply(); + uint256 balanceForBug = _reserve0 * _totalSupply /liquidity + 1; + uint256 amountToTransfer = balanceForBug - _reserve0 ; + + cpp.externalTransfer(amountToTransfer, 0); + cpp.burnSingle(true, liquidity); + + // lets continue to drain the protocol + cpp.transferAndSwap(false, 1); + console.log(token0.balanceOf(address(cpp)), token1.balanceOf(address(cpp)), cpp.totalSupply()); } + }