再次,我在Z3上苦苦挣扎。我正在尝试从使用IDA反汇编的二进制文件中构建代码:
此函数被调用0x80次。 ecx初始化为0x40。 [rdi + 8]初始化为0xDEADFACEDEADBEEF。 rsi从我试图找到的向量“ vec”中获取每个字节,其值只能是0x30、0x31和0x32。我不确定我的逻辑是否正确,或者我没有使用正确的Z3函数。它不是SAT,应该是SAT,因为最终我问题中的向量'v1'应该包含值0x123456701234567。我的代码:
from z3 import *
def set_number(vec,size): #vec
for i in range(0, size * 8 - 8, 8):
val = Extract(i + 7, i, vec)
val = BV2Int(val,False)
return Or(val==0x30,val == 0x31, val == 0x32)
s = z3.Solver()
size = 0x80
ecx = 0x40
v1 = BitVecVal(0xDEADFACEDEADBEEF,64)
vec = BitVec("inf",size*8) # <content from d.d file>
s.add(set_number(vec,size)) #40 bytes of {0,1,2}
for i in range(0, size*8-8, 8):
val = Extract(i + 7, i, vec)
val = BV2Int(val,False)
if(val == 0x30):
v1 = RotateLeft(v1, ecx)
v1 = v1 >> 1
v1 *= 2
v1 = RotateRight(v1, ecx)
ecx = ecx - 1
s.add(ecx>=0)
elif(val == 0x31):
s.add(ecx<40 and ecx>=0)
ecx = ecx+1
v1 = RotateLeft(v1,ecx)
v1 = v1 >> 1
v1 *= 2
v1 = RotateRight(v1,ecx)
ecx = ecx+1
elif (val==0x32):
s.add(ecx < 40 and ecx >= 0)
ecx = ecx + 1
v1 = RotateLeft(v1, ecx)
v1 = v1 >> 1
v1 *= 2
v1 = v1 | 1
v1 = RotateRight(v1, ecx)
ecx = ecx+1
s.add(v1 == 0x123456701234567)
s.check()
一如既往,非常感谢!
这里有一些问题,但最重要的是您对if-then-else
的使用。使用符号值时,不能使用Python的if-then-else。相反,您必须使用z3的If
构造。
在您的程序中,对if-then-else的值进行了具体评估,因此最后得到了虚假的断言。您可以通过在调用print s.sexpr()
之前放置check
来对此进行验证。
[通过调用if-then-else's
函数替换所有If
开始。然后在每个步骤中查看s.sexpr()
(假设在每个add
之后),并确保它包含正确的表达式。那应该导致您正确编码问题。从这里开始阅读:https://z3prover.github.io/api/html/namespacez3py.html#a782883a35d4c6a0be62cd5333645dbaf