Feature request: Please allow to specify initial state when analysing

[ytrezq]

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.

[norhh]

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

[ytrezq]

@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.

[norhh]

@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.

[ytrezq]

@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.

[norhh]

@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.

[ytrezq]

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

[norhh]

Oh! cool, we will try to add such addresses into our type of users.That would fix it right?

[ytrezq]

@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].

[norhh]

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

[ytrezq]

@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.

[norhh]

@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.

[ytrezq]

@norhh : except it won’t works for tokens which requires msg.sender to have a non zero Balance in order to perform any actions.

[norhh]

@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.

[ytrezq]

@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.