Additional symbolic expressions

[dmtch]

Hi! I was trying to solve this crackme with Ponce. In this way I got a problem. Look:

1. run the binary with one argument "AAAAAAAAAAAA", stop on main() and symbolize argv[1] bytes;
2. then, stop on first branch that checks argv[1] characters and use "Negate & Inject" feature;
3. look at argv[1] - it's filled with invalid characters, e.g. NULLs. For this challenge we need to put additional expressions for argv[1] variables: they have to be in range from 0x20 to 0x7f, obviously :) Is there any way to do this? Thanks!

[0ca]

Hi!

Thanks for trying Ponce. I check the same crackme with the same result:

[+] Solution found! Values:
 - SymVar_1 (argv[1][1]):0xff 
 - SymVar_3 (argv[1][3]):00 
 - SymVar_7 (argv[1][7]):00
 - SymVar_9 (argv[1][9]):00

We could add an option to automatically add an ascii constrain to all the characters in the arguments.

But it should be an option so the user can solve conditions that need the argument to be shorter, like in:

if strlen(argv[1])>5)
{
     printf("Too long!\n");
     exit(-1);
}

I will try to implement this soon.

Thank you for the feedback ;)

[dmtch]

Maybe it will be more universal if we could set arbitrary expressions for our variables, not just ascii characters for argv? What do you think?

[0ca]

I agree. It would be cool to be able to set "arbitrary expressions", or constraints to variable in the "Taint/Symbolic items" window:

[illera88]

Implemented at 23ea73e