From 2d88257fb27ad3c84b5166304a342e66055a81b3 Mon Sep 17 00:00:00 2001 From: Mike McDonald Date: Wed, 26 Feb 2020 12:52:51 -0600 Subject: [PATCH] Audit cleanup (#216) * update echidna, manticore tests. cleanup slither filters * update readme and fix manticore compilation * fix slither filter for informational --- .circleci/config.yml | 2 +- .gitignore | 3 +- .solcover.js | 3 +- Audit.md | 87 +++++++++---------- README.md | 13 +-- contracts/test/echidna/TBPoolJoinExitPool.sol | 6 +- .../test/echidna/TBPoolJoinExitPoolNoFee.sol | 10 ++- contracts/test/echidna/TBPoolJoinPool.sol | 2 + echidna/TBPoolJoinExit.sol | 2 + echidna/TBPoolLimits.sol | 13 +-- manticore/TBPoolJoinExitNoFee.py | 4 +- manticore/TBPoolJoinPool.py | 3 +- manticore/contracts/BNum.sol | 2 - manticore/contracts/TBPoolJoinExitPool.sol | 6 +- .../contracts/TBPoolJoinExitPoolNoFee.sol | 6 +- 15 files changed, 82 insertions(+), 80 deletions(-) diff --git a/.circleci/config.yml b/.circleci/config.yml index 9b521e62..28ec01f7 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -88,7 +88,7 @@ jobs: command: truffle compile - run: name: Slither - command: slither . --filter-paths test --exclude=naming-convention,unused-state,solc-version + command: slither . --filter-paths test --exclude=naming-convention,unused-state,solc-version,constable-states,external-function,reentrancy-events workflows: version: 2 diff --git a/.gitignore b/.gitignore index fa1c825b..e8f2d013 100644 --- a/.gitignore +++ b/.gitignore @@ -4,4 +4,5 @@ node_modules coverage.json coverage/ yarn-error.log -crytic-export \ No newline at end of file +crytic-export +mcore_* \ No newline at end of file diff --git a/.solcover.js b/.solcover.js index bd07c7e3..5e08b372 100644 --- a/.solcover.js +++ b/.solcover.js @@ -1,9 +1,8 @@ module.exports = { port: 8555, skipFiles: [ - 'BStub.sol', 'Migrations.sol', 'test' ], - testrpcOptions: "-p 8555 -d --allowUnlimitedContractSize" + testrpcOptions: "-p 8555 -d" }; \ No newline at end of file diff --git a/Audit.md b/Audit.md index 88ac8a01..b3239b49 100644 --- a/Audit.md +++ b/Audit.md @@ -46,14 +46,14 @@ To test a property, run `echidna-test echidna/CONTRACT_file.sol CONTRACT_name -- ## General Properties -| Description | Name | Contract | 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))| -| 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))| -| 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))| -| 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))| -| 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))| +| 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. @@ -62,42 +62,41 @@ To test a property, run `echidna-test echidna/CONTRACT_file.sol CONTRACT_name -- ## Unit-test-based Properties -| Description | Name | Contract | 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))| -| 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)| -| The balances of all the tokens are less or equal than `MAX_BALANCE`. | [`max_token_balance`](echidna/TBPoolLimits.sol#L54-L63) | [`TBPoolLimits`](echidna/TBPoolLimits.sol) |**FAILED** ([#210](https://github.com/balancer-labs/balancer-core/issues/210))| -| 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)) | -| 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))| -| 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))| -| 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))| -| The null address (`0x0`) owns no tokens | [`zero_always_empty`](echidna/TBTokenERC20.sol#L34-L36) | [`TBTokenERC20`](echidna/TBTokenERC20.sol) |**FAILED**| -| 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**| +| 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 diff --git a/README.md b/README.md index c52bfc8e..8583cf1b 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ your portfolio by following arbitrage opportunities. Balancer is based on an N-dimensional invariant surface which is a generalization of the constant product formula described by Vitalik Buterin and proven viable by the popular Uniswap dapp. -


🍂 bronze release 🍂

+## 🍂 Bronze Release 🍂 The *🍂Bronze Release🍂* is the first of 3 planned releases of the Balancer Protocol. Bronze emphasizes code clarity for audit and verification, and does not go to great lengths to optimize for gas. @@ -32,8 +32,12 @@ The *❄️Silver Release❄️* will bring many gas optimizations and architect The *☀️Golden Release☀️* will introduce a curious new liquidity mechanism to the market. +## Documentation -### Using the ABI definitions +The full documentation can be found at [https://docs.balancer.finance](https://docs.balancer.finance) + + +## Development Most users will want to consume the ABI definitions for BFactory and BPool. @@ -73,8 +77,7 @@ relDif : 1.6464292361378058e-12) ✓ exitswap_ExternAmountOut (537ms) ``` -Complete API docs are available at [https://balancer.finance/api](https://balancer.finance/api) -(or see the [markdown source](https://github.com/balancer-labs/balancer-finance/blob/master/api.md) if it's not available). -Look in the [`test/`](https://github.com/balancer-labs/balancer-core/tree/master/test) directory for working examples in a mock environment. +Complete API docs are available at [https://docs.balancer.finance/smart-contracts/api](https://docs.balancer.finance/smart-contracts/api) +

⊙

diff --git a/contracts/test/echidna/TBPoolJoinExitPool.sol b/contracts/test/echidna/TBPoolJoinExitPool.sol index 1c5acd0d..625f122a 100644 --- a/contracts/test/echidna/TBPoolJoinExitPool.sol +++ b/contracts/test/echidna/TBPoolJoinExitPool.sol @@ -1,5 +1,7 @@ import "../../BNum.sol"; +pragma solidity 0.5.12; + // This test is similar to TBPoolJoin but with an exit fee contract TBPoolJoinExit is BNum { @@ -7,7 +9,7 @@ contract TBPoolJoinExit is BNum { // joinPool models the BPool.joinPool behavior for one token function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountOut, poolTotal); require(ratio != 0, "ERR_MATH_APPROX"); @@ -20,7 +22,7 @@ contract TBPoolJoinExit is BNum { // exitPool models the BPool.exitPool behavior for one token function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal returns(uint) + internal pure returns(uint) { uint exitFee = bmul(poolAmountIn, EXIT_FEE); uint pAiAfterExitFee = bsub(poolAmountIn, exitFee); diff --git a/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol b/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol index 85b4aa95..5b311147 100644 --- a/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol +++ b/contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol @@ -1,5 +1,7 @@ import "../../BNum.sol"; +pragma solidity 0.5.12; + // This test is similar to TBPoolJoinExit but with no exit fee contract TBPoolJoinExitNoFee is BNum { @@ -7,7 +9,7 @@ contract TBPoolJoinExitNoFee is BNum { // joinPool models the BPool.joinPool behavior for one token function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountOut, poolTotal); require(ratio != 0, "ERR_MATH_APPROX"); @@ -20,7 +22,7 @@ contract TBPoolJoinExitNoFee is BNum { // 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 returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountIn, poolTotal); require(ratio != 0, "ERR_MATH_APPROX"); @@ -33,7 +35,9 @@ contract TBPoolJoinExitNoFee is BNum { // 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 { + 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 diff --git a/contracts/test/echidna/TBPoolJoinPool.sol b/contracts/test/echidna/TBPoolJoinPool.sol index 6ed3444d..d43ec43b 100644 --- a/contracts/test/echidna/TBPoolJoinPool.sol +++ b/contracts/test/echidna/TBPoolJoinPool.sol @@ -1,5 +1,7 @@ import "../../BNum.sol"; +pragma solidity 0.5.12; + contract TBPoolJoinPool is BNum { bool public echidna_no_bug_found = true; diff --git a/echidna/TBPoolJoinExit.sol b/echidna/TBPoolJoinExit.sol index 3012a7f1..a23c60b0 100644 --- a/echidna/TBPoolJoinExit.sol +++ b/echidna/TBPoolJoinExit.sol @@ -4,6 +4,8 @@ import "./CryticInterface.sol"; contract TBPoolJoinExit is CryticInterface, BPool { + uint MAX_BALANCE = BONE * 10**12; + constructor() public { MyToken t; t = new MyToken(uint(-1), address(this)); diff --git a/echidna/TBPoolLimits.sol b/echidna/TBPoolLimits.sol index 85ba17d9..4493db7a 100644 --- a/echidna/TBPoolLimits.sol +++ b/echidna/TBPoolLimits.sol @@ -4,6 +4,8 @@ import "./CryticInterface.sol"; contract TBPoolLimits is CryticInterface, BPool { + uint MAX_BALANCE = BONE * 10**12; + constructor() public { MyToken t; t = new MyToken(uint(-1), address(this)); @@ -50,17 +52,6 @@ contract TBPoolLimits is CryticInterface, BPool { // if there are tokens, the normalized weight should be 1 return (nw == 1); } - - function echidna_max_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 less than `MAX_BALACE` - if (this.getBalance(address(current_tokens[i])) > MAX_BALANCE) - return false; - } - // if there are no tokens, return true - return true; - } function echidna_min_token_balance() public returns (bool) { address[] memory current_tokens = this.getCurrentTokens(); diff --git a/manticore/TBPoolJoinExitNoFee.py b/manticore/TBPoolJoinExitNoFee.py index 16598a0b..4f049712 100644 --- a/manticore/TBPoolJoinExitNoFee.py +++ b/manticore/TBPoolJoinExitNoFee.py @@ -34,8 +34,8 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments): skipRequire = SkipRequire() m.register_plugin(skipRequire) -TestBpool = m.solidity_create_contract('./manticore/contracts/TestJoinExitNoFee.sol', - contract_name='TestJoinExitNoFee', +TestBpool = m.solidity_create_contract('./manticore/contracts/TBPoolJoinExitNoFee.sol', + contract_name='TBPoolJoinExitNoFee', owner=user) print(f'TestJoinExit deployed {hex(TestBpool.address)}') diff --git a/manticore/TBPoolJoinPool.py b/manticore/TBPoolJoinPool.py index 051d4484..09b16875 100644 --- a/manticore/TBPoolJoinPool.py +++ b/manticore/TBPoolJoinPool.py @@ -42,10 +42,9 @@ def will_evm_execute_instruction_callback(self, state, instruction, arguments): # 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.joinPool(poolAmountOut, poolAmountIn, poolTotal, _records_t_balance) +TestBpool.joinPool(poolAmountOut, poolTotal, _records_t_balance) print(f'joinPool Called') diff --git a/manticore/contracts/BNum.sol b/manticore/contracts/BNum.sol index be5910ad..e6708bd3 100644 --- a/manticore/contracts/BNum.sol +++ b/manticore/contracts/BNum.sol @@ -1,5 +1,3 @@ -pragma solidity 0.5.12; - // This file is a flatenen verison of BNum // where require(cond, string) where replaced by require(cond) // To allow SkipRequire to work properly diff --git a/manticore/contracts/TBPoolJoinExitPool.sol b/manticore/contracts/TBPoolJoinExitPool.sol index 9f9b092d..03487b51 100644 --- a/manticore/contracts/TBPoolJoinExitPool.sol +++ b/manticore/contracts/TBPoolJoinExitPool.sol @@ -5,7 +5,7 @@ contract TBPoolJoinExit is BNum { // joinPool models the BPool.joinPool behavior for one token function joinPool(uint poolAmountOut, uint poolTotal, uint _records_t_balance) - internal returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountOut, poolTotal); require(ratio != 0); @@ -18,7 +18,7 @@ contract TBPoolJoinExit is BNum { // exitPool models the BPool.exitPool behavior for one token function exitPool(uint poolAmountIn, uint poolTotal, uint _records_t_balance) - internal returns(uint) + internal pure returns(uint) { uint exitFee = bmul(poolAmountIn, EXIT_FEE); uint pAiAfterExitFee = bsub(poolAmountIn, exitFee); @@ -34,7 +34,7 @@ contract TBPoolJoinExit is BNum { // 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 { + 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 diff --git a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol b/manticore/contracts/TBPoolJoinExitPoolNoFee.sol index b443812d..703ca1d4 100644 --- a/manticore/contracts/TBPoolJoinExitPoolNoFee.sol +++ b/manticore/contracts/TBPoolJoinExitPoolNoFee.sol @@ -3,9 +3,11 @@ 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 returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountOut, poolTotal); require(ratio != 0); @@ -18,7 +20,7 @@ contract TBPoolJoinExitNoFee is BNum { // 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 returns(uint) + internal pure returns(uint) { uint ratio = bdiv(poolAmountIn, poolTotal); require(ratio != 0);