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

Concolic execution requires additional plugin. #1626

Closed bre4kpo1nt closed 2 years ago

bre4kpo1nt commented 2 years ago

Hello,

I am trying to use Mythril to perform concolic execution, but it seems that a plugin named "myth_concolic_execution" is required in the first place. And I don't know where it is and how to install it.

https://github.com/ConsenSys/mythril/blob/6b34febd5ec53bd61c2115013bda1e21164ee96d/mythril/interfaces/cli.py#L296-L304

norhh commented 2 years ago

Hi @break1ngpoint, That module might not be much of a help. If you want to restrict transactions that you want to execute, you can always try --transaction-sequence "[[<list of candidate function hashes for 1st tx>], [list of candidate function hashes for 2nd tx], ....[list of candidate function hashes for nth tx]]". For example something like --transaction-sequence "[[0xe46dcfeb], [0xcbf0b0c0]]". This will only execute transactions 0xe46dcfeb and 0xcbf0b0c0 in that following order of function hashes.

bre4kpo1nt commented 2 years ago

Hi @break1ngpoint, That module might not be much of a help. If you want to restrict transactions that you want to execute, you can always try --transaction-sequence "[[<list of candidate function hashes for 1st tx>], [list of candidate function hashes for 2nd tx], ....[list of candidate function hashes for nth tx]]". For example something like --transaction-sequence "[[0xe46dcfeb], [0xcbf0b0c0]]". This will only execute transactions 0xe46dcfeb and 0xcbf0b0c0 in that following order of function hashes.

Thanks for your advice. But I still have interest in the "concolic" command because the help message says that it is able to flip the desired branches. So how can I test with this command?

norhh commented 2 years ago

It is meant to be used with fuzzing as this mode does not detect any vulnerabilities, it just flips branches and gives out an output to be used by a fuzzer.

bre4kpo1nt commented 2 years ago

It is meant to be used with fuzzing as this mode does not detect any vulnerabilities, it just flips branches and gives out an output to be used by a fuzzer.

Got it. So how can I install the required plugin named "myth_concolic_execution"? It is not located in this repo.

norhh commented 2 years ago

At this moment, that plugin isn't public.

bre4kpo1nt commented 2 years ago

At this moment, that plugin isn't public.

All right, anyway, thanks again.