ETH enumerate undergoing

[Hearmen]

I noticed that there is something wrong when I am using this fantastic lib. It can not analysis ETH bytecode correctly when there is bytecode like

3d52 63 PUSH4 0xffffffff
3d57 16 AND
3d58 56 JUMP

And I find a comment in function ssa_stack_memory_storage_flow_instruction

logging.warning('JUMP DYNAMIC TODO')
logging.warning('[X] push_instr %s push_instr %x' % (push_instr.name, push_instr.offset))

I think is is because the push_instr.ssa is something like ADD PUSH XXX, PUSH YYY.

I wonder why you have not do this job. Is there something more complex hiding?

[pventuzelo]

Yes it's more complex.

In your case, the jump target offset is calculated dynamically when the AND occurs and the result is pushed to the stack. This value will be pop from the stack when the JUMP is executed.

The SSA engine only do static analysis (stack evaluation) and not dynamic analysis meaning that it will not calculate the result of AND(0xffffffff, %5)
The only way to statically retrieve the correct jump target offset is to used symbolic execution.

I'm currently working on EVM symbolic execution, can you provide me the complete bytecode and i will try to make it work ;)

[Hearmen]

Thanks for you replay,
The bytecode is at https://etherscan.io/address/0xabeed8e3f3e5e9862c2b500dfbe3c8d0e82489e5#code, I am sorry that I can not figure out which sol code could compile into this bytecode.

Thank you very much

[pventuzelo]

Thanks,
so the issue is what i was thinking (dynamic jump value):

WARNING:root:JUMP DYNAMIC TODO
WARNING:root:[X] push_instr 126f: AND
WARNING:root:[X] push_instr.ssa %87 = AND(%86, %85)
WARNING:root:[X] push_instr.ssa ['%86 = #0x2469', '%85 = #0xFFFFFFFF']

The jump target is the result of AND(0x2469, 0xFFFFFFFF), so at the current state the SSAengine is not able to convert that into a valid offset.
I'm working actually on ETH Symbolic execution, so i will update this piece of code asap and let you know in this issue when the code is available.

Thank for your feedback

[pventuzelo]

I have added some code into the Ethereum part of Octopus.
Also, i took your example as a test and it worked now.

In case of basic arithmetic operation (like AND), Octopus will try to resolve the operation and use the concrete result as the jump target offset.

You will need to run pip3 install -r requirements.txt again in order to install z3-solver package.

If you get some other bugs/crashes, don't hesitate to create issues with the smart contract address and i will fixes them ASAP ;)

[Hearmen]

Thank you very much，and while using it I encounter another question. When it analysis bytecode like https://etherscan.io/address/0x4Ea7De704bd13D48a2FdB5C81D54dBC50fE49319#code , it will cause an MEMORY ERROR. I wonder how to resolve it.

some other contract :
https://etherscan.io/address/0x3a2fe50bEAE11814E04f55f9D9F950659E48Eac3#code
https://etherscan.io/address/0x2C063A26BAe823A7497Cb4bfD2b9dc5D4d124A16#code
https://etherscan.io/address/0x2202aE82877aC6f5E516bb9db841B28F3d8F6681#code

Thank you.

[pventuzelo]

Thanks for the report, i have created a specific ticket #3 for the memory issue.
I will let you know of the evolution ASAP.