Low/High Level Architecture?

[Danc2050]

I am writing a MS thesis on the Ethereum blockchain as a graduation requirement. My primary tool of use was Mythril (why I have made a lot of posts on here lately :smile:).

But I have been having a tough time finding out how Mythril actually works. The documentation does not really say much of anything on how Mythril works at a high level. For example, my current understanding is: potentially pulls bytecode from chain, gets msg.data and separates out the contracts 4-byte functions, uses the disassembler on that (?), runs symbolic execution using some symbolic voodoo (this is my current understanding). Neither can I find a low level explanation (e.g., with regards to catching specific vulnerabilities).

I know from talking on here that the z3 solver does quite a bit of work, but I don't know much about that either. I can read some of the code, but its not always clear to me what is going on (likely my inexperience, not bad code). I am using the myth -v4 analyze -1 -a [address] command. Is there any resource I can pull from to help me write this portion of my thesis? I want to represent Mythril accurately. Thank you.

[norhh]

Mythril also runs on any solidity file provided offchain. myth a <file_path> This article might give a high level working of mythril https://medium.com/@joran.honig/introduction-to-mythril-classic-and-symbolic-execution-ef59339f259b. Mythril converts source code to bytecode, Executes a bunch of transactions with symbolic calldata and caller.

[JoranHonig]

The following document might also help: https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf

This is already somewhat older, but many of the high level aspects will be valid