z3借鉴了JX Note的博客
题目解答借鉴了夏了茶糜的博客

这次结合着python的re正则表达式，来对z3进行一次系统的学习，如果写好了，事半功倍，一旦里面出点差错，基本上就没的搞了。后面会有补充，会什么就写什么吧。

z3一些点

创建变量
[Int(‘a%d’%i) for i in range(15)]、[BitVec(‘a%d’%i) for i in range(15)]
还有Real之类的等等，这里注意一下，虽然变量叫a1，a2之类的，但在后面写表达式可以用a[i]表达

创建求解器
s=z3.Solver() ##记得括号

添加表达式
s.add()
这里添加可以通过eval(str)进行批量添加

检查约束条件
s.check() ##结果只有sat和unsat
s.check ##我们构造的check结构

得出结果
s.model()
出来的type是个instance类型，算是一个畸形字典，现在我还是不太懂，等后面深入学习一下python在做补充
现在假设a1=0,a2=1,a3=2
m=s.model()
print m
print m[a1]

结果展示：
[a1=0,a2=1,a3=2]
0

instance通过as_long()转换成instancemethod类型，然后就可以运算啥的，各种变幻了
res=(m[a0].as_long()^i)<<5

大致z3就是这么个东西，很方便的一个工具

例题

攻防世界————babyunic

这道题，真的挺牛逼的，里面我还学到了设置lib库导入的姿势，虽然对这个题没什么逼用，具体的就不分析了，主要是中间正则的表达式，这道题就是先用unicorn-engine框架创建，然后调用了一个mips的func，主要函数在mips的func里面，里面就是一个42方程，然后这里作者用的re正则把整个copy过来的式子简化放到z3了，这里我也是学着写了写

脚本：

#ida-python
import binascii
for i in range(0x0000000000202020,0x00000000002020C7,4):
    if Byte(i)==0xff:
        print str(-(0-int(binascii.hexlify(get_bytes(i,4)),16)&0xffffffff))+",",
    else:
        print str(int(binascii.hexlify(get_bytes(i,4)),16))+",",
print
#因为是大端序，所以需要用大端序方式读，ida编译出来的是小段序，这里我直接是进行了十六进制负数的转化
#解题脚本
import ctypes
import z3
import ctypes
import re
#这里我只写了一部分，想做题的可以直接去[夏了茶糜](https://blog.csdn.net/qin9800/article/details/104826788)博客看，不然这个42元方程太长了
a='''*piParm2 = ((((((((((((((((((((((((((((((((uint)*pbParm1 + (uint)pbParm1[1] + (uint)pbParm1[2]) -
                                          (uint)pbParm1[3]) + (uint)pbParm1[4]) - (uint)pbParm1[5])
                                       - (uint)pbParm1[6]) - (uint)pbParm1[7]) - (uint)pbParm1[8]) +
                                     (uint)pbParm1[9] + (uint)pbParm1[10]) - (uint)pbParm1[0xb]) +
                                  (uint)pbParm1[0xc]) - (uint)pbParm1[0xd]) - (uint)pbParm1[0xe]) +
                               (uint)pbParm1[0xf]) - (uint)pbParm1[0x10]) - (uint)pbParm1[0x11]) +
                             (uint)pbParm1[0x12] + (uint)pbParm1[0x13]) - (uint)pbParm1[0x14]) +
                           (uint)pbParm1[0x15] + (uint)pbParm1[0x16] + (uint)pbParm1[0x17] +
                          (uint)pbParm1[0x18]) - (uint)pbParm1[0x19]) + (uint)pbParm1[0x1a]) -
                       (uint)pbParm1[0x1b]) + (uint)pbParm1[0x1c] + (uint)pbParm1[0x1d]) -
                     (uint)pbParm1[0x1e]) - (uint)pbParm1[0x1f]) + (uint)pbParm1[0x20]) -
                  (uint)pbParm1[0x21]) + (uint)pbParm1[0x22] + (uint)pbParm1[0x23]) -
                (uint)pbParm1[0x24]) - (uint)pbParm1[0x25]) + (uint)pbParm1[0x26]) -
             (uint)pbParm1[0x27]) + (uint)pbParm1[0x28] + (uint)pbParm1[0x29];
'''
res=[ -108, -200, 294, -216, -1008, 660, -866, 1770, 220, 6, -244, -522, -1406, -816, 386, 990, 334, 690, -1832, 372, -1370, -1580, 450, -1668, 858, 326, -196, -1516, 462, 2012, -696, 152, 2142, -592, -68, 878, -178, -1994, 1472, 1710, 1684, 34]

#上面是我直接得出的数组，下面是原作者通过ctype得出来的
tmp = ['ffffff94', 'ffffff38', '00000126', 'ffffff28', 'fffffc10', '00000294', 'fffffc9e', '000006ea', '000000dc', '00000006', 'ffffff0c', 'fffffdf6', 'fffffa82', 'fffffcd0', '00000182', '000003de', '0000014e', '000002b2', 'fffff8d8', '00000174', 'fffffaa6', 'fffff9d4', '000001c2', 'fffff97c', '0000035a', '00000146', 'ffffff3c', 'fffffa14', '000001ce', '000007dc', 'fffffd48', '00000098', '0000085e', 'fffffdb0', 'ffffffbc', '0000036e', 'ffffff4e', 'fffff836', '000005c0', '000006ae', '00000694', '00000022']
piParm2 = list(map(lambda x:z3.IntVal(ctypes.c_int32(int(x,16)).value),tmp))

#正则表达式的对齐
a=re.sub(r'\(uint\)',"",a)                    #去掉(uint)    ps:因为正则表达式中，一个()表达一个group，所以我们这里需要将他转义成正常字符，这里的r有没有都可以
a=re.sub(r'\*pbParm1',"pbParm1[0x0]",a)        #有一个没下标，更改一下下标，*记得转义
#替换回车、空格、大空格
a=re.sub('\n',"",a)                            
a=re.sub(' ',"",a)                            
a=re.sub('\t',"",a)    
#将所有[]里的值变成0x之类的，例如[0x0]、[0x1]等等        
for i in range(11):
    a=re.sub(r"\[%d\]" %i,"[%s]"%hex(i),a)
#将所有pbParm1[0xk] 变成m[t]
for i in range(42):
    a=re.sub(r"pbParm1\[%s\]"%hex(i),"m[%d]"%i,a)
#去掉开头的piParm2
a=re.sub(r"piParm2\[%s\]","",a)
#替换等号，去掉;
a=re.sub('=',"",a)
a=re.sub(';',r" =="+"\n",a)

#设置正则表达式
patt=re.compile(r"\(.*?==")            #ps?表示取正则匹配到的数据中最小的一种
#创建数组
arr=patt.findall(a)
#编写z3
m=[z3.Int('m%d'%i) for i in range(42)]
s=z3.Solver()
#print len(arr)
#print
#print m
for i in m:
    s.add(i<0xff)
    s.add(i>0)
k=0
#print s
for i in arr:
    #print i+str(res[k])
    s.add(eval(i+str(res[k])))
    k+=1
flag=""
#打印输出
if s.check()== z3.sat:
    tem=s.model()
    print type(tem[m[0]].as_long)
    for i in range(42):
        te=tem[m[i]].as_long() ^ i
        #print te
        flag+=(chr(((te>>3)&0xff)+(te<<5)&0xff))
print flag

效果图：
效果图
用了一下午，感觉挺有趣的，就记下来，以后应该会用到。累了，去玩会

赏

一个好奇的人