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.

[matheus-junio-da-silva]

Dear @norhh,
I hope you're doing well!

First, thank you so much for your detailed and thoughtful response to my previous question—it really helped me make significant progress in understanding the symbolic execution process in Mythril. Since our last interaction, I’ve been studying the parts of the codebase you mentioned, particularly the symbolic modeling in instructions.py, and I also started exploring the external_calls detection module.

However, I’ve hit a roadblock that I was hoping you could help me with. You’re the only person I can think of who might have the insight I need, and I’d be immensely grateful for any guidance. I know this is a complex topic, and I’ve been working day and night to understand it better, but I feel a bit stuck. If my questions seem too basic, I sincerely apologize—it’s just that I don’t have a strong theoretical background in this area yet.

Here’s what I’ve been working on: I’m analyzing a simple contract that Mythril detects as having the vulnerability “External Call To User-Supplied Address.” While studying the external_calls module, I noticed that the detection seems to involve constraints from two sources:

Constraints explicitly defined in the module itself, such as verifying that the available gas is greater than 2300 and checking if the destination address matches the attacker's:

constraints = [  
    UGT(2_gas, 2300),  
    1271270613000041655817448348132275889066893754095 ==  
    Concat(0,  
        If(1_calldatasize <= 12, 0, 1_calldata[12]),  
        If(1_calldatasize <= 13, 0, 1_calldata[13]),  
        ...  
        If(1_calldatasize <= 31, 0, 1_calldata[31]))  
]  

Could you explain how this Concat function works in this context? Specifically, what is calldata and calldatasize, and how are they used here?

Constraints from state.world_state.constraints. I couldn’t fully grasp how these constraints are gathered and added to the detection process. What criteria are used to determine whether something qualifies as a constraint and gets added to state.world_state.constraints?

From my understanding, these constraints are then provided to the SMT solver to check if there’s any sequence of transactions that satisfies them, ultimately identifying vulnerabilities. Are there optimizations applied to these constraints before they are passed to the solver?

Additionally, are detection modules in Mythril generally structured in a similar way—that is, by combining module-specific constraints with those from world_state and passing them to the solver?

Once again, I apologize if this question seems simple, but I really want to understand how these pieces fit together. Your insight would mean a lot to me as I try to overcome this learning plateau.

Thank you so much for your time and for all the work you do in this field. Mythril is such an inspiring tool, and your support has been invaluable.
Best regards,
M. Silva

[norhh]

Hi @matheus-junio-da-silva, sorry for the delay.
call_data here is modeled as an array. So, call_data_size is the size of the array.
Consider the first argument, it ranges in the calldata from 0 to 32. So, it's actual value is calldata[0:32], which is equivalent to that concat function, since, we do not know the actual size of calldata, we model it symbolically with calldatasize as its bound.

Constraints from [state.world_state.constraints](https://github.com/Consensys/mythril/blob/0cd0a8974f4aa6ee6e11ad0012745ae22d15cea4/mythril/analysis/module/modules/external_calls.py#L89). I couldn’t fully grasp how these constraints are gathered and added to the detection process. What criteria are used to determine whether something qualifies as a constraint and gets added to state.world_state.constraints?

One example to explain this is for branching out. When you encounter a JUMPI instruction with it's condition which is symbolic. The condition can either be true or false, so we model it by copying a new state and adding condition to one state and Not(condition) to the other state which has been copied. You can check it out here: https://github.com/Consensys/mythril/blob/2a48dcd5af27c39d5b63590b5c6340b0fb717d92/mythril/laser/ethereum/instructions.py#L1619.

Additionally, are detection modules in Mythril generally structured in a similar way—that is, by combining module-specific constraints with those from world_state and passing them to the solver?

Yes, I believe most of the detection modules are modeled as you have mentioned.

Feel free to ask me any more questions.