search

illera88 / Ponce

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
https://docs.idaponce.com
Other
1.48k stars 72 forks source link

[Question] Limitations of symbolizing memory #76

Closed ferbeb closed 4 years ago

ferbeb commented 7 years ago

To be honest I am not sure what symbolic execution is capable of and if it should work for the following rather simple code:

ponce

I symbolized the memory at global_input:

[+] Ponce plugin version: 0.1.20161027.deceab6 running! [+] Symbolizing memory from 0x215084c to 0x2150856. Total: 11 bytes [+] Reanalizyng instruction at 0x4084d8

Strangely, I could not symbolize the memory in the Hex window, the Symbolize Memory option was grayed out, so I used the dialog instead. I am positive that I symbolized the right memory, I checked in the hex window that in fact my input ("123456789a") is located at 0x215084c.

As you can see on the screenshot, Ponce was seemingly not able to recognize the condition depends on the symbolized memory.

Did I use Ponce wrong, or is symbolic execution not capable of solving this problem?

I apologize for my lack of knowledge about symbolic execution and Triton, I hope you don't mind helping me out anyway, thanks.

illera88 commented 7 years ago

Hi, sorry for not getting back to you earlier. It seems that you are doing it right. Ponce should be able to help you in this situation. Do you mind providing me the binary so I can debug it? If you don't want/ can't send me the binary we can try other things but I can help you out faster with it.

Cheers

ferbeb commented 7 years ago

Thanks for getting back to me.

Here's the binary, it's a beginner crackme that just decrypts a xor-ed function before calling it. I also uploaded an idc script that does the decryption.

Link

illera88 commented 4 years ago

Should be fixed on v0.3.

Let me know if it is not and I'll reopen it.

Thanks for reporting.