diff --git a/Audit.md b/Audit.md deleted file mode 100644 index b3239b49..00000000 --- a/Audit.md +++ /dev/null @@ -1,111 +0,0 @@ -- [Installation](#Installation) -- [Testing with Echidna](#testing-properties-with-echidna) -- [Code verification with Manticore](#Code-verification-with-Manticore) - -# Installation - -**Slither** -``` -pip3 install slither-analyzer -``` - -**Manticore** -``` -pip3 install manticore -``` - -**Echidna** -See [Echidna Installation](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna#installation). - - -``` -docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox -``` - -``` -solc-select 0.5.12 -cd /home/training -``` - - -# Testing properties with Echidna - -`slither-flat` will export the contract and translate external function to public, to faciliate writting properties: -``` -slither-flat . --convert-external -``` - -The flattened contracts are in `crytic-export/flattening`. The Echidna properties are in `echidna/`. - -## Properties - -Echidna properties can be broadly divided in two categories: general properties of the contracts that states what user can and cannot do and -specific properties based on unit tests. - -To test a property, run `echidna-test echidna/CONTRACT_file.sol CONTRACT_name --config echidna/CONTRACT_name.yaml`. - -## General Properties - -| Description | Name | Contract | Finding | Status | -| :--- | :---: | :---: | :---: | :---: | -| An attacker cannot steal assets from a public pool. | [`attacker_token_balance`](echidna/TBPoolBalance.sol#L22-L25) | [`TBPoolBalance`](echidna/TBPoolBalance.sol) |FAILED ([#193](https://github.com/balancer-labs/balancer-core/issues/193))| **Fixed** | -| An attacker cannot force the pool balance to be out-of-sync. | [`pool_record_balance`](echidna/TBPoolBalance.sol#L27-L33) | [`TBPoolBalance`](echidna/TBPoolBalance.sol)|PASSED| | -| An attacker cannot generate free pool tokens with `joinPool` (1, 2). | [`joinPool`](contracts/test/echidna/TBPoolJoinPool.sol#L7-L31) | [`TBPoolJoinPool`](contracts/test/echidna/TBPoolBalance.sol)|FAILED ([#204](https://github.com/balancer-labs/balancer-core/issues/204))| **Mitigated** | -| Calling `joinPool-exitPool` does not lead to free pool tokens (no fee) (1, 2). | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol#L34-L59) | [`TBPoolJoinExitNoFee`](contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol)|FAILED ([#205](https://github.com/balancer-labs/balancer-core/issues/205))| **Mitigated** | -| Calling `joinPool-exitPool` does not lead to free pool tokens (with fee) (1, 2). | [`joinPool`](contracts/test/echidna/TBPoolJoinExitPool.sol#L37-L62) | [`TBPoolJoinExit`](contracts/test/echidna/TBPoolJoinExitPool.sol)|FAILED ([#205](https://github.com/balancer-labs/balancer-core/issues/205))| **Mitigated** | -| Calling `exitswapExternAmountOut` does not lead to free asset (1). | [`exitswapExternAmountOut`](echidna/TBPoolExitSwap.sol#L8-L21) | [`TBPoolExitSwap`](contracts/test/echidna/TBPoolExitSwap.sol)|FAILED ([#203](https://github.com/balancer-labs/balancer-core/issues/203))| **Mitigated** | - - -(1) These properties target a specific piece of code. - -(2) These properties don't need slither-flat, and are integrated into `contracts/test/echidna/`. To test them run `echidna-test . CONTRACT_name --config ./echidna_general_config.yaml`. - -## Unit-test-based Properties - -| Description | Name | Contract | Finding | Status | -| :--- | :---: | :---: | :---: | :---: | -| If the controller calls `setController`, then the `getController()` should return the new controller. | [`controller_should_change`](echidna/TBPoolController.sol#L6-L13) | [`TBPoolController`](echidna/TBPoolController.sol)|PASSED| | -| The controller cannot be changed to a null address (`0x0`). | [`controller_cannot_be_null`](echidna/TBPoolController.sol#L15-L23) | [`TBPoolController`](echidna/TBPoolController.sol)|FAILED ([#198](https://github.com/balancer-labs/balancer-core/issues/198))| **WONT FIX** | -| The controller cannot be changed by other users. | [`no_other_user_can_change_the_controller`](echidna/TBPoolController.sol#L28-L31) | [`TBPoolController`](echidna/TBPoolController.sol)|PASSED| | -| The sum of normalized weight should be 1 if there are tokens binded. | [`valid_weights`](echidna/TBPoolLimits.sol#L35-L52) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#208](https://github.com/balancer-labs/balancer-core/issues/208)| **Mitigated** | -| The balances of all the tokens are greater or equal than `MIN_BALANCE`. | [`min_token_balance`](echidna/TBPoolLimits.sol#L65-L74) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#210](https://github.com/balancer-labs/balancer-core/issues/210)) | **WONT FIX**| -| The weight of all the tokens are less or equal than `MAX_WEIGHT`. | [`max_weight`](echidna/TBPoolLimits.sol#L76-L85) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| | -| The weight of all the tokens are greater or equal than `MIN_WEIGHT`. | [`min_weight`](echidna/TBPoolLimits.sol#L87-L96) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| | -| The swap fee is less or equal tan `MAX_FEE`. | [`min_swap_free`](echidna/TBPoolLimits.sol#L99-L102) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| | -| The swap fee is greater or equal than `MIN_FEE`. | [`max_swap_free`](echidna/TBPoolLimits.sol#L104-L107) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |PASSED| | -| An user can only swap in less than 50% of the current balance of tokenIn for a given pool. | [`max_swapExactAmountIn`](echidna/TBPoolLimits.sol#L134-L156) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#212](https://github.com/balancer-labs/balancer-core/issues/212))| **Fixed** | -| An user can only swap out less than 33.33% of the current balance of tokenOut for a given pool. | [`max_swapExactAmountOut`](echidna/TBPoolLimits.sol#L109-L132) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |FAILED ([#212](https://github.com/balancer-labs/balancer-core/issues/212))| **Fixed** | -| If a token is bounded, the `getSpotPrice` should never revert. | [`getSpotPrice_no_revert`](echidna/TBPoolNoRevert.sol#L34-L44) | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| | -| If a token is bounded, the `getSpotPriceSansFee` should never revert. | [`getSpotPriceSansFee_no_revert`](echidna/TBPoolNoRevert.sol#L46-L56) | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| | -| Calling `swapExactAmountIn` with a small value of the same token should never revert. | [`swapExactAmountIn_no_revert`](echidna/TBPoolNoRevert.sol#L58-L77) | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| | -| Calling `swapExactAmountOut` with a small value of the same token should never revert. | [`swapExactAmountOut_no_revert`](echidna/TBPoolNoRevert.sol#L79-L99) | [`TBPoolNoRevert`](echidna/TBPoolNoRevert.sol) |PASSED| | -| If a user joins pool and exits it with the same amount, the balances should keep constant. | [`joinPool_exitPool_balance_consistency`](echidna/TBPoolJoinExit.sol#L48-L97) | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |PASSED| | -| If a user joins pool and exits it with a larger amount, `exitPool` should revert. | [`impossible_joinPool_exitPool`](echidna/TBPoolJoinExit.sol#L99-L112) | [`TBPoolJoinExit`](echidna/TBPoolJoinExit.sol) |PASSED| | -| It is not possible to bind more than `MAX_BOUND_TOKENS`. | [`getNumTokens_less_or_equal_MAX_BOUND_TOKENS`](echidna/TBPoolBind.sol#L40-L43) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| It is not possible to bind more than once the same token. | [`bind_twice`](echidna/TBPoolBind.sol#L45-L54) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| It is not possible to unbind more than once the same token. | [`unbind_twice`](echidna/TBPoolBind.sol#L56-L66) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| It is always possible to unbind a token. | [`all_tokens_are_unbindable`](echidna/TBPoolBind.sol#L68-L81) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| All tokens are rebindable with valid parameters. | [`all_tokens_are_rebindable_with_valid_parameters`](echidna/TBPoolBind.sol#L83-L95) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| It is not possible to rebind an unbinded token. | [`rebind_unbinded`](echidna/TBPoolBind.sol#L97-L107) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| Only the controller can bind. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154) and [`only_controller_can_bind`](echidna/TBPoolBind.sol#L145-L148) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| If a user that is not the controller, tries to bind, rebind or unbind, the operation will revert. | [`when_bind`](echidna/TBPoolBind.sol#L150-L154), [`when_rebind`](echidna/TBPoolBind.sol#L150-L154) and [`when_unbind`](echidna/TBPoolBind.sol#L163-L168) | [`TBPoolBind`](echidna/TBPoolBind.sol) |PASSED| | -| Transfer tokens to the null address (`0x0`) causes a revert | [`transfer_to_zero`](echidna/TBTokenERC20.sol#L75-L79) and [`transferFrom_to_zero`](echidna/TBTokenERC20.sol#L85-L89) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |FAILED ([#197](https://github.com/balancer-labs/balancer-core/issues/197))| **WONT FIX** | -| The null address (`0x0`) owns no tokens | [`zero_always_empty`](echidna/TBTokenERC20.sol#L34-L36) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |FAILED| **WONT FIX** | -| Transfer a valid amout of tokens to non-null address reduces the current balance | [`transferFrom_to_other`](echidna/TBTokenERC20.sol#L108-L113) and [`transfer_to_other`](echidna/TBTokenERC20.sol#L131-L142) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | -| Transfer an invalid amout of tokens to non-null address reverts or returns false | [`transfer_to_user`](echidna/TBTokenERC20.sol#L149-L155) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | -| Self transfer a valid amout of tokens keeps the current balance constant | [`self_transferFrom`](echidna/TBTokenERC20.sol#L96-L101) and [`self_transfer`](echidna/TBTokenERC20.sol#L120-L124) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | -| Approving overwrites the previous allowance value | [`approve_overwrites`](echidna/TBTokenERC20.sol#L42-L49) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | -| The `totalSupply` is a constant | [`totalSupply_constant`](echidna/TBTokenERC20.sol#L166-L168) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | -| The balances are consistent with the `totalSupply` | [`totalSupply_balances_consistency`](echidna/TBTokenERC20.sol#L63-L65) and [`balance_less_than_totalSupply`](echidna/TBTokenERC20.sol#L55-L57) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |PASSED| | - -# Code verification with Manticore - -The following properties have equivalent Echidna property, but Manticore allows to either prove the absence of bugs, or look for an upper bound. - -To execute the script, run `python3 ./manticore/script_name.py`. - -| Description | Script | Contract | Status | -| :--- | :---: | :---: | :---: | -| An attacker cannot generate free pool tokens with `joinPool`. | [`TBPoolJoinPool.py`](manticore/TBPoolJoinPool.py)| [`TBPoolJoinPool`](manticore/contracts/TBPoolJoinPool.sol) | **FAILED** ([#204](https://github.com/balancer-labs/balancer-core/issues/204)) | -| Calling `joinPool-exitPool` does not lead to free pool tokens (no fee). | [`TBPoolJoinExitNoFee.py`](manticore/TBPoolJoinExitNoFee.py) | [`TBPoolJoinExitPoolNoFee`](manticore/contracts/TBPoolJoinExitPoolNoFee.sol) |**FAILED** ([#205](https://github.com/balancer-labs/balancer-core/issues/205)) | -| Calling `joinPool-exitPool` does not lead to free pool tokens (with fee).| [`TBPoolJoinExit.py`](manticore/TBPoolJoinExit.py) | [`TBPoolJoinExit`](manticore/contracts/TBPoolJoinExitPool.sol) |**FAILED** ([#205](https://github.com/balancer-labs/balancer-core/issues/205))| diff --git a/Trail of Bits Full Audit.pdf b/Trail of Bits Full Audit.pdf deleted file mode 100644 index b6fcff1b..00000000 Binary files a/Trail of Bits Full Audit.pdf and /dev/null differ diff --git a/echidna/BMathInternal.sol b/echidna/BMathInternal.sol deleted file mode 100644 index 4598873e..00000000 --- a/echidna/BMathInternal.sol +++ /dev/null @@ -1,445 +0,0 @@ -/* - This file is a flatenen version of BMath where all the public functions have been marked internal. - This helps Echidna to focus on some specific properties. -*/ - - - -pragma solidity 0.8.23; -contract BColor { - function getColor() - internal view - returns (bytes32); -} -contract BBronze is BColor { - function getColor() - internal view - returns (bytes32) { - return bytes32("BRONZE"); - } -} -contract BConst is BBronze { - uint internal constant BONE = 10**18; - - uint internal constant MAX_BOUND_TOKENS = 8; - uint internal constant BPOW_PRECISION = BONE / 10**10; - - uint internal constant MIN_FEE = BONE / 10**6; - uint internal constant MAX_FEE = BONE / 10; - uint internal constant EXIT_FEE = BONE / 10000; - - uint internal constant MIN_WEIGHT = BONE; - uint internal constant MAX_WEIGHT = BONE * 50; - uint internal constant MAX_TOTAL_WEIGHT = BONE * 50; - uint internal constant MIN_BALANCE = BONE / 10**12; - uint internal constant MAX_BALANCE = BONE * 10**12; - - uint internal constant MIN_POOL_SUPPLY = BONE; - - uint internal constant MIN_BPOW_BASE = 1 wei; - uint internal constant MAX_BPOW_BASE = (2 * BONE) - 1 wei; - - uint internal constant MAX_IN_RATIO = BONE / 2; - uint internal constant MAX_OUT_RATIO = (BONE / 3) + 1 wei; - -} -contract BNum is BConst { - - function btoi(uint a) - internal pure - returns (uint) - { - return a / BONE; - } - - function bfloor(uint a) - internal pure - returns (uint) - { - return btoi(a) * BONE; - } - - function badd(uint a, uint b) - internal pure - returns (uint) - { - uint c = a + b; - require(c >= a, "ERR_ADD_OVERFLOW"); - return c; - } - - function bsub(uint a, uint b) - internal pure - returns (uint) - { - (uint c, bool flag) = bsubSign(a, b); - require(!flag, "ERR_SUB_UNDERFLOW"); - return c; - } - - function bsubSign(uint a, uint b) - internal pure - returns (uint, bool) - { - if (a >= b) { - return (a - b, false); - } else { - return (b - a, true); - } - } - - function bmul(uint a, uint b) - internal pure - returns (uint) - { - uint c0 = a * b; - require(a == 0 || c0 / a == b, "ERR_MUL_OVERFLOW"); - uint c1 = c0 + (BONE / 2); - require(c1 >= c0, "ERR_MUL_OVERFLOW"); - uint c2 = c1 / BONE; - return c2; - } - - function bdiv(uint a, uint b) - internal pure - returns (uint) - { - require(b != 0, "ERR_DIV_ZERO"); - uint c0 = a * BONE; - require(a == 0 || c0 / a == BONE, "ERR_DIV_INTERNAL"); // bmul overflow - uint c1 = c0 + (b / 2); - require(c1 >= c0, "ERR_DIV_INTERNAL"); // badd require - uint c2 = c1 / b; - return c2; - } - - // DSMath.wpow - function bpowi(uint a, uint n) - internal pure - returns (uint) - { - uint z = n % 2 != 0 ? a : BONE; - - for (n /= 2; n != 0; n /= 2) { - a = bmul(a, a); - - if (n % 2 != 0) { - z = bmul(z, a); - } - } - return z; - } - - // Compute b^(e.w) by splitting it into (b^e)*(b^0.w). - // Use `bpowi` for `b^e` and `bpowK` for k iterations - // of approximation of b^0.w - function bpow(uint base, uint exp) - internal pure - returns (uint) - { - require(base >= MIN_BPOW_BASE, "ERR_BPOW_BASE_TOO_LOW"); - require(base <= MAX_BPOW_BASE, "ERR_BPOW_BASE_TOO_HIGH"); - - uint whole = bfloor(exp); - uint remain = bsub(exp, whole); - - uint wholePow = bpowi(base, btoi(whole)); - - if (remain == 0) { - return wholePow; - } - - uint partialResult = bpowApprox(base, remain, BPOW_PRECISION); - return bmul(wholePow, partialResult); - } - - function bpowApprox(uint base, uint exp, uint precision) - internal pure - returns (uint) - { - // term 0: - uint a = exp; - (uint x, bool xneg) = bsubSign(base, BONE); - uint term = BONE; - uint sum = term; - bool negative = false; - - - // term(k) = numer / denom - // = (product(a - i - 1, i=1-->k) * x^k) / (k!) - // each iteration, multiply previous term by (a-(k-1)) * x / k - // continue until term is less than precision - for (uint i = 1; term >= precision; i++) { - uint bigK = i * BONE; - (uint c, bool cneg) = bsubSign(a, bsub(bigK, BONE)); - term = bmul(term, bmul(c, x)); - term = bdiv(term, bigK); - if (term == 0) break; - - if (xneg) negative = !negative; - if (cneg) negative = !negative; - if (negative) { - sum = bsub(sum, term); - } else { - sum = badd(sum, term); - } - } - - return sum; - } - -} -contract BMath is BBronze, BConst, BNum { - /********************************************************************************************** - // calcSpotPrice // - // sP = spotPrice // - // bI = tokenBalanceIn ( bI / wI ) 1 // - // bO = tokenBalanceOut sP = ----------- * ---------- // - // wI = tokenWeightIn ( bO / wO ) ( 1 - sF ) // - // wO = tokenWeightOut // - // sF = swapFee // - **********************************************************************************************/ - function calcSpotPrice( - uint tokenBalanceIn, - uint tokenWeightIn, - uint tokenBalanceOut, - uint tokenWeightOut, - uint swapFee - ) - internal pure - returns (uint spotPrice) - { - uint numer = bdiv(tokenBalanceIn, tokenWeightIn); - uint denom = bdiv(tokenBalanceOut, tokenWeightOut); - uint ratio = bdiv(numer, denom); - uint scale = bdiv(BONE, bsub(BONE, swapFee)); - return (spotPrice = bmul(ratio, scale)); - } - - /********************************************************************************************** - // calcOutGivenIn // - // aO = tokenAmountOut // - // bO = tokenBalanceOut // - // bI = tokenBalanceIn / / bI \ (wI / wO) \ // - // aI = tokenAmountIn aO = bO * | 1 - | -------------------------- | ^ | // - // wI = tokenWeightIn \ \ ( bI + ( aI * ( 1 - sF )) / / // - // wO = tokenWeightOut // - // sF = swapFee // - **********************************************************************************************/ - function calcOutGivenIn( - uint tokenBalanceIn, - uint tokenWeightIn, - uint tokenBalanceOut, - uint tokenWeightOut, - uint tokenAmountIn, - uint swapFee - ) - internal pure - returns (uint tokenAmountOut) - { - uint weightRatio = bdiv(tokenWeightIn, tokenWeightOut); - uint adjustedIn = bsub(BONE, swapFee); - adjustedIn = bmul(tokenAmountIn, adjustedIn); - uint y = bdiv(tokenBalanceIn, badd(tokenBalanceIn, adjustedIn)); - uint foo = bpow(y, weightRatio); - uint bar = bsub(BONE, foo); - tokenAmountOut = bmul(tokenBalanceOut, bar); - return tokenAmountOut; - } - - /********************************************************************************************** - // calcInGivenOut // - // aI = tokenAmountIn // - // bO = tokenBalanceOut / / bO \ (wO / wI) \ // - // bI = tokenBalanceIn bI * | | ------------ | ^ - 1 | // - // aO = tokenAmountOut aI = \ \ ( bO - aO ) / / // - // wI = tokenWeightIn -------------------------------------------- // - // wO = tokenWeightOut ( 1 - sF ) // - // sF = swapFee // - **********************************************************************************************/ - function calcInGivenOut( - uint tokenBalanceIn, - uint tokenWeightIn, - uint tokenBalanceOut, - uint tokenWeightOut, - uint tokenAmountOut, - uint swapFee - ) - internal pure - returns (uint tokenAmountIn) - { - uint weightRatio = bdiv(tokenWeightOut, tokenWeightIn); - uint diff = bsub(tokenBalanceOut, tokenAmountOut); - uint y = bdiv(tokenBalanceOut, diff); - uint foo = bpow(y, weightRatio); - foo = bsub(foo, BONE); - tokenAmountIn = bsub(BONE, swapFee); - tokenAmountIn = bdiv(bmul(tokenBalanceIn, foo), tokenAmountIn); - return tokenAmountIn; - } - - /********************************************************************************************** - // calcPoolOutGivenSingleIn // - // pAo = poolAmountOut / \ // - // tAi = tokenAmountIn /// / // wI \ \\ \ wI \ // - // wI = tokenWeightIn //| tAi *| 1 - || 1 - -- | * sF || + tBi \ -- \ // - // tW = totalWeight pAo=|| \ \ \\ tW / // | ^ tW | * pS - pS // - // tBi = tokenBalanceIn \\ ------------------------------------- / / // - // pS = poolSupply \\ tBi / / // - // sF = swapFee \ / // - **********************************************************************************************/ - function calcPoolOutGivenSingleIn( - uint tokenBalanceIn, - uint tokenWeightIn, - uint poolSupply, - uint totalWeight, - uint tokenAmountIn, - uint swapFee - ) - internal pure - returns (uint poolAmountOut) - { - // Charge the trading fee for the proportion of tokenAi - /// which is implicitly traded to the other pool tokens. - // That proportion is (1- weightTokenIn) - // tokenAiAfterFee = tAi * (1 - (1-weightTi) * poolFee); - uint normalizedWeight = bdiv(tokenWeightIn, totalWeight); - uint zaz = bmul(bsub(BONE, normalizedWeight), swapFee); - uint tokenAmountInAfterFee = bmul(tokenAmountIn, bsub(BONE, zaz)); - - uint newTokenBalanceIn = badd(tokenBalanceIn, tokenAmountInAfterFee); - uint tokenInRatio = bdiv(newTokenBalanceIn, tokenBalanceIn); - - // uint newPoolSupply = (ratioTi ^ weightTi) * poolSupply; - uint poolRatio = bpow(tokenInRatio, normalizedWeight); - uint newPoolSupply = bmul(poolRatio, poolSupply); - poolAmountOut = bsub(newPoolSupply, poolSupply); - return poolAmountOut; - } - - /********************************************************************************************** - // calcSingleInGivenPoolOut // - // tAi = tokenAmountIn //(pS + pAo)\ / 1 \\ // - // pS = poolSupply || --------- | ^ | --------- || * bI - bI // - // pAo = poolAmountOut \\ pS / \(wI / tW)// // - // bI = balanceIn tAi = -------------------------------------------- // - // wI = weightIn / wI \ // - // tW = totalWeight | 1 - ---- | * sF // - // sF = swapFee \ tW / // - **********************************************************************************************/ - function calcSingleInGivenPoolOut( - uint tokenBalanceIn, - uint tokenWeightIn, - uint poolSupply, - uint totalWeight, - uint poolAmountOut, - uint swapFee - ) - internal pure - returns (uint tokenAmountIn) - { - uint normalizedWeight = bdiv(tokenWeightIn, totalWeight); - uint newPoolSupply = badd(poolSupply, poolAmountOut); - uint poolRatio = bdiv(newPoolSupply, poolSupply); - - //uint newBalTi = poolRatio^(1/weightTi) * balTi; - uint boo = bdiv(BONE, normalizedWeight); - uint tokenInRatio = bpow(poolRatio, boo); - uint newTokenBalanceIn = bmul(tokenInRatio, tokenBalanceIn); - uint tokenAmountInAfterFee = bsub(newTokenBalanceIn, tokenBalanceIn); - // Do reverse order of fees charged in joinswap_ExternAmountIn, this way - // ``` pAo == joinswap_ExternAmountIn(Ti, joinswap_PoolAmountOut(pAo, Ti)) ``` - //uint tAi = tAiAfterFee / (1 - (1-weightTi) * swapFee) ; - uint zar = bmul(bsub(BONE, normalizedWeight), swapFee); - tokenAmountIn = bdiv(tokenAmountInAfterFee, bsub(BONE, zar)); - return tokenAmountIn; - } - - /********************************************************************************************** - // calcSingleOutGivenPoolIn // - // tAo = tokenAmountOut / / \\ // - // bO = tokenBalanceOut / // pS - (pAi * (1 - eF)) \ / 1 \ \\ // - // pAi = poolAmountIn | bO - || ----------------------- | ^ | --------- | * b0 || // - // ps = poolSupply \ \\ pS / \(wO / tW)/ // // - // wI = tokenWeightIn tAo = \ \ // // - // tW = totalWeight / / wO \ \ // - // sF = swapFee * | 1 - | 1 - ---- | * sF | // - // eF = exitFee \ \ tW / / // - **********************************************************************************************/ - function calcSingleOutGivenPoolIn( - uint tokenBalanceOut, - uint tokenWeightOut, - uint poolSupply, - uint totalWeight, - uint poolAmountIn, - uint swapFee - ) - internal pure - returns (uint tokenAmountOut) - { - uint normalizedWeight = bdiv(tokenWeightOut, totalWeight); - // charge exit fee on the pool token side - // pAiAfterExitFee = pAi*(1-exitFee) - uint poolAmountInAfterExitFee = bmul(poolAmountIn, bsub(BONE, EXIT_FEE)); - uint newPoolSupply = bsub(poolSupply, poolAmountInAfterExitFee); - uint poolRatio = bdiv(newPoolSupply, poolSupply); - - // newBalTo = poolRatio^(1/weightTo) * balTo; - uint tokenOutRatio = bpow(poolRatio, bdiv(BONE, normalizedWeight)); - uint newTokenBalanceOut = bmul(tokenOutRatio, tokenBalanceOut); - - uint tokenAmountOutBeforeSwapFee = bsub(tokenBalanceOut, newTokenBalanceOut); - - // charge swap fee on the output token side - //uint tAo = tAoBeforeSwapFee * (1 - (1-weightTo) * swapFee) - uint zaz = bmul(bsub(BONE, normalizedWeight), swapFee); - tokenAmountOut = bmul(tokenAmountOutBeforeSwapFee, bsub(BONE, zaz)); - return tokenAmountOut; - } - - /********************************************************************************************** - // calcPoolInGivenSingleOut // - // pAi = poolAmountIn // / tAo \\ / wO \ \ // - // bO = tokenBalanceOut // | bO - -------------------------- |\ | ---- | \ // - // tAo = tokenAmountOut pS - || \ 1 - ((1 - (tO / tW)) * sF)/ | ^ \ tW / * pS | // - // ps = poolSupply \\ -----------------------------------/ / // - // wO = tokenWeightOut pAi = \\ bO / / // - // tW = totalWeight ------------------------------------------------------------- // - // sF = swapFee ( 1 - eF ) // - // eF = exitFee // - **********************************************************************************************/ - function calcPoolInGivenSingleOut( - uint tokenBalanceOut, - uint tokenWeightOut, - uint poolSupply, - uint totalWeight, - uint tokenAmountOut, - uint swapFee - ) - internal pure - returns (uint poolAmountIn) - { - - // charge swap fee on the output token side - uint normalizedWeight = bdiv(tokenWeightOut, totalWeight); - //uint tAoBeforeSwapFee = tAo / (1 - (1-weightTo) * swapFee) ; - uint zoo = bsub(BONE, normalizedWeight); - uint zar = bmul(zoo, swapFee); - uint tokenAmountOutBeforeSwapFee = bdiv(tokenAmountOut, bsub(BONE, zar)); - - uint newTokenBalanceOut = bsub(tokenBalanceOut, tokenAmountOutBeforeSwapFee); - uint tokenOutRatio = bdiv(newTokenBalanceOut, tokenBalanceOut); - - //uint newPoolSupply = (ratioTo ^ weightTo) * poolSupply; - uint poolRatio = bpow(tokenOutRatio, normalizedWeight); - uint newPoolSupply = bmul(poolRatio, poolSupply); - uint poolAmountInAfterExitFee = bsub(poolSupply, newPoolSupply); - - // charge exit fee on the pool token side - // pAi = pAiAfterExitFee/(1-exitFee) - poolAmountIn = bdiv(poolAmountInAfterExitFee, bsub(BONE, EXIT_FEE)); - return poolAmountIn; - } - - -} \ No newline at end of file diff --git a/echidna/CryticInterface.sol b/echidna/CryticInterface.sol deleted file mode 100644 index 0b43050b..00000000 --- a/echidna/CryticInterface.sol +++ /dev/null @@ -1,5 +0,0 @@ -contract CryticInterface { - address internal crytic_owner = address(0x41414141); - address internal crytic_user = address(0x42424242); - address internal crytic_attacker = address(0x43434343); -} diff --git a/echidna/MyToken.sol b/echidna/MyToken.sol deleted file mode 100644 index 8c48dba9..00000000 --- a/echidna/MyToken.sol +++ /dev/null @@ -1,19 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./CryticInterface.sol"; - -contract MyToken is BToken, CryticInterface{ - - constructor(uint balance, address allowed) { - // balance is the new totalSupply - _totalSupply = balance; - // each user receives 1/3 of the balance and sets - // the allowance of the allowed address. - uint initialTotalSupply = balance; - _balance[crytic_owner] = initialTotalSupply/3; - _allowance[crytic_owner][allowed] = balance; - _balance[crytic_user] = initialTotalSupply/3; - _allowance[crytic_user][allowed] = balance; - _balance[crytic_attacker] = initialTotalSupply/3; - _allowance[crytic_attacker][allowed] = balance; - } -} diff --git a/echidna/TBPoolBalance.sol b/echidna/TBPoolBalance.sol deleted file mode 100644 index 6931e434..00000000 --- a/echidna/TBPoolBalance.sol +++ /dev/null @@ -1,34 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./MyToken.sol"; -import "./CryticInterface.sol"; - -contract TBPoolBalance is BPool, CryticInterface { - - MyToken public token; - uint internal initial_token_balance = uint(-1); - - constructor() public{ - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - token = new MyToken(initial_token_balance, address(this)); - // Bind the token with the minimal balance/weights - bind(address(token), MIN_BALANCE, MIN_WEIGHT); - // Enable public swap - setPublicSwap(true); - } - - function echidna_attacker_token_balance() public returns(bool){ - // An attacker cannot obtain more tokens than its initial balance - return token.balanceOf(crytic_attacker) == initial_token_balance/3; //initial balance of crytic_attacker - } - - function echidna_pool_record_balance() public returns (bool) { - // If the token was unbinded, avoid revert and return true - if (this.getNumTokens() == 0) - return true; - // The token balance should not be out-of-sync - return (token.balanceOf(address(this)) >= this.getBalance(address(token))); - } -} diff --git a/echidna/TBPoolBalance.yaml b/echidna/TBPoolBalance.yaml deleted file mode 100644 index cd4d21c4..00000000 --- a/echidna/TBPoolBalance.yaml +++ /dev/null @@ -1,7 +0,0 @@ -seqLen: 50 -testLimit: 100000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242","0x43434343"] -psender: "0x41414141" -dashboard: true diff --git a/echidna/TBPoolBind.sol b/echidna/TBPoolBind.sol deleted file mode 100644 index 0e98164d..00000000 --- a/echidna/TBPoolBind.sol +++ /dev/null @@ -1,169 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./MyToken.sol"; -import "./CryticInterface.sol"; - -contract TBPoolBindPrivileged is CryticInterface, BPool { - - constructor() { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken t; - t = new MyToken(initial_token_balance, address(this)); - bind(address(t), MIN_BALANCE, MIN_WEIGHT); - } - - // initial token balances is the max amount for uint256 - uint internal initial_token_balance = uint(-1); - // these two variables are used to save valid balances and denorm parameters - uint internal valid_balance_to_bind = MIN_BALANCE; - uint internal valid_denorm_to_bind = MIN_WEIGHT; - - - // this function allows to create as many tokens as needed - function create_and_bind(uint balance, uint denorm) public returns (address) { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken bt = new MyToken(initial_token_balance, address(this)); - bt.approve(address(this), initial_token_balance); - // Bind the token with the provided parameters - bind(address(bt), balance, denorm); - // Save the balance and denorm values used. These are used in the rebind checks - valid_balance_to_bind = balance; - valid_denorm_to_bind = denorm; - return address(bt); - } - - function echidna_getNumTokens_less_or_equal_MAX_BOUND_TOKENS() public returns (bool) { - // it is not possible to bind more than `MAX_BOUND_TOKENS` - return this.getNumTokens() <= MAX_BOUND_TOKENS; - } - - function echidna_revert_bind_twice() public returns (bool) { - if (this.getCurrentTokens().length > 0 && this.getController() == crytic_owner && !this.isFinalized()) { - // binding the first token should be enough, if we have this property to always revert - bind(this.getCurrentTokens()[0], valid_balance_to_bind, valid_denorm_to_bind); - // This return will make this property to fail - return true; - } - // If there are no tokens or if the controller was changed or if the pool was finalized, just revert. - revert(); - } - - function echidna_revert_unbind_twice() public returns (bool) { - if (this.getCurrentTokens().length > 0 && this.getController() == crytic_owner && !this.isFinalized()) { - address[] memory current_tokens = this.getCurrentTokens(); - // unbinding the first token twice should be enough, if we want this property to always revert - unbind(current_tokens[0]); - unbind(current_tokens[0]); - return true; - } - // if there are no tokens or if the controller was changed or if the pool was finalized, just revert - revert(); - } - - function echidna_all_tokens_are_unbindable() public returns (bool) { - if (this.getController() == crytic_owner && !this.isFinalized()) { - address[] memory current_tokens = this.getCurrentTokens(); - // unbind all the tokens, one by one - for (uint i = 0; i < current_tokens.length; i++) { - unbind(current_tokens[i]); - } - // at the end, the list of current tokens should be empty - return (this.getCurrentTokens().length == 0); - } - - // if the controller was changed or if the pool was finalized, just return true - return true; - } - - function echidna_all_tokens_are_rebindable_with_valid_parameters() public returns (bool) { - if (this.getController() == crytic_owner && !this.isFinalized()) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // rebind all the tokens, one by one, using valid parameters - rebind(current_tokens[i], valid_balance_to_bind, valid_denorm_to_bind); - } - // at the end, the list of current tokens should have not change in size - return current_tokens.length == this.getCurrentTokens().length; - } - // if the controller was changed or if the pool was finalized, just return true - return true; - } - - function echidna_revert_rebind_unbinded() public returns (bool) { - if (this.getCurrentTokens().length > 0 && this.getController() == crytic_owner && !this.isFinalized()) { - address[] memory current_tokens = this.getCurrentTokens(); - // unbinding and rebinding the first token should be enough, if we want this property to always revert - unbind(current_tokens[0]); - rebind(current_tokens[0], valid_balance_to_bind, valid_denorm_to_bind); - return true; - } - // if the controller was changed or if the pool was finalized, just return true - revert(); - } -} - -contract TBPoolBindUnprivileged is CryticInterface, BPool { - - MyToken t1; - MyToken t2; - // initial token balances is the max amount for uint256 - uint internal initial_token_balance = uint(-1); - - constructor() { - // two tokens with minimal balances and weights are created by the controller - t1 = new MyToken(initial_token_balance, address(this)); - bind(address(t1), MIN_BALANCE, MIN_WEIGHT); - t2 = new MyToken(initial_token_balance, address(this)); - bind(address(t2), MIN_BALANCE, MIN_WEIGHT); - } - - // these two variables are used to save valid balances and denorm parameters - uint internal valid_balance_to_bind = MIN_BALANCE; - uint internal valid_denorm_to_bind = MIN_WEIGHT; - - // this function allows to create as many tokens as needed - function create_and_bind(uint balance, uint denorm) public returns (address) { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken bt = new MyToken(initial_token_balance, address(this)); - bt.approve(address(this), initial_token_balance); - // Bind the token with the provided parameters - bind(address(bt), balance, denorm); - // Save the balance and denorm values used. These are used in the rebind checks - valid_balance_to_bind = balance; - valid_denorm_to_bind = denorm; - return address(bt); - } - - function echidna_only_controller_can_bind() public returns (bool) { - // the number of tokens cannot be changed - return this.getNumTokens() == 2; - } - - function echidna_revert_when_bind() public returns (bool) { - // calling bind will revert - create_and_bind(valid_balance_to_bind, valid_denorm_to_bind); - return true; - } - - function echidna_revert_when_rebind() public returns (bool) { - // calling rebind on binded tokens will revert - rebind(address(t1), valid_balance_to_bind, valid_denorm_to_bind); - rebind(address(t2), valid_balance_to_bind, valid_denorm_to_bind); - return true; - } - - function echidna_revert_when_unbind() public returns (bool) { - // calling unbind on binded tokens will revert - unbind(address(t1)); - unbind(address(t2)); - return true; - } -} diff --git a/echidna/TBPoolBindPrivileged.yaml b/echidna/TBPoolBindPrivileged.yaml deleted file mode 100644 index 1695608f..00000000 --- a/echidna/TBPoolBindPrivileged.yaml +++ /dev/null @@ -1,9 +0,0 @@ -seqLen: 50 -testLimit: 100000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true -corpusDir: "corpus" -mutation: true diff --git a/echidna/TBPoolBindUnprivileged.yaml b/echidna/TBPoolBindUnprivileged.yaml deleted file mode 100644 index 95044fad..00000000 --- a/echidna/TBPoolBindUnprivileged.yaml +++ /dev/null @@ -1,7 +0,0 @@ -seqLen: 50 -testLimit: 20000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x42424242", "0x43434343"] -psender: "0x42424242" -dashboard: true diff --git a/echidna/TBPoolController.sol b/echidna/TBPoolController.sol deleted file mode 100644 index 5a3d3947..00000000 --- a/echidna/TBPoolController.sol +++ /dev/null @@ -1,33 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./CryticInterface.sol"; - -contract TBPoolControllerPrivileged is CryticInterface, BPool { - - function echidna_controller_should_change() public returns (bool) { - if (this.getController() == crytic_owner) { - setController(crytic_user); - return (this.getController() == crytic_user); - } - // if the controller was changed, this should return true - return true; - } - - function echidna_revert_controller_cannot_be_null() public returns (bool) { - if (this.getController() == crytic_owner) { - // setting the controller to 0x0 should fail - setController(address(0x0)); - return true; - } - // if the controller was changed, this should revert anyway - revert(); - } -} - -contract TBPoolControllerUnprivileged is CryticInterface, BPool { - - function echidna_no_other_user_can_change_the_controller() public returns (bool) { - // the controller cannot be changed by other users - return this.getController() == crytic_owner; - } - -} diff --git a/echidna/TBPoolControllerPrivileged.yaml b/echidna/TBPoolControllerPrivileged.yaml deleted file mode 100644 index 86790a19..00000000 --- a/echidna/TBPoolControllerPrivileged.yaml +++ /dev/null @@ -1,7 +0,0 @@ -seqLen: 50 -testLimit: 20000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true diff --git a/echidna/TBPoolControllerUnprivileged.yaml b/echidna/TBPoolControllerUnprivileged.yaml deleted file mode 100644 index 6e69a8a9..00000000 --- a/echidna/TBPoolControllerUnprivileged.yaml +++ /dev/null @@ -1,7 +0,0 @@ -seqLen: 50 -testLimit: 20000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true diff --git a/echidna/TBPoolExitSwap.sol b/echidna/TBPoolExitSwap.sol deleted file mode 100644 index fb1826a2..00000000 --- a/echidna/TBPoolExitSwap.sol +++ /dev/null @@ -1,23 +0,0 @@ -import "./BMathInternal.sol"; - -// This contract used a modified version of BMath where all the public/external functions are internal to speed up Echidna exploration -contract TestSwapOut is BMath { - - bool public echidna_no_bug = true; - - // A bug is found if tokenAmountOut can be greater than 0 while calcPoolInGivenSingleOut returns 0 - function exitswapExternAmountOut(uint balanceOut, uint poolTotal, uint tokenAmountOut) public { - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - - require(balanceOut <= 10 ether); - require(balanceOut >= 10**6); - - require(tokenAmountOut > 0); - require(calcPoolInGivenSingleOut(balanceOut, MIN_WEIGHT, poolTotal, MIN_WEIGHT*2, tokenAmountOut, MIN_FEE)==0); - echidna_no_bug = false; - } - -} \ No newline at end of file diff --git a/echidna/TBPoolJoinExit.sol b/echidna/TBPoolJoinExit.sol deleted file mode 100644 index c2563036..00000000 --- a/echidna/TBPoolJoinExit.sol +++ /dev/null @@ -1,116 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./MyToken.sol"; -import "./CryticInterface.sol"; - -contract TBPoolJoinExit is CryticInterface, BPool { - - uint MAX_BALANCE = BONE * 10**12; - - constructor() { - MyToken t; - t = new MyToken(uint(-1), address(this)); - bind(address(t), MAX_BALANCE, MAX_WEIGHT); - } - - // initial token balances is the max amount for uint256 - uint internal initial_token_balance = uint(-1); - - // this function allows to create as many tokens as needed - function create_and_bind(uint balance, uint denorm) public returns (address) { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken bt = new MyToken(initial_token_balance, address(this)); - bt.approve(address(this), initial_token_balance); - // Bind the token with the provided parameters - bind(address(bt), balance, denorm); - return address(bt); - } - - uint[] internal maxAmountsIn = [uint(-1), uint(-1), uint(-1), uint(-1), uint(-1), uint(-1)]; - uint[] internal minAmountsOut = [0, 0, 0, 0, 0, 0, 0, 0]; - uint[8] internal balances = [0, 0, 0, 0, 0, 0, 0, 0]; - - uint internal amount = EXIT_FEE; - uint internal amount1 = EXIT_FEE; - uint internal amount2 = EXIT_FEE; - - // sets an amount between EXIT_FEE and EXIT_FEE + 2**64 - function set_input(uint _amount) public { - amount = EXIT_FEE + _amount % 2**64; - } - - // sets two amounts between EXIT_FEE and EXIT_FEE + 2**64 - function set_two_inputs(uint _amount1, uint _amount2) public { - amount1 = EXIT_FEE + _amount1 % 2**64; - amount2 = EXIT_FEE + _amount2 % 2**64; - } - - function echidna_joinPool_exitPool_balance_consistency() public returns (bool) { - - // if the pool was not finalize, return true (it is unclear how to finalize it) - if (!this.isFinalized()) - return true; - - // check this precondition for joinPool - if (bdiv(amount, this.totalSupply()) == 0) - return true; - - // save all the token balances in `balances` before calling joinPool / exitPool - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) - balances[i] = (IERC20(current_tokens[i]).balanceOf(address(msg.sender))); - - // save the amount of share tokens - uint old_balance = this.balanceOf(crytic_owner); - - // call joinPool, with some some reasonable amount - joinPool(amount, maxAmountsIn); - // check that the amount of shares decreased - if (this.balanceOf(crytic_owner) - amount != old_balance) - return false; - - // check the precondition for exitPool - uint exit_fee = bmul(amount, EXIT_FEE); - uint pAiAfterExitFee = bsub(amount, exit_fee); - if(bdiv(pAiAfterExitFee, this.totalSupply()) == 0) - return true; - - // call exitPool with some reasonable amount - exitPool(amount, minAmountsOut); - uint new_balance = this.balanceOf(crytic_owner); - - // check that the amount of shares decreased, taking in consideration that - // _factory is crytic_owner, so it will receive the exit_fees - if (old_balance != new_balance - exit_fee) - return false; - - // verify that the final token balance are consistent. It is possible - // to have rounding issues, but it should not allow to obtain more tokens than - // the ones a user owned - for (uint i = 0; i < current_tokens.length; i++) { - uint current_balance = IERC20(current_tokens[i]).balanceOf(address(msg.sender)); - if (balances[i] < current_balance) - return false; - } - - return true; - } - - function echidna_revert_impossible_joinPool_exitPool() public returns (bool) { - - // the amount to join should be smaller to the amount to exit - if (amount1 >= amount2) - revert(); - - // burn all the shares transfering them to 0x0 - transfer(address(0x0), this.balanceOf(msg.sender)); - // join a pool with a reasonable amount. - joinPool(amount1, maxAmountsIn); - // exit a pool with a larger amount - exitPool(amount2, minAmountsOut); - return true; - } - -} diff --git a/echidna/TBPoolJoinExit.yaml b/echidna/TBPoolJoinExit.yaml deleted file mode 100644 index e27c5ce4..00000000 --- a/echidna/TBPoolJoinExit.yaml +++ /dev/null @@ -1,9 +0,0 @@ -seqLen: 50 -testLimit: 1000000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true -corpusDir: "corpus" -mutation: true diff --git a/echidna/TBPoolLimits.sol b/echidna/TBPoolLimits.sol deleted file mode 100644 index c2407ede..00000000 --- a/echidna/TBPoolLimits.sol +++ /dev/null @@ -1,149 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./MyToken.sol"; -import "./CryticInterface.sol"; - -contract TBPoolLimits is CryticInterface, BPool { - - uint MAX_BALANCE = BONE * 10**12; - - constructor() { - MyToken t; - t = new MyToken(uint(-1), address(this)); - bind(address(t), MIN_BALANCE, MIN_WEIGHT); - } - - // initial token balances is the max amount for uint256 - uint internal initial_token_balance = uint(-1); - // these two variables are used to save valid balances and denorm parameters - uint internal valid_balance_to_bind = MIN_BALANCE; - uint internal valid_denorm_to_bind = MIN_WEIGHT; - - // this function allows to create as many tokens as needed - function create_and_bind(uint balance, uint denorm) public returns (address) { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken bt = new MyToken(initial_token_balance, address(this)); - bt.approve(address(this), initial_token_balance); - // Bind the token with the provided parameters - bind(address(bt), balance, denorm); - // Save the balance and denorm values used. These are used in the rebind checks - valid_balance_to_bind = balance; - valid_denorm_to_bind = denorm; - return address(bt); - } - - function echidna_valid_weights() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - // store the normalized weight in this variable - uint nw = 0; - for (uint i = 0; i < current_tokens.length; i++) { - // accumulate the total normalized weights, checking for overflows - nw = badd(nw,this.getNormalizedWeight(current_tokens[i])); - } - // convert the sum of normalized weights into an integer - nw = btoi(nw); - - // if there are no tokens, check that the normalized weight is zero - if (current_tokens.length == 0) - return (nw == 0); - - // if there are tokens, the normalized weight should be 1 - return (nw == 1); - } - - function echidna_min_token_balance() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // verify that the balance of each token is more than `MIN_BALACE` - if (this.getBalance(address(current_tokens[i])) < MIN_BALANCE) - return false; - } - // if there are no tokens, return true - return true; - } - - function echidna_max_weight() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // verify that the weight of each token is less than `MAX_WEIGHT` - if (this.getDenormalizedWeight(address(current_tokens[i])) > MAX_WEIGHT) - return false; - } - // if there are no tokens, return true - return true; - } - - function echidna_min_weight() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // verify that the weight of each token is more than `MIN_WEIGHT` - if (this.getDenormalizedWeight(address(current_tokens[i])) < MIN_WEIGHT) - return false; - } - // if there are no tokens, return true - return true; - } - - - function echidna_min_swap_free() public returns (bool) { - // verify that the swap fee is greater or equal than `MIN_FEE` - return this.getSwapFee() >= MIN_FEE; - } - - function echidna_max_swap_free() public returns (bool) { - // verify that the swap fee is less or equal than `MAX_FEE` - return this.getSwapFee() <= MAX_FEE; - } - - function echidna_revert_max_swapExactAmountOut() public returns (bool) { - // if the controller was changed, revert - if (this.getController() != crytic_owner) - revert(); - - // if the pool is not finalized, make sure public swap is enabled - if (!this.isFinalized()) - setPublicSwap(true); - - address[] memory current_tokens = this.getCurrentTokens(); - // if there is not token, revert - if (current_tokens.length == 0) - revert(); - - uint large_balance = this.getBalance(current_tokens[0])/3 + 2; - - // check that the balance is large enough - if (IERC20(current_tokens[0]).balanceOf(crytic_owner) < large_balance) - revert(); - - // call swapExactAmountOut with more than 1/3 of the balance should revert - swapExactAmountOut(address(current_tokens[0]), uint(-1), address(current_tokens[0]), large_balance, uint(-1)); - return true; - } - - function echidna_revert_max_swapExactAmountIn() public returns (bool) { - // if the controller was changed, revert - if (this.getController() != crytic_owner) - revert(); - - // if the pool is not finalized, make sure public swap is enabled - if (!this.isFinalized()) - setPublicSwap(true); - - address[] memory current_tokens = this.getCurrentTokens(); - // if there is not token, revert - if (current_tokens.length == 0) - revert(); - - uint large_balance = this.getBalance(current_tokens[0])/2 + 1; - - if (IERC20(current_tokens[0]).balanceOf(crytic_owner) < large_balance) - revert(); - - swapExactAmountIn(address(current_tokens[0]), large_balance, address(current_tokens[0]), 0, uint(-1)); - - return true; - } - -} diff --git a/echidna/TBPoolLimits.yaml b/echidna/TBPoolLimits.yaml deleted file mode 100644 index 1695608f..00000000 --- a/echidna/TBPoolLimits.yaml +++ /dev/null @@ -1,9 +0,0 @@ -seqLen: 50 -testLimit: 100000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true -corpusDir: "corpus" -mutation: true diff --git a/echidna/TBPoolNoRevert.sol b/echidna/TBPoolNoRevert.sol deleted file mode 100644 index 4ddb4f92..00000000 --- a/echidna/TBPoolNoRevert.sol +++ /dev/null @@ -1,102 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; -import "./MyToken.sol"; -import "./CryticInterface.sol"; - -contract TBPoolNoRevert is CryticInterface, BPool { - - constructor() { // out-of-gas? - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken t; - t = new MyToken(initial_token_balance, address(this)); - bind(address(t), MIN_BALANCE, MIN_WEIGHT); - } - - // initial token balances is the max amount for uint256 - uint internal initial_token_balance = uint(-1); - - // this function allows to create as many tokens as needed - function create_and_bind(uint balance, uint denorm) public returns (address) { - // Create a new token with initial_token_balance as total supply. - // After the token is created, each user defined in CryticInterface - // (crytic_owner, crytic_user and crytic_attacker) receives 1/3 of - // the initial balance - MyToken bt = new MyToken(initial_token_balance, address(this)); - bt.approve(address(this), initial_token_balance); - // Bind the token with the provided parameters - bind(address(bt), balance, denorm); - // Save the balance and denorm values used. These are used in the rebind checks - return address(bt); - } - - function echidna_getSpotPrice_no_revert() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - for (uint j = 0; j < current_tokens.length; j++) { - // getSpotPrice should not revert for any pair of tokens - this.getSpotPrice(address(current_tokens[i]), address(current_tokens[j])); - } - } - - return true; - } - - function echidna_getSpotPriceSansFee_no_revert() public returns (bool) { - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - for (uint j = 0; j < current_tokens.length; j++) { - // getSpotPriceSansFee should not revert for any pair of tokens - this.getSpotPriceSansFee(address(current_tokens[i]), address(current_tokens[j])); - } - } - - return true; - } - - function echidna_swapExactAmountIn_no_revert() public returns (bool) { - // if the controller was changed, return true - if (this.getController() != crytic_owner) - return true; - - // if the pool was not finalized, enable the public swap - if (!this.isFinalized()) - setPublicSwap(true); - - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // a small balance is 1% of the total balance available - uint small_balance = this.getBalance(current_tokens[i])/100; - // if the user has a small balance, it should be able to swap it - if (IERC20(current_tokens[i]).balanceOf(crytic_owner) > small_balance) - swapExactAmountIn(address(current_tokens[i]), small_balance, address(current_tokens[i]), 0, uint(-1)); - } - - return true; - } - - function echidna_swapExactAmountOut_no_revert() public returns (bool) { - - // if the controller was changed, return true - if (this.getController() != crytic_owner) - return true; - - // if the pool was not finalized, enable the public swap - if (!this.isFinalized()) - setPublicSwap(true); - - address[] memory current_tokens = this.getCurrentTokens(); - for (uint i = 0; i < current_tokens.length; i++) { - // a small balance is 1% of the total balance available - uint small_balance = this.getBalance(current_tokens[i])/100; - // if the user has a small balance, it should be able to swap it - if (IERC20(current_tokens[i]).balanceOf(crytic_owner) > small_balance) - swapExactAmountOut(address(current_tokens[i]), uint(-1), address(current_tokens[i]), small_balance, uint(-1)); - } - - return true; - } - -} - diff --git a/echidna/TBPoolNoRevert.yaml b/echidna/TBPoolNoRevert.yaml deleted file mode 100644 index 1695608f..00000000 --- a/echidna/TBPoolNoRevert.yaml +++ /dev/null @@ -1,9 +0,0 @@ -seqLen: 50 -testLimit: 100000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x41414141", "0x42424242", "0x43434343"] -psender: "0x41414141" -dashboard: true -corpusDir: "corpus" -mutation: true diff --git a/echidna/TBTokenERC20.sol b/echidna/TBTokenERC20.sol deleted file mode 100644 index ca750037..00000000 --- a/echidna/TBTokenERC20.sol +++ /dev/null @@ -1,170 +0,0 @@ -import "../crytic-export/flattening/BPool.sol"; - -contract CryticInterface{ - address internal crytic_owner = address(0x41414141); - address internal crytic_user = address(0x42424242); - address internal crytic_attacker = address(0x43434343); - - uint internal initialTotalSupply = uint(-1); - uint internal initialBalance_owner; - uint internal initialBalance_user; - uint internal initialBalance_attacker; - - uint initialAllowance_user_attacker; - uint initialAllowance_attacker_user; - uint initialAllowance_attacker_attacker; -} - -contract TBTokenERC20 is CryticInterface, BToken { - - constructor() { - _totalSupply = initialTotalSupply; - _balance[crytic_owner] = 0; - _balance[crytic_user] = initialTotalSupply/2; - initialBalance_user = initialTotalSupply/2; - _balance[crytic_attacker] = initialTotalSupply/2; - initialBalance_attacker = initialTotalSupply/2; - } - - - /* - Type: Code quality - Return: Success - */ - function echidna_zero_always_empty() public returns(bool){ - return this.balanceOf(address(0x0)) == 0; - } - - /* - Type: Code Quality - Return: - */ - function echidna_approve_overwrites() public returns (bool) { - bool approve_return; - approve_return = approve(crytic_user, 10); - require(approve_return); - approve_return = approve(crytic_user, 20); - require(approve_return); - return this.allowance(msg.sender, crytic_user) == 20; - } - - /* - Type: Undetermined severity - Return: Success - */ - function echidna_balance_less_than_totalSupply() public returns(bool){ - return this.balanceOf(msg.sender) <= _totalSupply; - } - - /* - Type: Low severity - Return: Success - */ - function echidna_totalSupply_balances_consistency() public returns(bool){ - return this.balanceOf(crytic_owner) + this.balanceOf(crytic_user) + this.balanceOf(crytic_attacker) <= totalSupply(); - } - - /* - Properties: Transferable - */ - - /* - Type: Code Quality - Return: Fail or Throw - */ - function echidna_revert_transfer_to_zero() public returns (bool) { - if (this.balanceOf(msg.sender) == 0) - revert(); - return transfer(address(0x0), this.balanceOf(msg.sender)); - } - - /* - Type: Code Quality - Return: Fail or Throw - */ - function echidna_revert_transferFrom_to_zero() public returns (bool) { - uint balance = this.balanceOf(msg.sender); - bool approve_return = approve(msg.sender, balance); - return transferFrom(msg.sender, address(0x0), this.balanceOf(msg.sender)); - } - - /* - Type: ERC20 Standard - Fire: Transfer(msg.sender, msg.sender, balanceOf(msg.sender)) - Return: Success - */ - function echidna_self_transferFrom() public returns(bool){ - uint balance = this.balanceOf(msg.sender); - bool approve_return = approve(msg.sender, balance); - bool transfer_return = transferFrom(msg.sender, msg.sender, balance); - return (this.balanceOf(msg.sender) == balance) && approve_return && transfer_return; - } - - - /* - Type: ERC20 Standard - Return: Success - */ - function echidna_self_transferFrom_to_other() public returns(bool){ - uint balance = this.balanceOf(msg.sender); - bool approve_return = approve(msg.sender, balance); - bool transfer_return = transferFrom(msg.sender, crytic_owner, balance); - return (this.balanceOf(msg.sender) == 0) && approve_return && transfer_return; - } - - /* - Type: ERC20 Standard - Fire: Transfer(msg.sender, msg.sender, balanceOf(msg.sender)) - Return: Success - */ - function echidna_self_transfer() public returns(bool){ - uint balance = this.balanceOf(msg.sender); - bool transfer_return = transfer(msg.sender, balance); - return (this.balanceOf(msg.sender) == balance) && transfer_return; - } - - /* - Type: ERC20 Standard - Fire: Transfer(msg.sender, other, 1) - Return: Success - */ - function echidna_transfer_to_other() public returns(bool){ - uint balance = this.balanceOf(msg.sender); - address other = crytic_user; - if (other == msg.sender) { - other = crytic_owner; - } - if (balance >= 1) { - bool transfer_other = transfer(other, 1); - return (this.balanceOf(msg.sender) == balance-1) && (this.balanceOf(other) >= 1) && transfer_other; - } - return true; - } - - /* - Type: ERC20 Standard - Fire: Transfer(msg.sender, user, balance+1) - Return: Fail or Throw - */ - function echidna_revert_transfer_to_user() public returns(bool){ - uint balance = this.balanceOf(msg.sender); - if (balance == (2 ** 256 - 1)) - revert(); - bool transfer_other = transfer(crytic_user, balance+1); - return true; - } - - - /* - Properties: Not Mintable - */ - - /* - Type: Undetermined severity - Return: Success - */ - function echidna_totalSupply_constant() public returns(bool){ - return initialTotalSupply == totalSupply(); - } - -} diff --git a/echidna/TBTokenERC20.yaml b/echidna/TBTokenERC20.yaml deleted file mode 100644 index 9234033a..00000000 --- a/echidna/TBTokenERC20.yaml +++ /dev/null @@ -1,7 +0,0 @@ -seqLen: 50 -testLimit: 100000 -prefix: "echidna_" -deployer: "0x41414141" -sender: ["0x42424242", "0x43434343"] -psender: "0x43434343" -dashboard: true diff --git a/echidna_general_config.yaml b/echidna_general_config.yaml deleted file mode 100644 index 19d47dde..00000000 --- a/echidna_general_config.yaml +++ /dev/null @@ -1,2 +0,0 @@ -seqLen: 50 -testLimit: 1000000 diff --git a/manticore/TBPoolJoinExit.py b/manticore/TBPoolJoinExit.py deleted file mode 100644 index c604d0b7..00000000 --- a/manticore/TBPoolJoinExit.py +++ /dev/null @@ -1,64 +0,0 @@ -from manticore.ethereum import ManticoreEVM, ABI -from manticore.core.smtlib import Operators, Z3Solver -from manticore.utils import config -from manticore.core.plugin import Plugin - -m = ManticoreEVM() - -# Disable the gas tracking -consts_evm = config.get_group("evm") -consts_evm.oog = "ignore" - -# Increase the solver timeout -config.get_group("smt").defaultunsat = False -config.get_group("smt").timeout = 3600 - -ETHER = 10 ** 18 - -user = m.create_account(balance=1 * ETHER) - -# This plugin is used to speed up the exploration and skip the require(false) paths -# It won't be needed once https://github.com/trailofbits/manticore/issues/1593 is added -class SkipRequire(Plugin): - def will_evm_execute_instruction_callback(self, state, instruction, arguments): - world = state.platform - if state.platform.current_transaction.sort != 'CREATE': - if instruction.semantics == "JUMPI": - potential_revert = world.current_vm.read_code(world.current_vm.pc + 4) - if potential_revert[0].size == 8 and potential_revert[0].value == 0xfd: - state.constrain(arguments[1] == True) - - -print(f'controller: {hex(user.address)}') - -skipRequire = SkipRequire() -m.register_plugin(skipRequire) - -TestBpool = m.solidity_create_contract('./manticore/contracts/TBPoolJoinExit.sol', - contract_name='TestJoinExit', - owner=user) - -print(f'TBPoolJoinExit deployed {hex(TestBpool.address)}') - -# Call joinAndExitPool with symbolic values -poolAmountOut = m.make_symbolic_value() -poolAmountIn = m.make_symbolic_value() -poolTotal = m.make_symbolic_value() -_records_t_balance = m.make_symbolic_value() -TestBpool.joinAndExitPool(poolAmountOut, poolAmountIn, poolTotal, _records_t_balance) - -print(f'joinAndExitPool Called') - -for state in m.ready_states: - - m.generate_testcase(state, name="BugFound") - - # Look over the 10**i, and try to generate more free tokens - for i in range(0, 18): - print(i) - add_value = 10**i - condition = Operators.AND(poolAmountOut > poolAmountIn + add_value, poolAmountIn + add_value > poolAmountIn) - m.generate_testcase(state, name=f"BugFound{add_value}", only_if=condition) - -print(f'Results are in {m.workspace}') - diff --git a/manticore/TBPoolJoinExitNoFee.py b/manticore/TBPoolJoinExitNoFee.py deleted file mode 100644 index 4f049712..00000000 --- a/manticore/TBPoolJoinExitNoFee.py +++ /dev/null @@ -1,64 +0,0 @@ -from manticore.ethereum import ManticoreEVM, ABI -from manticore.core.smtlib import Operators, Z3Solver -from manticore.utils import config -from manticore.core.plugin import Plugin - -m = ManticoreEVM() - -# Disable the gas tracking -consts_evm = config.get_group("evm") -consts_evm.oog = "ignore" - -# Increase the solver timeout -config.get_group("smt").defaultunsat = False -config.get_group("smt").timeout = 3600 - -ETHER = 10 ** 18 - -user = m.create_account(balance=1 * ETHER) - -# This plugin is used to speed up the exploration and skip the require(false) paths -# It won't be needed once https://github.com/trailofbits/manticore/issues/1593 is added -class SkipRequire(Plugin): - def will_evm_execute_instruction_callback(self, state, instruction, arguments): - world = state.platform - if state.platform.current_transaction.sort != 'CREATE': - if instruction.semantics == "JUMPI": - potential_revert = world.current_vm.read_code(world.current_vm.pc + 4) - if potential_revert[0].size == 8 and potential_revert[0].value == 0xfd: - state.constrain(arguments[1] == True) - - -print(f'controller: {hex(user.address)}') - -skipRequire = SkipRequire() -m.register_plugin(skipRequire) - -TestBpool = m.solidity_create_contract('./manticore/contracts/TBPoolJoinExitNoFee.sol', - contract_name='TBPoolJoinExitNoFee', - owner=user) - -print(f'TestJoinExit deployed {hex(TestBpool.address)}') - -# Call joinAndExitNoFeePool with symbolic values -poolAmountOut = m.make_symbolic_value() -poolAmountIn = m.make_symbolic_value() -poolTotal = m.make_symbolic_value() -_records_t_balance = m.make_symbolic_value() -TestBpool.joinAndExitNoFeePool(poolAmountOut, poolAmountIn, poolTotal, _records_t_balance) - -print(f'joinAndExitNoFeePool Called') - -for state in m.ready_states: - - m.generate_testcase(state, name="BugFound") - - # Look over the 10**i, and try to generate more free tokens - for i in range(0, 18): - print(i) - add_value = 10**i - condition = Operators.AND(poolAmountOut > poolAmountIn + add_value, poolAmountIn + add_value > poolAmountIn) - m.generate_testcase(state, name=f"BugFound{add_value}", only_if=condition) - -print(f'Results are in {m.workspace}') - diff --git a/manticore/TBPoolJoinPool.py b/manticore/TBPoolJoinPool.py deleted file mode 100644 index 09b16875..00000000 --- a/manticore/TBPoolJoinPool.py +++ /dev/null @@ -1,63 +0,0 @@ -from manticore.ethereum import ManticoreEVM, ABI -from manticore.core.smtlib import Operators, Z3Solver -from manticore.utils import config -from manticore.core.plugin import Plugin - -m = ManticoreEVM() - -# Disable the gas tracking -consts_evm = config.get_group("evm") -consts_evm.oog = "ignore" - -# Increase the solver timeout -config.get_group("smt").defaultunsat = False -config.get_group("smt").timeout = 3600 - -ETHER = 10 ** 18 - -user = m.create_account(balance=1 * ETHER) - -# This plugin is used to speed up the exploration and skip the require(false) paths -# It won't be needed once https://github.com/trailofbits/manticore/issues/1593 is added -class SkipRequire(Plugin): - def will_evm_execute_instruction_callback(self, state, instruction, arguments): - world = state.platform - if state.platform.current_transaction.sort != 'CREATE': - if instruction.semantics == "JUMPI": - potential_revert = world.current_vm.read_code(world.current_vm.pc + 4) - if potential_revert[0].size == 8 and potential_revert[0].value == 0xfd: - state.constrain(arguments[1] == True) - - -print(f'controller: {hex(user.address)}') - -skipRequire = SkipRequire() -m.register_plugin(skipRequire) - -TestBpool = m.solidity_create_contract('./manticore/contracts/TBPoolJoinPool.sol', - contract_name='TBPoolJoinPool', - owner=user) - -print(f'TBPoolJoinPool deployed {hex(TestBpool.address)}') - -# Call joinAndExitNoFeePool with symbolic values -poolAmountOut = m.make_symbolic_value() -poolTotal = m.make_symbolic_value() -_records_t_balance = m.make_symbolic_value() -TestBpool.joinPool(poolAmountOut, poolTotal, _records_t_balance) - -print(f'joinPool Called') - -for state in m.ready_states: - - m.generate_testcase(state, name="BugFound") - - # Look over the 10**i, and try to generate more free tokens - for i in range(0, 18): - print(i) - add_value = 10**i - condition = Operators.AND(poolAmountOut > poolAmountIn + add_value, poolAmountIn + add_value > poolAmountIn) - m.generate_testcase(state, name=f"BugFound{add_value}", only_if=condition) - -print(f'Results are in {m.workspace}') - diff --git a/manticore/contracts/BNum.sol b/manticore/contracts/BNum.sol deleted file mode 100644 index e6708bd3..00000000 --- a/manticore/contracts/BNum.sol +++ /dev/null @@ -1,88 +0,0 @@ -// This file is a flatenen verison of BNum -// where require(cond, string) where replaced by require(cond) -// To allow SkipRequire to work properly -// It won't be needed once https://github.com/trailofbits/manticore/issues/1593 is added - -contract BConst { - uint internal constant BONE = 10**18; - - uint internal constant MAX_BOUND_TOKENS = 8; - uint internal constant BPOW_PRECISION = BONE / 10**10; - - uint internal constant MIN_FEE = BONE / 10**6; - uint internal constant MAX_FEE = BONE / 10; - uint internal constant EXIT_FEE = BONE / 10000; - - uint internal constant MIN_WEIGHT = BONE; - uint internal constant MAX_WEIGHT = BONE * 50; - uint internal constant MAX_TOTAL_WEIGHT = BONE * 50; - uint internal constant MIN_BALANCE = BONE / 10**12; - uint internal constant MAX_BALANCE = BONE * 10**12; - - uint internal constant MIN_POOL_SUPPLY = BONE; - - uint internal constant MIN_BPOW_BASE = 1 wei; - uint internal constant MAX_BPOW_BASE = (2 * BONE) - 1 wei; - - uint internal constant MAX_IN_RATIO = BONE / 2; - uint internal constant MAX_OUT_RATIO = (BONE / 3) + 1 wei; - -} -contract BNum is BConst { - - - function badd(uint a, uint b) - internal pure - returns (uint) - { - uint c = a + b; - require(c >= a); - return c; - } - - function bsub(uint a, uint b) - internal pure - returns (uint) - { - (uint c, bool flag) = bsubSign(a, b); - require(!flag); - return c; - } - - function bsubSign(uint a, uint b) - internal pure - returns (uint, bool) - { - if (a >= b) { - return (a - b, false); - } else { - return (b - a, true); - } - } - - function bmul(uint a, uint b) - internal pure - returns (uint) - { - uint c0 = a * b; - require(a == 0 || c0 / a == b); - uint c1 = c0 + (BONE / 2); - require(c1 >= c0); - uint c2 = c1 / BONE; - return c2; - } - - function bdiv(uint a, uint b) - internal pure - returns (uint) - { - require(b != 0); - uint c0 = a * BONE; - require(a == 0 || c0 / a == BONE); // bmul overflow - uint c1 = c0 + (b / 2); - require(c1 >= c0); // badd require - uint c2 = c1 / b; - return c2; - } - -} \ No newline at end of file diff --git a/manticore/contracts/TBPoolJoinExitPool.sol b/manticore/contracts/TBPoolJoinExitPool.sol deleted file mode 100644 index 03487b51..00000000 --- a/manticore/contracts/TBPoolJoinExitPool.sol +++ /dev/null @@ -1,61 +0,0 @@ -import "./BNum.sol"; - -// This test is similar to TBPoolJoin but with an exit fee -contract TBPoolJoinExit is BNum { - - // joinPool models the BPool.joinPool behavior for one token - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - return tokenAmountIn; - } - - // exitPool models the BPool.exitPool behavior for one token - function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint exitFee = bmul(poolAmountIn, EXIT_FEE); - uint pAiAfterExitFee = bsub(poolAmountIn, exitFee); - uint ratio = bdiv(pAiAfterExitFee, poolTotal); - require(ratio != 0); - - uint bal = _records_t_balance; - uint tokenAmountOut = bmul(ratio, bal); - - return tokenAmountOut; - } - - - // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding - // issues to generate free pool token - function joinAndExitPool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public pure { - uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance); - - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - poolTotal = badd(poolTotal, poolAmountOut); - _records_t_balance = badd(_records_t_balance, tokenAmountIn); - - require(tokenAmountIn > 0); // prevent triggering the free token generation from joinPool - - require(poolTotal >= poolAmountIn); - uint tokenAmountOut = exitPool(poolAmountIn, poolTotal, _records_t_balance); - require(_records_t_balance >= tokenAmountOut); - - // We try to generate free pool share - require(poolAmountOut > poolAmountIn); - require(tokenAmountOut == tokenAmountIn); - } - -} \ No newline at end of file diff --git a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol b/manticore/contracts/TBPoolJoinExitPoolNoFee.sol deleted file mode 100644 index 703ca1d4..00000000 --- a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol +++ /dev/null @@ -1,62 +0,0 @@ -import "./BNum.sol"; - -// This test is similar to TBPoolJoinExit but with no exit fee -contract TBPoolJoinExitNoFee is BNum { - - bool public echidna_no_bug_found = true; - - // joinPool models the BPool.joinPool behavior for one token - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - return tokenAmountIn; - } - - // exitPool models the BPool.exitPool behavior for one token where no fee is applied - function exitPoolNoFee(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountIn, poolTotal); - require(ratio != 0); - - uint bal = _records_t_balance; - uint tokenAmountOut = bmul(ratio, bal); - - return tokenAmountOut; - } - - // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding - // issues to generate free pool token - function joinAndExitNoFeePool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public { - uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance); - - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - poolTotal = badd(poolTotal, poolAmountOut); - _records_t_balance = badd(_records_t_balance, tokenAmountIn); - - require(tokenAmountIn > 0); // prevent triggering the free token generation from joinPool - - require(poolTotal >= poolAmountIn); - uint tokenAmountOut = exitPoolNoFee(poolAmountIn, poolTotal, _records_t_balance); - require(_records_t_balance >= tokenAmountOut); - - // We try to generate free pool share - require(poolAmountOut > poolAmountIn); - require(tokenAmountOut == tokenAmountIn); - echidna_no_bug_found = false; - } - - -} \ No newline at end of file diff --git a/manticore/contracts/TBPoolJoinPool.sol b/manticore/contracts/TBPoolJoinPool.sol deleted file mode 100644 index 21441b0b..00000000 --- a/manticore/contracts/TBPoolJoinPool.sol +++ /dev/null @@ -1,32 +0,0 @@ -import "./BNum.sol"; - -contract TBPoolJoinPool is BNum { - - bool public echidna_no_bug_found = true; - - // joinPool models the BPool.joinPool behavior for one token - // A bug is found if poolAmountOut is greater than 0 - // And tokenAmountIn is 0 - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - public returns(uint) - { - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - require(poolAmountOut > 0); - require(tokenAmountIn == 0); - - echidna_no_bug_found = false; - } - -} \ No newline at end of file diff --git a/src/contracts/test/TMath.sol b/src/contracts/test/TMath.sol deleted file mode 100644 index b5cd0cf5..00000000 --- a/src/contracts/test/TMath.sol +++ /dev/null @@ -1,62 +0,0 @@ -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. - -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -pragma solidity 0.8.23; - -import "../BMath.sol"; -import "../BNum.sol"; - -// Contract to wrap internal functions for testing - -contract TMath is BMath { - - function calc_btoi(uint a) external pure returns (uint) { - return btoi(a); - } - - function calc_bfloor(uint a) external pure returns (uint) { - return bfloor(a); - } - - function calc_badd(uint a, uint b) external pure returns (uint) { - return badd(a, b); - } - - function calc_bsub(uint a, uint b) external pure returns (uint) { - return bsub(a, b); - } - - function calc_bsubSign(uint a, uint b) external pure returns (uint, bool) { - return bsubSign(a, b); - } - - function calc_bmul(uint a, uint b) external pure returns (uint) { - return bmul(a, b); - } - - function calc_bdiv(uint a, uint b) external pure returns (uint) { - return bdiv(a, b); - } - - function calc_bpowi(uint a, uint n) external pure returns (uint) { - return bpowi(a, n); - } - - function calc_bpow(uint base, uint exp) external pure returns (uint) { - return bpow(base, exp); - } - - function calc_bpowApprox(uint base, uint exp, uint precision) external pure returns (uint) { - return bpowApprox(base, exp, precision); - } -} diff --git a/src/contracts/test/TToken.sol b/src/contracts/test/TToken.sol deleted file mode 100644 index d9134492..00000000 --- a/src/contracts/test/TToken.sol +++ /dev/null @@ -1,136 +0,0 @@ -// This program is free software: you can redistribute it and/or modify -// it under the terms of the GNU General Public License as published by -// the Free Software Foundation, either version 3 of the License, or -// (at your option) any later version. - -// This program is distributed in the hope that it will be useful, -// but WITHOUT ANY WARRANTY; without even the implied warranty of -// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -// GNU General Public License for more details. - -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -pragma solidity 0.8.23; - -// Test Token - -contract TToken { - - string private _name; - string private _symbol; - uint8 private _decimals; - - address private _owner; - - uint internal _totalSupply; - - mapping(address => uint) private _balance; - mapping(address => mapping(address=>uint)) private _allowance; - - modifier _onlyOwner_() { - require(msg.sender == _owner, "ERR_NOT_OWNER"); - _; - } - - event Approval(address indexed src, address indexed dst, uint amt); - event Transfer(address indexed src, address indexed dst, uint amt); - - // Math - function add(uint a, uint b) internal pure returns (uint c) { - require((c = a + b) >= a); - } - function sub(uint a, uint b) internal pure returns (uint c) { - require((c = a - b) <= a); - } - - constructor( - string memory name, - string memory symbol, - uint8 decimals - ) public { - _name = name; - _symbol = symbol; - _decimals = decimals; - _owner = msg.sender; - } - - function name() public view returns (string memory) { - return _name; - } - - function symbol() public view returns (string memory) { - return _symbol; - } - - function decimals() public view returns(uint8) { - return _decimals; - } - - function _move(address src, address dst, uint amt) internal { - require(_balance[src] >= amt, "ERR_INSUFFICIENT_BAL"); - _balance[src] = sub(_balance[src], amt); - _balance[dst] = add(_balance[dst], amt); - emit Transfer(src, dst, amt); - } - - function _push(address to, uint amt) internal { - _move(address(this), to, amt); - } - - function _pull(address from, uint amt) internal { - _move(from, address(this), amt); - } - - function _mint(address dst, uint amt) internal { - _balance[dst] = add(_balance[dst], amt); - _totalSupply = add(_totalSupply, amt); - emit Transfer(address(0), dst, amt); - } - - function allowance(address src, address dst) external view returns (uint) { - return _allowance[src][dst]; - } - - function balanceOf(address whom) external view returns (uint) { - return _balance[whom]; - } - - function totalSupply() public view returns (uint) { - return _totalSupply; - } - - function approve(address dst, uint amt) external returns (bool) { - _allowance[msg.sender][dst] = amt; - emit Approval(msg.sender, dst, amt); - return true; - } - - function mint(address dst, uint256 amt) public _onlyOwner_ returns (bool) { - _mint(dst, amt); - return true; - } - - function burn(uint amt) public returns (bool) { - require(_balance[address(this)] >= amt, "ERR_INSUFFICIENT_BAL"); - _balance[address(this)] = sub(_balance[address(this)], amt); - _totalSupply = sub(_totalSupply, amt); - emit Transfer(address(this), address(0), amt); - return true; - } - - function transfer(address dst, uint amt) external returns (bool) { - _move(msg.sender, dst, amt); - return true; - } - - function transferFrom(address src, address dst, uint amt) external returns (bool) { - require(msg.sender == src || amt <= _allowance[src][msg.sender], "ERR_BTOKEN_BAD_CALLER"); - _move(src, dst, amt); - if (msg.sender != src && _allowance[src][msg.sender] != type(uint256).max) { - _allowance[src][msg.sender] = sub(_allowance[src][msg.sender], amt); - emit Approval(msg.sender, dst, _allowance[src][msg.sender]); - } - return true; - } -} diff --git a/src/contracts/test/echidna/TBPoolJoinExitPool.sol b/src/contracts/test/echidna/TBPoolJoinExitPool.sol deleted file mode 100644 index 7dcc7836..00000000 --- a/src/contracts/test/echidna/TBPoolJoinExitPool.sol +++ /dev/null @@ -1,66 +0,0 @@ -import "../../BNum.sol"; - -pragma solidity 0.8.23; - -// This test is similar to TBPoolJoin but with an exit fee -contract TBPoolJoinExit is BNum { - - bool public echidna_no_bug_found = true; - - // joinPool models the BPool.joinPool behavior for one token - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0, "ERR_MATH_APPROX"); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - return tokenAmountIn; - } - - // exitPool models the BPool.exitPool behavior for one token - function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint exitFee = bmul(poolAmountIn, EXIT_FEE); - uint pAiAfterExitFee = bsub(poolAmountIn, exitFee); - uint ratio = bdiv(pAiAfterExitFee, poolTotal); - require(ratio != 0, "ERR_MATH_APPROX"); - - uint bal = _records_t_balance; - uint tokenAmountOut = bmul(ratio, bal); - - return tokenAmountOut; - } - - - // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding - // issues to generate free pool token - function joinAndExitPool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) public { - uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance); - - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - poolTotal = badd(poolTotal, poolAmountOut); - _records_t_balance = badd(_records_t_balance, tokenAmountIn); - - require(tokenAmountIn > 0); // prevent triggering the free token generation from joinPool - - require(poolTotal >= poolAmountIn); - uint tokenAmountOut = exitPool(poolAmountIn, poolTotal, _records_t_balance); - require(_records_t_balance >= tokenAmountOut); - - // We try to generate free pool share - require(poolAmountOut > poolAmountIn); - require(tokenAmountOut == tokenAmountIn); - echidna_no_bug_found = false; - } - -} \ No newline at end of file diff --git a/src/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol b/src/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol deleted file mode 100644 index e79d8f73..00000000 --- a/src/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol +++ /dev/null @@ -1,66 +0,0 @@ -import "../../BNum.sol"; - -pragma solidity 0.8.23; - -// This test is similar to TBPoolJoinExit but with no exit fee -contract TBPoolJoinExitNoFee is BNum { - - bool public echidna_no_bug_found = true; - - // joinPool models the BPool.joinPool behavior for one token - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0, "ERR_MATH_APPROX"); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - return tokenAmountIn; - } - - // exitPool models the BPool.exitPool behavior for one token where no fee is applied - function exitPoolNoFee(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal pure returns(uint) - { - uint ratio = bdiv(poolAmountIn, poolTotal); - require(ratio != 0, "ERR_MATH_APPROX"); - - uint bal = _records_t_balance; - uint tokenAmountOut = bmul(ratio, bal); - - return tokenAmountOut; - } - - // This function model an attacker calling joinPool - exitPool and taking advantage of potential rounding - // issues to generate free pool token - function joinAndExitNoFeePool(uint poolAmountOut, uint poolAmountIn, uint poolTotal, uint _records_t_balance) - public - { - uint tokenAmountIn = joinPool(poolAmountOut, poolTotal, _records_t_balance); - - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - poolTotal = badd(poolTotal, poolAmountOut); - _records_t_balance = badd(_records_t_balance, tokenAmountIn); - - require(tokenAmountIn > 0); // prevent triggering the free token generation from joinPool - - require(poolTotal >= poolAmountIn); - uint tokenAmountOut = exitPoolNoFee(poolAmountIn, poolTotal, _records_t_balance); - require(_records_t_balance >= tokenAmountOut); - - // We try to generate free pool share - require(poolAmountOut > poolAmountIn); - require(tokenAmountOut == tokenAmountIn); - echidna_no_bug_found = false; - } - - -} \ No newline at end of file diff --git a/src/contracts/test/echidna/TBPoolJoinPool.sol b/src/contracts/test/echidna/TBPoolJoinPool.sol deleted file mode 100644 index 0c37972b..00000000 --- a/src/contracts/test/echidna/TBPoolJoinPool.sol +++ /dev/null @@ -1,34 +0,0 @@ -import "../../BNum.sol"; - -pragma solidity 0.8.23; - -contract TBPoolJoinPool is BNum { - - bool public echidna_no_bug_found = true; - - // joinPool models the BPool.joinPool behavior for one token - // A bug is found if poolAmountOut is greater than 0 - // And tokenAmountIn is 0 - function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - public returns(uint) - { - // We constraint poolTotal and _records_t_balance - // To have "realistic" values - require(poolTotal <= 100 ether); - require(poolTotal >= 1 ether); - require(_records_t_balance <= 10 ether); - require(_records_t_balance >= 10**6); - - uint ratio = bdiv(poolAmountOut, poolTotal); - require(ratio != 0, "ERR_MATH_APPROX"); - - uint bal = _records_t_balance; - uint tokenAmountIn = bmul(ratio, bal); - - require(poolAmountOut > 0); - require(tokenAmountIn == 0); - - echidna_no_bug_found = false; - } - -} \ No newline at end of file