Request for Guidance on Mythril’s Code Transformation Process

[matheus-junio-da-silva]

Dear Mythril Developers,

I hope this message finds you well. My name is M. Silva, and I’m a Computer Science student currently working on a project that involves understanding how Mythril transforms smart contract code for analysis.

I’ve been diving deep into the documentation and even debugging the codebase, but I’m struggling to fully grasp the intricacies, particularly when it comes to the symbolic execution process. I understand this is a foundational aspect of Mythril, and I truly want to comprehend it, not just for my project but also to deepen my understanding of these critical security concepts.

This project is very important to me, and I’m reaching out with a heartfelt request: could you kindly provide some guidance or resources that might help clarify how Mythril processes and transforms code during analysis? I’d be immensely grateful for any insight you could share.

Thank you so much for your time and for the incredible work you’ve done with Mythril. It’s an inspiring tool, and I hope to understand it better with your help.

Warm regards,
M. Silva

[norhh]

Hi, Mythril operates on bytecode. So, each instruction has to be symbolically modeled as in this file: https://github.com/Consensys/mythril/blob/develop/mythril/laser/ethereum/instructions.py.

Consider JUMPI instruction as an example.
The condition and the jump destination are popped from the stack (EVM is a stack based machine). Usually, if the condition is true, program counter jumps to the jump destination, otherwise, the program counter is just incremented. In symbolic execution, when the condition is a symbol and can resolve to both true and false, both the paths get added to the list of states. Hence, this instruction returns two states.

Whenever an instruction is being evaluated by symbolic vm, this code is wrapped by analysis modules. One such example is arbitrary jump destination module. This module wraps around JUMP and JUMPI instructions as prehooks, so, this analysis module is executed before symbolically executing the instructions JUMP and JUMPI. This analysis module returns an issue if the jump destination popped from the stack (the jump dest still exists in stack during pre_hooks) is symbolic rather than a concrete value.

Feel free to ask me any questions.