n00b question

[vyrus001]

I'm sure this is a total idiot question as I am fledgling at using SMT solvers still, but is it possible after one has symbolized a desired piece of user input, to solve for a location (similar to what is done in the first example) where the application does not exit after it is resumed and the input is symbolized?

I am working with a target currently where I can successfully breakpoint the application and find the targeted memory input with trivial ease, but then when I resume, the ray tracing never finishes and when I stop the processes, I am unable to select my "win branch" (which I have identified) and solve for it.

Is there a way to do this?

[0ca]

@vyrus001 So the problem is that Ponce is not finishing after you symbolize an input?

You could do the trace manually and see where the execution is going. Probably Ponce is going inside some big functions and it is taking a lot of time to process all the instructions. You could skip these functions if you know they are not using your input.

So my recommendation is first use the taint analysis. This analysis should be faster and use less RAM. And then manually identify which functions you could skip (using F8) to reach the conditions you want to negate.

If you need more help, an example, or binary would be very helpful ;)

[vyrus001]

so my issue is not that i don't know where execution is going, as i have identified the path i WANT it to go but cant make it go there. I am attempting to perform a task very similar to the first gif example where you symbolize a piece of user input and then solve it to a specific branch. However, in that example, you wait for the program to exit and then are able to right click on the branch you want to solve for and see the equation displayed. In my case, the code that executes up to that "fork" is in a standalone loop, there for the application does not "exit" after the "failure" case has been executed. As such, when I then stop the program after the memory has been symbolized, I see no option to execute to my desired branch, as the ray tracing results seem to have disappeared as the result of the application not exiting after its first run of execution.

Its also possible I am simply missing something in the example, in which case I would be happy to discuss offline and not take up an issue thread.

[0ca]

I see, you could set a breakpoint at the end of the loop so after the first execution you see all the tainted/symbolized instructions and you could solve symbolized conditions.

Other option is put a breakpoint in the condition you are interested, so the tracing will stop when that instruction is reached and if it is symbolized you could solve it or negate it (modify in runtime the path taken).

ps: I am happy to talk offline. Add me to hangouts: foca at salesforce.com

[vyrus001]

I have invited you on hangouts, but just to update...

so the situation I am dealing with is the following

lea       r9, [rbp+67h]
lea       r8, dword_7FF6EF0C3F58
lea       rcx, [rbp+5Fh+lpThreadId] ; key input
call      sub_7FF6EEC84D58 <- my breakpoint is here!
cmp       eax, 1
setz      cs:byte_7FF6EF0C3F4D
cmp       eax, 1
jnz       loc_7FF6EEC85FD8

so the path I want to solve for is where the jnz instruction in the segment above does not jump. Weather or not it jumps is based on the return of the function where I have set my breakpoint (indicated above). Now before you ask, yes, I could manually reverse the function that call points to but I am attempting to gain experiance with ponce as well as SMT in general so instead of doing that, I'm trying to get ponce to solve that for me.

the input in question is a char ptr inside rcx at the time of my breakpoint. I can track down this ptr and symbolize memory just as the examples show in the ponce documentation (yay). But if i resume after the break point, the application simply returns to a neutral state, and sense it never "ends" my SMT menu is never populated with "solve for here -> ".

.if i put an additional breakpoint exactly on the jnz instruction, my target application crashes. (still not sure why on that one), so pausing at the jnz and then using negate to artificially execute into where I want and then solve is ALSO apparently not an option.

Just for good measure, I have also tried break pointing much further down the branch I don't want things to go and letting the ray trace finish (as well as avoiding the crash) in order to get to the point where i can "solve for" well... anything... and so far, nothing.

[0ca]

@vyrus001 thank you for the detailed explanation.

One thing it could be happening is inside the sub_7FF6EEC84D58 some library functions (syscalls, stdlib, etc....) is call and Ponce get stuck there because it is being executed tons of instructions. We want to show in the future more information about the current status of ponce (How many instructions are being analyzed).

You can use F7 to go inside the function and see how Ponce is working inside. If your input (rcx) is used inside you should see Ponce identifying symbolic instructions and coloring them.

Could you share the binary or the instructions inside sub_7FF6EEC84D58?

Thank you!

[vyrus001]

I could, but I probably shouldn't, it would also be a very LONG post as it is a giant function. However, I can verify that ponce doesn't get stuck there since as I stated earlier, if I remove all break points aside from the one shown above, the application functions just fine however the application does not exit and I'm back to the issue where i have lots of ray's traced but nothing I can solve for

[0ca]

@vyrus001 here you can see the function we are blacklisting (because they don't modify the user input) https://github.com/illera88/Ponce/blob/master/Ponce/src/blacklisted.hpp We want to add in the future quite more functions to that list.

It would be helpful if you can manually go inside the function and using F7 see where Ponce got stuck.

[0ca]

The problem was the program was using strchr and this function was using FPU operations unsupported by Triton/Ponce.

We will work in the future to provide equivalent expression for the most common library functions used to parse user input (strcmp, strchr, etc...)

And we will show warning or some kind of feedback when an instruction (like the fpu in this case) is not supported.