2.elf z3暴力破解

通过进行动态调试发现确实


此处是进行校验的字符串

但是开始我所理解的顺序不是从左到右而是从低位到高位如图


0x04,0x46,0x81,0x63……正是v4从低位到高位的顺序排列的，我又犯了些低级错误。。。。。

所以此处通过z3

from z3 import *
a=[0x4,0x46,0x81,0x63,0x14,
0x53,0x17,0x6d,0x6a,0x67,0x76,0x16,0x34,0x14,
0x34]
flag = [BitVec('flag[%2d]' % i, 8) for i in range(14)]
out=[0]*14
for i in range(14):
    out[i]=flag[i]
v0=0
for i in range(14):
    for j in range(3):
        out[i]^=i^j^0x32
        out[i]+=v0
        v0+=1
f=Solver()
for i in range(14):
    f.add(out[i]==a[i])
while(f.check()==sat):
    condition = []
    m = f.model()
    p=""
    for i in range(14):
        p+=chr(int("%s" % (m[flag[i]])))
        condition.append(flag[i]!=int("%s" % (m[flag[i]])))
    print(p)
    f.add(Or(condition))

找到了对应的flag（也许？）