Increase max_depth during constructor execution

[muellerberndt]

Description

When considering the symbolic execution of the contract creation bytecode, then a low max-depth setting can result in no contract being created. Therefore we'll set a minimum max depth of 64 for these types of transactions.

Requirements

• during contract creation the following max depth is considered max(64, max_depth) where max_depth is the user provided value
• during normal transactions max_depth is used as the max depth

Background

For some contracts such as BECToken the default max-depth is insufficient:

$ myth -x BECToken.sol:BecToken -v1
root[22918] INFO Using INFURA for RPC queries
root[22918] INFO LASER EVM initialized with dynamic loader: <mythril.support.loader.DynLoader object at 0x109de3048>
root[22918] INFO Found 0 detection modules
root[22918] INFO Starting contract creation transaction
root[22918] INFO Finished contract creation, found 0 open states
root[22918] WARNING No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout)
root[22918] INFO Starting message call transaction, iteration: 0
root[22918] INFO Number of new instructions covered in tx 0: 0
root[22918] INFO Starting message call transaction, iteration: 1
root[22918] INFO Number of new instructions covered in tx 1: 0
root[22918] INFO Finished symbolic execution
root[22918] INFO 23 nodes, 22 edges, 357 total states
root[22918] INFO Starting analysis
root[22918] INFO Found 11 detection modules
root[22918] INFO Executing DELEGATECALL Usage in Fallback Function
root[22918] INFO Executing Dependence of Predictable Variables
root[22918] INFO Executing Deprecated Operations
root[22918] INFO Executing Ether Thief
root[22918] INFO Executing Reachable Exceptions
root[22918] INFO Executing External Calls
root[22918] INFO Executing Integer Overflow and Underflow
root[22918] INFO Executing Multiple Sends
root[22918] INFO Executing Unprotected Suicide
root[22918] INFO Executing Transaction Order Dependence
root[22918] INFO Executing Unchecked Return Value
The analysis was completed successfully. No issues were detected.

It works if --max-depth is set to 32, but this makes the main analysis run take very long.

I propose setting max_depth to a high fixed value (e.g. 64) for the contract creation transaction instead of using the user-provided value.

[JoranHonig]

How about using max(max_depth, 64). So the user can still add more if necessary

[muellerberndt]

Yeah, that sounds good.

[muellerberndt]

I tried adding a hack in symbolic.py, didn't work (laser still returns 0 open states).

It works with --max-depth 64 on the cmdline though.

EDIT: OK, max_depth is used only to initialize the search strategy so changing it later doesn't do anything.

Maybe we can add a strategy arg to sym_exec to override the default strategy?

[JoranHonig]

@b-mueller We can probably set the overall max depth to 64, as the timeouts are being used now to limit execution duration vs max depth

[norhh]

@JoranHonig , how about the gas based depth that we were talking in some meeting. doing both depth+ gas based pruning might also be good when increasing it to 64.

[JoranHonig]

I'm not sure that that would have too much priority right now

[norhh]

We can probably set the overall max depth to 64, as the timeouts are being used now to limit execution duration vs max depth If we are increasing max-depth to 64, then changing default search to bfs might be good, WDYT?