Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Increase the default size of the symbolic value when using manticore EVM from command line #2462

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

ggrieco-tob
Copy link
Contributor

When manticore is used during audits, it's very common to take a piece of code and abstract the state variables as parameters, to allow our tool to explore any possible state (even at the cost of false positives). This increases the list of parameters in functions. Unfortunately with the current size of symbolic inputs, this can happen:

contract C {
  function f(uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256, uint256 x) public {
    require(x > 0);
  }
}

Manticore silently fails to produce live states:

$ manticore long.sol --txlimit 1
2021-06-23 14:48:15,905: [32264] m.main:INFO: Registered plugins: <class 'manticore.core.plugin.IntrospectionAPIPlugin'>, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
2021-06-23 14:48:15,905: [32264] m.main:INFO: Beginning analysis
2021-06-23 14:48:15,907: [32264] m.e.manticore:INFO: Starting symbolic create contract
2021-06-23 14:48:16,091: [32264] m.e.manticore:INFO: Starting symbolic transaction: 0
2021-06-23 14:48:16,736: [32264] m.e.manticore:INFO: 0 alive states, 2 terminated states
2021-06-23 14:48:16,774: [32264] m.c.manticore:INFO: Results in /home/g/Code/manticore/mcore_mkqlwra1
2021-06-23 14:48:16,775: [32264] m.c.manticore:INFO: Total time: 0.6813325881958008

This PR doubles the amount of symbolic bytes to mitigate this issue.

@ehennenfent
Copy link
Contributor

Per the meeting, since this could increase the amount of symbolic data Manticore has to deal with in simple cases, we should look into using the information crytic-compile provides us to see if we can choose the exact number of symbolic bytes we need based on the ABI of the contract functions. This will only work for fixed-size arguments, but would be more efficient than always just guessing, as we currently do.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants