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
Required steps to integrate maybe-alias analysis into the symbolic execution engine #1401
Comments
Hi @mrphrazer & @fvrmatteo ! Ok, let me rephrase, to be sure I understand correctly what you proposed, and maybe add some precision.
sb = SymbolicExecutionEngine(lifter)
sb.symbols[ExprId("RAX", 64)] = ExprOp("may_alias", ExprId("RAX", 64), ExprId("RBX", 64), ExprId("RCX", 64))
sb.symbols[ExprId("RBX", 64)] = ExprOp("may_alias", ExprId("RBX", 64), ExprId("RAX", 64), ExprId("RCX", 64))
sb.symbols[ExprId("RCX", 64)] = ExprOp("may_alias", ExprId("RCX", 64), ExprId("RAX", 64), ExprId("RBX", 64)) Note the arguments order in the initialization.
MOV QWORD PTR [RAX], 0x1
MOV RCX, QWORD PTR [RAX]
CMP RCX, 0x2
JZ loc_20 During the evaluation of the first line ExprMem(ExprOp(RAX, RBX, RCX), 64) = 1 If we use the current memory assignment hook (eval_assignblk) in the Symbolic engine to customize the "assignment", we could do the nexts steps:
ExprMem(RAX, 64) = 1 This will in return link ExprMem(RAX, 64) to 1 in the "classic" symbolic engine.
Next, we will evaluate the mov. So the code will evaluate So rcx is 1, so the CMP is not taken. Ok, now let's apply this to your example: MOV QWORD PTR [RAX], 0x1
MOV QWORD PTR [RBX], 0x2
MOV RCX, QWORD PTR [RAX]
CMP RCX, 0x2
JZ loc_20 The first
The next line,
now, when evaluating the line
Are those steps seems legit to you guys? It seems that this "poc" might be done using the current engine, correct? |
Heya guys!
I was discussing together with @fvrmatteo the following case: By default, Miasm's memory model assumes that symbolic memory addresses do not aliase. As a result, the symbolic execution engine never takes the jump since
@64[RAX]
can never be0x2
.To handle cases like that, I wrote a maybe-alias analysis which tells me possible code locations that might aliase. Then, I can handle it manually by mapping those to the same values, like
In other words, I can handle both cases individually: By default, they will never aliase. If I map them to the same value, we handle the aliasing case.
However, I would like to build sth such that the symbolic execution stops at a conditional branch at the end of the basic block. It might look similar to the following:
I'm aware that Miasm doesn't support this right now. However, I am currently trying to figure out would be required/the best way to implement it on my own. I think I would have to introduce a
maybe_aliase
operator, perform some analysis beforehand and propagate it somehow during symbolic execution. Would you guys agree or do you even think there might be an easier way to realize that?Best,
mrphrazer
The text was updated successfully, but these errors were encountered: