search

Consensys / mythril

Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Rootstock, Tron and other EVM-compatible blockchains.
https://mythx.io/
MIT License
3.84k stars 736 forks source link

Please support dumping all found states regardless of vulnerabilties found. #1455

Open ytrezq opened 3 years ago

ytrezq commented 3 years ago

Using the same state mergin branch of Mythril, the analysis of smart contract doing only 1 thing (taking or withdrawing a deposit of a fixed 1 amount) and neverless it found 729 differrent states.

By reading the source code, I m failing to find how they can be reached and what they does. And since Mythril often miss potential funds theft or Integer overflow, this is something which can definitely help manual anaylysis.

Would it be possible to dump all states being found in general? Please note this involve dumping contract s storage change (addresses s value from contract addresses) in addition to the transaction sequence in order to reach them.

norhh commented 3 years ago

@ytrezq , it will take days to dump all the states because serializing z3 constraints and storage will make it huge. You can print the information you need in this function https://github.com/ConsenSys/mythril/blob/9a2572c3d38296091fea5e4e91e8c0fffa489afa/mythril/laser/ethereum/svm.py#L189 self.open_states has all the states. It's of type GlobalState, you can choose to print the information as it is of no use to dump everything due to its inefficiency.

ytrezq commented 3 years ago

I am not talking about serializing z3 but just dumping transaction sequences alang storage changes un text format. Would it be possible to do this?

norhh commented 3 years ago

storage is an SMT array, so it should be serialized.

ytrezq commented 3 years ago

How is it possible exactly? Are eth balance changes are in the same array?

norhh commented 3 years ago

storage access with symbolic indices need an SMT array for an accurate representation