trailofbits
Increase the default size of the symbolic value when using manticore EVM from command line
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.
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.
