-
Notifications
You must be signed in to change notification settings - Fork 540
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Question: enhancing code coverage with external tracers #1269
Comments
You have to update the memory only if there is a desynchronization between your real CPU state (via IntelPin/Dynamorio) and the Triton's state Take a look at the |
Thank you so much for your response @JonathanSalwan . I did it and my path constraint is still empty. As soon as I enabled ONLY_ON_TAINTED, and the memory region containing my data was symbolized and tainted, so the path constraints were filled and the number of paths was less than when ONLY_ON_SYMBOLIZED disabled (I take that as a good sign). That's the right way to do it? However, when I tried to solve branches, I got junk data, I expected the strings used in comparison. |
How do you solve a branch? If you want to solve a branch you have to take into account previous constraints too (what we call the path predicate). The constraint must be something like this ast = ctx.getAstContext()
pred = ctx.getPathPredicate() # returns the path predicate
crt = ast.land([pred, <your constraint that goes to your branch here>])
model = ctx.getModel(crt) |
Here are the whole instructions for strstr in libc fom my tracer:
This is the first constraint from ctx.getPathConstraints(), which is MultipleBranches:
But comparison will be done via XMM registers. What should I do? Another thing, is it okay that I got an exception when building the semantic (ctx.buildSemantics(inst))? Triton can disassemble the opcode, as you can see.
|
I'm not sure to get this point. If you receive a model from the solver, you just have to inject the model into symbolic variables that you defined at the beginning (probably in memory cells).
If you receive a Here is the list of supported x86_64 instructions :). |
I changed the source to only do this:
Backward slice for the first 4 bytes of memory looks like this:
P.S: If you've gotten emails from Github for editing messages, I'm sorry. I got confused and don't know what I did wrong! |
In order to increase the code coverage, I want to solve the unsolved branches. Sample target does only string comparison (strcmp) .
My tarcer was IntelPin/Dynamorio, I sent execution information to Triton like instructions and registers, and updated memory via Triton callbacks. Update will lose path constraints, like issue #1128 . In this situation, I don't know what to do. I'm going to send and want to solve some specific execution regions.
Any leads like pseudo code or workflow that can clarify the path are appreciated.
The text was updated successfully, but these errors were encountered: