Audit cleanup (#216)

* update echidna, manticore tests. cleanup slither filters

* update readme and fix manticore compilation

* fix slither filter for informational

.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

.gitignore

@@ -4,4 +4,5 @@ node_modules
 coverage.json
 coverage/
 yarn-error.log
-crytic-export
+crytic-export
+mcore_*

.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"
 };

README.md

@@ -24,16 +24,20 @@ 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.
 
-<h2 align=center><br/><code>🍂 bronze release 🍂</code></h2>
+## 🍂 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.
 
 The *❄️Silver Release❄️* will bring many gas optimizations and architecture changes that will reduce transaction overhead and enable more flexibility for managed pools.
 
 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)
+
 
 <p align=center>⊙</p>

contracts/test/echidna/TBPoolJoinExitPool.sol

@@ -1,13 +1,15 @@
 import "../../BNum.sol";
 
+pragma solidity 0.5.12;
+
 //  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 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);

contracts/test/echidna/TBPoolJoinExitPoolNoFee.sol

@@ -1,13 +1,15 @@
 import "../../BNum.sol";
 
+pragma solidity 0.5.12;
+
 //  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, "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

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;

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));

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();

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)}')

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')
 

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

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

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);