Installation
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
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 |
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.
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 |
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 |
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 |
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) |