mythril
mythril copied to clipboard
Consensys
Feature request: Please allow to specify initial state when analysing
Currently, anaylysis are performed with [SOMEGUY] and [ATTACKER] having initally a balance of 0 and no storage in the target smart contract (which can also means a token balances of 0).
But almost all smart contract real bug founds initally required buying a tiny amount of the token on an exchange or attacker sending an amount of ether in order to withdraw way more than he should.
Hi @ytrezq, The analysis is actually performed with a variable balance, but while reporting the vulnerability we try to show minimum possible balance for the attacker to exploit. And the SOMEGUY is used to buy tokens and the ATTACKER tries to steal the ether from the contract so it detects most real world vulnerabilities given adequate time and transaction length argument. You can check it out by trying out an example
@norhh : Ok, but what about the storage mappings ?
This is typicall for token which can be acquired using only off‑chain purchase. Or even when the onlycustodian address is in fact a robot/Oracle which can be triggered by anyone.
@ytrezq , some transactions are also executed by creator who tries to trigger some functions which might result in those storage changes. It's like this: constructor is executed by CREATOR. there will be a bunch of transactions from either SOME GUY, CREATOR, or ATTACKER SOME GUY and CREATOR change the state which the attacker tries to attack later, and this is handled without causing any state explosion.
@norhh : and sometimes owner isn’t the creator or some but not all actions of the owner aren’t able to be performed (typically off‑chain actions) by third party leading to false positives.
That’s why I’m requesting to specify initial storage key=value.
@ytrezq can you give an example as I am not quite getting it. sometimes owner isn’t the creator in that case SOME_GUY would be the owner. Also if you are talking about running analysis of onchain contracts then you can directly specify it's address to mythril and it will take the storage data onchain for that onchain contract.
@norhh : oh ! Simple : Etherrol ! For such on‑chain contract, mythril base it’s permissions on creator actions whereas the adress which has real owner priviliges isn’t controlled by creator but by a off‑chain robot and thus mythril doesn’t use the address controlled by the bot in analysis (where the address of the robot was specified in constructor and isn’t modifiable).
Oh! cool, we will try to add such addresses into our type of users.That would fix it right?
@norhh : It would be a first step. Thanks. Oh, also please notice the off‑chain robot of Etherrol is triggered by a log event fired by the contract address. Thus, if there is a possible attack the attacker first create a transaction firering the event which tells the robot what to do then, the robot performs a second transaction in a different block giving an unintended privilege to attacker which he/she can exploit in a third different transaction possibly in a third different block. And also, do not forget to fetch the address of such type of users from the blockhain in case of mainnet !
But what about tokens with onlyTokenholders modifiers at all function where the token can’t be minted ? Why not instead have a one rule them all option which would consist at specifying initial key=value storage state for [SOMEGUY] and [ATTACKER].
Why not instead have a one rule them all option which would consist at specifying key=value storage state for Mythril is a bytecode analyzer, so giving initial user inputted state for such storage is hard from user perspective because it should be inputted as raw storage Dict which is either key or Keccak(key, storage_slot) or Keccak(storage_slot) + key depending on data structure and the storage_slot is compiler dependent. Alternative option which is easier will be to add functions which are executed first in Mythril. Like this
contract Contract {
uint first;
... // some contract variables
...
modifier init_state{
require(first==0);
_;
first=1;
}
modifier other_functions{
require(first!=0);
_;
}
function initialise_storage() init_state{
array[958695489] = 9599;
// and some other initialisations
}
// And the rest of the contract would be below this, also add the modifier other_functions to rest of the functions.
...
...
}
@norhh : hard for newbie perspective, but easy to determine both the key and the value for someone like me (especially with the new low‑level storage change per transaction feature of Etherscan).
But yes, specifying the address of storage along it’s value for each contracts on a key=value scheme in binary is what I need.
Remember than on‑chain contract can’t be modified for adding debugging functions like the one you are suggesting. Especially if the source code isn’t available.
@ytrezq Another easier option in that case is that If the address and mainnet/testnet stuff is provided then mythril will try to use the onchain storage and the onchain code. You can use that feature till we add this feature. As we are working on other things like state merging, SMT strategy optimisations etc this might take some time.
@norhh : except it won’t works for tokens which requires msg.sender to have a non zero Balance in order to perform any actions.
@ytrezq for tokens which requires msg.sender to have a non zero Balance in order to perform any actions. All the actors are assumed to have some ether which they can use to buy token in some transaction.So it should work, if there is an example where it doesn't work then the reason for it shouldn't be this.
@norhh : All the actors are assumed to have some ether which they can use to buy token in some transaction Except if the contract as no mechanism for minting. So far Metronome is the only contract which you can purschase on chain through exchanging and without minting.
The result is mythril fails constantly to find anything because in no scenario [SOMEGUY] or [ATTACKER] or [CREATOR] get any token balance.
@ytrezq Transfer of tokens happen in smart contracts right(ERC20 based tokens)? If the Owner is the CREATOR(in most cases yes) then in one transaction he can transfer tokens to the ATTACKER, so that won't be a problem in most cases. But mythril doesn't detect stealing of tokens because it's hand to understand whether the increase of a number in a storage slot was intended by the programmer or not. One way to handle it is to put assertions at multiple locations and check for assertion failures with mythril.
@norhh : except if again at contract creation creaor isn’t the original recipient of the tokens.
Part1 of this Feature Request Merged! https://github.com/ConsenSys/mythril/pull/1252 It now just remains to specify storage.
@norhh : are you aware for example that because of the impossibility to specify address balance through raw storage address and value, that mythril fails to find the specific bug which was used in the dao hack even using 7 as loop bound limit and 6 as number of transaction ?
The competiting change you’re proposing wouldn’t solve that issue all while being harder to implement. This is definitely absurd.
@ytrezq, we will look into it soon. it's just that there was other stuff to deal with at the moment.
mythril fails to find the specific bug which was used in the dao hack even using 7 as loop bound limit and 6 as number of transaction If you are talking about the reentrancy then Mythril should detect it.
The competiting change you’re proposing wouldn’t solve that issue all while being harder to implement. This is definitely absurd. If you are talking about modifying the solidity contract change which I mentioned, It is definitely equivalent to mentioning key: value as the initial state.If it didn't work then it might be due to some bug in mythril which we will be happy to fix.
@norhh : If you are talking about the reentrancy then Mythril should detect it. It detects no longer usable re-entrancy but not the ones which were used for the hack.
As the functions involved in the real world 2016 hacks would require all someguy and attacker and creator to have a positive token balance all the way along, this is just expected.
but not the ones which were used for the hack. it doesn't detect re-entrancy as ether theft but it detects it as any state change after external calls, as that may result in re-entrancy.
As the functions involved in the real world 2016 hacks would require all someguy and attacker and creator to have a positive token balance all the way along Yeah, mythril reaches that state in most of the circumstances by executing a sequence of transactions. A smart contract can only change state by executing the functions inside it which mythril does. So it shouldn't have such a problem.
it doesn't detect re-entrancy as ether theft but it detects it as any state change after external calls, as that may result in re-entrancy. No it doesn’t detect the state change after sending, at least not the ones which could and had been used for the hack (since the one it reports requires having a block.timestamp value inferior to the last ones in other blocks).
It’s not possible to have a storage state which both allows tokens generation and to hack the contract using the 2016 methods. So it doesn’t work.
It depends on how you run it. If it's run using an address then it uses the storage onchain which may not be exploitable. Running the contract using source code should work as it starts with fresh storage and can execute anything.
@norhh but you stated that https://github.com/ConsenSys/mythril/pull/1252 never use on chain storage so that it only works only if the address is specified in the source code. Anyway, after multi level transactions I suppose it makes it’s simulation based it’s own previous simulated storage changes, correct?
I mean mythril uses onchain storage if you are accessing onchain contract, something like myth analyze --rpc infura-mainnet -a <address>
only works only if the address is specified in the source code Or if you specify that address as a command line argument.
Anyway, after multi level transactions I suppose it makes it’s simulation based it’s own previous simulated storage changes, correct I am not sure what it means, mythril creates a contract from the source code and then executes multiple sequence of transactions locally which mutates the local storage.