[Z3在python中的按位运算

问题描述 投票:0回答:1

再次,我在Z3上苦苦挣扎。我正在尝试从使用IDA反汇编的二进制文件中构建代码:ida graph

此函数被调用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()

一如既往,非常感谢!

python bit-manipulation z3
1个回答
0
投票

这里有一些问题,但最重要的是您对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

© www.soinside.com 2019 - 2024. All rights reserved.