Slither
pip3 install slither-analyzer
Manticore
pip3 install manticore
Echidna See Echidna Installation.
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox
solc-select 0.5.12
cd /home/training
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/.
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.
| Description | Name | Contract | Finding | Status |
|---|---|---|---|---|
| An attacker cannot steal assets from a public pool. | attacker_token_balance |
TBPoolBalance |
FAILED (#193) | Fixed |
| An attacker cannot force the pool balance to be out-of-sync. | pool_record_balance |
TBPoolBalance |
PASSED | |
An attacker cannot generate free pool tokens with joinPool (1, 2). |
joinPool |
TBPoolJoinPool |
FAILED (#204) | Mitigated |
Calling joinPool-exitPool does not lead to free pool tokens (no fee) (1, 2). |
joinPool |
TBPoolJoinExitNoFee |
FAILED (#205) | Mitigated |
Calling joinPool-exitPool does not lead to free pool tokens (with fee) (1, 2). |
joinPool |
TBPoolJoinExit |
FAILED (#205) | Mitigated |
Calling exitswapExternAmountOut does not lead to free asset (1). |
exitswapExternAmountOut |
TBPoolExitSwap |
FAILED (#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.
| Description | Name | Contract | Finding | Status |
|---|---|---|---|---|
If the controller calls setController, then the getController() should return the new controller. |
controller_should_change |
TBPoolController |
PASSED | |
The controller cannot be changed to a null address (0x0). |
controller_cannot_be_null |
TBPoolController |
FAILED (#198) | WONT FIX |
| The controller cannot be changed by other users. | no_other_user_can_change_the_controller |
TBPoolController |
PASSED | |
| The sum of normalized weight should be 1 if there are tokens binded. | valid_weights |
TBPoolLimits |
FAILED (#208 | Mitigated |
The balances of all the tokens are greater or equal than MIN_BALANCE. |
min_token_balance |
TBPoolLimits |
FAILED (#210) | WONT FIX |
The weight of all the tokens are less or equal than MAX_WEIGHT. |
max_weight |
TBPoolLimits |
PASSED | |
The weight of all the tokens are greater or equal than MIN_WEIGHT. |
min_weight |
TBPoolLimits |
PASSED | |
The swap fee is less or equal tan MAX_FEE. |
min_swap_free |
TBPoolLimits |
PASSED | |
The swap fee is greater or equal than MIN_FEE. |
max_swap_free |
TBPoolLimits |
PASSED | |
| An user can only swap in less than 50% of the current balance of tokenIn for a given pool. | max_swapExactAmountIn |
TBPoolLimits |
FAILED (#212) | Fixed |
| An user can only swap out less than 33.33% of the current balance of tokenOut for a given pool. | max_swapExactAmountOut |
TBPoolLimits |
FAILED (#212) | Fixed |
If a token is bounded, the getSpotPrice should never revert. |
getSpotPrice_no_revert |
TBPoolNoRevert |
PASSED | |
If a token is bounded, the getSpotPriceSansFee should never revert. |
getSpotPriceSansFee_no_revert |
TBPoolNoRevert |
PASSED | |
Calling swapExactAmountIn with a small value of the same token should never revert. |
swapExactAmountIn_no_revert |
TBPoolNoRevert |
PASSED | |
Calling swapExactAmountOut with a small value of the same token should never revert. |
swapExactAmountOut_no_revert |
TBPoolNoRevert |
PASSED | |
| If a user joins pool and exits it with the same amount, the balances should keep constant. | joinPool_exitPool_balance_consistency |
TBPoolJoinExit |
PASSED | |
If a user joins pool and exits it with a larger amount, exitPool should revert. |
impossible_joinPool_exitPool |
TBPoolJoinExit |
PASSED | |
It is not possible to bind more than MAX_BOUND_TOKENS. |
getNumTokens_less_or_equal_MAX_BOUND_TOKENS |
TBPoolBind |
PASSED | |
| It is not possible to bind more than once the same token. | bind_twice |
TBPoolBind |
PASSED | |
| It is not possible to unbind more than once the same token. | unbind_twice |
TBPoolBind |
PASSED | |
| It is always possible to unbind a token. | all_tokens_are_unbindable |
TBPoolBind |
PASSED | |
| All tokens are rebindable with valid parameters. | all_tokens_are_rebindable_with_valid_parameters |
TBPoolBind |
PASSED | |
| It is not possible to rebind an unbinded token. | rebind_unbinded |
TBPoolBind |
PASSED | |
| Only the controller can bind. | when_bind and only_controller_can_bind |
TBPoolBind |
PASSED | |
| If a user that is not the controller, tries to bind, rebind or unbind, the operation will revert. | when_bind, when_rebind and when_unbind |
TBPoolBind |
PASSED | |
Transfer tokens to the null address (0x0) causes a revert |
transfer_to_zero and transferFrom_to_zero |
TBTokenERC20 |
FAILED (#197) | WONT FIX |
The null address (0x0) owns no tokens |
zero_always_empty |
TBTokenERC20 |
FAILED | WONT FIX |
| Transfer a valid amout of tokens to non-null address reduces the current balance | transferFrom_to_other and transfer_to_other |
TBTokenERC20 |
PASSED | |
| Transfer an invalid amout of tokens to non-null address reverts or returns false | transfer_to_user |
TBTokenERC20 |
PASSED | |
| Self transfer a valid amout of tokens keeps the current balance constant | self_transferFrom and self_transfer |
TBTokenERC20 |
PASSED | |
| Approving overwrites the previous allowance value | approve_overwrites |
TBTokenERC20 |
PASSED | |
The totalSupply is a constant |
totalSupply_constant |
TBTokenERC20 |
PASSED | |
The balances are consistent with the totalSupply |
totalSupply_balances_consistency and balance_less_than_totalSupply |
TBTokenERC20 |
PASSED |
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 |
TBPoolJoinPool |
FAILED (#204) |
Calling joinPool-exitPool does not lead to free pool tokens (no fee). |
TBPoolJoinExitNoFee.py |
TBPoolJoinExitPoolNoFee |
FAILED (#205) |
Calling joinPool-exitPool does not lead to free pool tokens (with fee). |
TBPoolJoinExit.py |
TBPoolJoinExit |
FAILED (#205) |